[racket] users Digest, Vol 109, Issue 73
Please take me off the list
Thanks
On Sun, Sep 28, 2014 at 10:29 PM, <users-request at racket-lang.org> wrote:
> Send users mailing list submissions to
> users at racket-lang.org
>
> To subscribe or unsubscribe via the World Wide Web, visit
> http://lists.racket-lang.org/users/listinfo
> or, via email, send a message with subject or body 'help' to
> users-request at racket-lang.org
>
> You can reach the person managing the list at
> users-owner at racket-lang.org
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of users digest..."
>
>
> [Racket Users list:
> http://lists.racket-lang.org/users ]
>
>
> Today's Topics:
>
> 1. Re: typed racket, filters, and polymorphism (Alexander D. Knauth)
> 2. Re: typed racket, filters, and polymorphism (Matthias Felleisen)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Sun, 28 Sep 2014 22:03:02 -0400
> From: "Alexander D. Knauth" <alexander at knauth.org>
> To: Matthias Felleisen <matthias at ccs.neu.edu>
> Cc: racket users list <users at racket-lang.org>
> Subject: Re: [racket] typed racket, filters, and polymorphism
> Message-ID: <6237F562-9E68-4D2D-A307-49668BB8E5DF at knauth.org>
> Content-Type: text/plain; charset="utf-8"
>
>
>
> On Sep 28, 2014, at 8:25 PM, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
>
>>
>> Your message points out where gradual typing badly fails.
>>
>> Type systems combine two nearly orthogonal ideas: (1) proving theorems about your program and (2) bridging the gap between abstract linguistic constructs and concrete machine implementations. In a sense, the design of a type system should always have the goal to eliminate as much run-time overhead as possible.
>>
>> In this specific case, you have two aspects of dimensionality: dimension per se (I am sure there is a word for it) and the chosen unit to represent it. So if you know that a number denotes a distance, you can choose mm, m, and km to represent it. If you want to represent an area, you choose mm^2, m^2, km^2. Now if you want to compute the area of a rectangle, you write
>>
>> area-of-rectangle : Real [Distance in m] * Real [Distance in m] -> Real [Area in m^2]
>>
>> If someone writes (area-of-rectangle 1 [mm] 1 [km]), there is nothing wrong with it -- except that the type checker should insert a coercion from mm to m and from km to m (multiplying/dividing by 1,000). That is, a type system for this application ought to use the type elaboration process idea and translate code as it goes.
>>
>> This is quite comparable to the idea that a machine-oriented type system needs to insert a coercion from integer to real (for example) as Algol 60 and its degraded successors do.
>
> What I had in mind was for the structs to be available at run-time, but that ideally the optimizer could take them out for the intermediate operations and put them back for the final result.
>
> And then if this value goes into untyped code, then it knows at run-time that it has the unit (u* millimeter kilometer), which is unit=? to square-meter.
>
> Is this sort of like what happens with flonum unboxing?
>
>
>
>>
>> Our gradual type system lacks some (intensiona) expressive power, which is why you can't get close to this ideal.
>>
>> -- Matthias
>>
>>
>>
>>
>>
>>
>>
>>
>> On Sep 28, 2014, at 8:14 PM, Alexander D. Knauth wrote:
>>
>>> Yes I do want run-time residual of the dimensions, and yes I want a unit struct.
>>>
>>> Also if there?s run-time residual, then I can use predicates and occurrence typing, and it can also be used in untyped code with contracts instead of types.
>>>
>>> And also the type-checker would check if it is dimension-correct, but at run-time it would would still convert between different units of the same dimension, multiply and divide units, etc.
>>>
>>> On Sep 28, 2014, at 6:58 PM, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
>>>
>>>>
>>>> If you want the type checker to ensure your program is unit-correct, I assume you also want no run-time residual of the dimensions but that is in conflict with wanting a structure because it imposes a run-time cost. Are you sure you want a unit? -- Matthias
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>> On Sep 28, 2014, at 1:37 PM, Alexander D. Knauth wrote:
>>>>
>>>>> No because I want the unit to be a struct that has a dimension field, not a symbol with various dimensions defined as unions of units.
>>>>> I want the unit to be based on the dimension, not the other way around, so that new units can be made that have the same dimension.
>>>>>
>>>>> I have something like the number+unit struct (I called it measure), but I?ll work on more that after I have the unit struct figured out.
>>>>>
>>>>> On Sep 28, 2014, at 12:13 PM, Spencer florence <spencerflorence at gmail.com> wrote:
>>>>>
>>>>>> would something like this work?
>>>>>>
>>>>>> #lang typed/racket
>>>>>>
>>>>>> (struct (U) number+unit ([amount : Real] [unit : U]))
>>>>>>
>>>>>> (define-type Weight-Unit (U 'kg 'g 'mg '?g))
>>>>>> (define-type Weight (number+unit Weight-Unit))
>>>>>> (define-predicate weight? Weight)
>>>>>>
>>>>>> (: make-weight : Real Weight-Unit -> Weight)
>>>>>> (define (make-weight n u)
>>>>>> (number+unit n u))
>>>>>>
>>>>>> (: +/weight : Weight Weight -> Weight)
>>>>>> ;; something something needs unit conversion
>>>>>> (define (+/weight w1 w2)
>>>>>> (number+unit (+ (number+unit-amount w1)
>>>>>> (number+unit-amount w1))
>>>>>> (number+unit-unit w1)))
>>>>>>
>>>>>> (+/weight (make-weight 1 'kg) (make-weight 1 'kg))
>>>>>>
>>>>>>
>>>>>>
>>>>>> On Sun, Sep 28, 2014 at 11:03 AM, Alexander D. Knauth <alexander at knauth.org> wrote:
>>>>>>
>>>>>> Because the struct is representing a unit (kilograms, meters, seconds, etc.), and a unit has a dimension (mass, length, time, etc.) and I want the type-checker to be able to know what the dimension of a unit is so that the types of functions can specify the dimension that something should have.
>>>>>> The real solution to this would probably be bounded polymorphism, but I was wondering if there was some other way to do it with occurrence typing in the guard or something like that.
>>>>>>
>>>>>> On Sep 28, 2014, at 11:48 AM, Sam Tobin-Hochstadt <samth at cs.indiana.edu> wrote:
>>>>>>
>>>>>> > Why not do this with the type, instead of making this polymorphic?
>>>>>> >
>>>>>> > Sam
>>>>>> >
>>>>>> > On Fri, Sep 26, 2014 at 7:35 PM, Alexander D. Knauth
>>>>>> > <alexander at knauth.org> wrote:
>>>>>> >> Is it possible to have a struct that does certain things according to the
>>>>>> >> guard?
>>>>>> >> #lang typed/racket
>>>>>> >>
>>>>>> >> (struct (a) foo ([a : a]) #:transparent
>>>>>> >> #:guard (lambda (a _)
>>>>>> >> (unless (exact-integer? a)
>>>>>> >> (error 'foo "expected Integer, given ~v" a))
>>>>>> >> a))
>>>>>> >>
>>>>>> >> (ann (foo (ann 1 Any)) (foo Integer))
>>>>>> >>
>>>>>> >> (: x : (foo Any))
>>>>>> >> (define x (foo 1))
>>>>>> >>
>>>>>> >> (ann (foo-a x) Integer)
>>>>>> >>
>>>>>> >> ;. Type Checker: Polymorphic function `foo1' could not be applied to
>>>>>> >> arguments:
>>>>>> >> ;Argument 1:
>>>>>> >> ; Expected: a
>>>>>> >> ; Given: Any
>>>>>> >> ;
>>>>>> >> ;Result type: (foo a)
>>>>>> >> ;Expected result: (foo Integer)
>>>>>> >> ; in: (foo (ann 1 Any))
>>>>>> >> ;. Type Checker: Polymorphic function `foo-a' could not be applied to
>>>>>> >> arguments:
>>>>>> >> ;Argument 1:
>>>>>> >> ; Expected: (foo a)
>>>>>> >> ; Given: (foo Any)
>>>>>> >> ;
>>>>>> >> ;Result type: (a : ....)
>>>>>> >> ;Expected result: Integer
>>>>>> >> ; in: (foo-a x)
>>>>>> >>
>>>>>> >> On Sep 25, 2014, at 9:42 PM, Alexander D. Knauth <alexander at knauth.org>
>>>>>> >> wrote:
>>>>>> >>
>>>>>> >> What I?m trying to accomplish is something more like this:
>>>>>> >> #lang typed/racket
>>>>>> >>
>>>>>> >> (require "dimensions.rkt")
>>>>>> >>
>>>>>> >> (struct (d) unit ([name : Any] [scalar : Positive-Real] [dimension : d])
>>>>>> >> #:transparent
>>>>>> >> #:guard (lambda (name scalar dimension _)
>>>>>> >> (unless (dimension? dimension)
>>>>>> >> (error 'unit "expected Dimension, given ~v" dimension))
>>>>>> >> (values name scalar dimension)))
>>>>>> >>
>>>>>> >> (define-type (Unitof d) (unit d))
>>>>>> >>
>>>>>> >> (define-type Unit (Unitof Dimension))
>>>>>> >>
>>>>>> >> (define Unit? (make-predicate Unit))
>>>>>> >>
>>>>>> >> (define-type Unitish
>>>>>> >> (U (Unitof Any)
>>>>>> >> Dimension
>>>>>> >> Positive-Real))
>>>>>> >>
>>>>>> >> (: ->unit : (All (d) (case-> [(Unitof d) -> (Unitof d)]
>>>>>> >> [Unitish -> Unit])))
>>>>>> >> (define (->unit u)
>>>>>> >> (cond [(unit? u)
>>>>>> >> (unless (Unit? u) ; this should never happen anyway because of the
>>>>>> >> guard
>>>>>> >> (error '->unit "expected (Unitof Dimension), given ~v" u))
>>>>>> >> u]
>>>>>> >> [(dimension? u) (unit u 1 u)]
>>>>>> >> [(positive-real? u) (unit u u dimensionless-dimension)]))
>>>>>> >>
>>>>>> >>
>>>>>> >> On Sep 25, 2014, at 6:19 PM, Sam Tobin-Hochstadt <samth at cs.indiana.edu>
>>>>>> >> wrote:
>>>>>> >>
>>>>>> >> No, I don't think you can do this. Can you say more about what you're
>>>>>> >> trying to accomplish?
>>>>>> >>
>>>>>> >> Sam
>>>>>> >>
>>>>>> >> On Thu, Sep 25, 2014 at 6:15 PM, Alexander D. Knauth
>>>>>> >> <alexander at knauth.org> wrote:
>>>>>> >>
>>>>>> >> Do any of you have any advice for getting a function like this to
>>>>>> >> type-check?
>>>>>> >> #lang typed/racket
>>>>>> >>
>>>>>> >> (: check-int : (All (a) (case-> [a -> a]
>>>>>> >> [Any -> Integer])))
>>>>>> >> (define (check-int int)
>>>>>> >> (unless (exact-integer? int)
>>>>>> >> (error 'check-int "expected Integer, given ~v" int))
>>>>>> >> int)
>>>>>> >>
>>>>>> >> ;. Type Checker: type mismatch
>>>>>> >> ; expected: a
>>>>>> >> ; given: Integer in: int
>>>>>> >>
>>>>>> >>
>>>>>> >>
>>>>>> >> ____________________
>>>>>> >> Racket Users list:
>>>>>> >> http://lists.racket-lang.org/users
>>>>>> >>
>>>>>> >>
>>>>>> >> ____________________
>>>>>> >> Racket Users list:
>>>>>> >> http://lists.racket-lang.org/users
>>>>>> >>
>>>>>> >>
>>>>>>
>>>>>>
>>>>>> ____________________
>>>>>> Racket Users list:
>>>>>> http://lists.racket-lang.org/users
>>>>>>
>>>>>>
>>>>>
>>>>> ____________________
>>>>> Racket Users list:
>>>>> http://lists.racket-lang.org/users
>>>>
>>>
>>
>
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: <http://lists.racket-lang.org/users/archive/attachments/20140928/ca23ed92/attachment-0001.html>
>
> ------------------------------
>
> Message: 2
> Date: Sun, 28 Sep 2014 22:29:31 -0400
> From: Matthias Felleisen <matthias at ccs.neu.edu>
> To: "Alexander D. Knauth" <alexander at knauth.org>
> Cc: racket users list <users at racket-lang.org>
> Subject: Re: [racket] typed racket, filters, and polymorphism
> Message-ID: <6ADD4F6D-6B79-4F32-AD11-379CD2FF87AB at ccs.neu.edu>
> Content-Type: text/plain; charset="utf-8"
>
>
> You might be able to unwrap such things for a local context, but then you need to wrap it again on the way out. That cost might become quite high if it happens in a loop. Then again Racket programs rely on this a lot too (as do many dynamically typed programs) so it might not be a cost that kills performance completely. But do be aware of how others deal with this issue -- Matthias
>
>
>
>
>
>
>
> On Sep 28, 2014, at 10:03 PM, Alexander D. Knauth wrote:
>
>>
>>
>> On Sep 28, 2014, at 8:25 PM, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
>>
>>>
>>> Your message points out where gradual typing badly fails.
>>>
>>> Type systems combine two nearly orthogonal ideas: (1) proving theorems about your program and (2) bridging the gap between abstract linguistic constructs and concrete machine implementations. In a sense, the design of a type system should always have the goal to eliminate as much run-time overhead as possible.
>>>
>>> In this specific case, you have two aspects of dimensionality: dimension per se (I am sure there is a word for it) and the chosen unit to represent it. So if you know that a number denotes a distance, you can choose mm, m, and km to represent it. If you want to represent an area, you choose mm^2, m^2, km^2. Now if you want to compute the area of a rectangle, you write
>>>
>>> area-of-rectangle : Real [Distance in m] * Real [Distance in m] -> Real [Area in m^2]
>>>
>>> If someone writes (area-of-rectangle 1 [mm] 1 [km]), there is nothing wrong with it -- except that the type checker should insert a coercion from mm to m and from km to m (multiplying/dividing by 1,000). That is, a type system for this application ought to use the type elaboration process idea and translate code as it goes.
>>>
>>> This is quite comparable to the idea that a machine-oriented type system needs to insert a coercion from integer to real (for example) as Algol 60 and its degraded successors do.
>>
>> What I had in mind was for the structs to be available at run-time, but that ideally the optimizer could take them out for the intermediate operations and put them back for the final result.
>>
>> And then if this value goes into untyped code, then it knows at run-time that it has the unit (u* millimeter kilometer), which is unit=? to square-meter.
>>
>> Is this sort of like what happens with flonum unboxing?
>>
>>
>>
>>>
>>> Our gradual type system lacks some (intensiona) expressive power, which is why you can't get close to this ideal.
>>>
>>> -- Matthias
>>>
>>>
>>>
>>>
>>>
>>>
>>>
>>>
>>> On Sep 28, 2014, at 8:14 PM, Alexander D. Knauth wrote:
>>>
>>>> Yes I do want run-time residual of the dimensions, and yes I want a unit struct.
>>>>
>>>> Also if there?s run-time residual, then I can use predicates and occurrence typing, and it can also be used in untyped code with contracts instead of types.
>>>>
>>>> And also the type-checker would check if it is dimension-correct, but at run-time it would would still convert between different units of the same dimension, multiply and divide units, etc.
>>>>
>>>> On Sep 28, 2014, at 6:58 PM, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
>>>>
>>>>>
>>>>> If you want the type checker to ensure your program is unit-correct, I assume you also want no run-time residual of the dimensions but that is in conflict with wanting a structure because it imposes a run-time cost. Are you sure you want a unit? -- Matthias
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>> On Sep 28, 2014, at 1:37 PM, Alexander D. Knauth wrote:
>>>>>
>>>>>> No because I want the unit to be a struct that has a dimension field, not a symbol with various dimensions defined as unions of units.
>>>>>> I want the unit to be based on the dimension, not the other way around, so that new units can be made that have the same dimension.
>>>>>>
>>>>>> I have something like the number+unit struct (I called it measure), but I?ll work on more that after I have the unit struct figured out.
>>>>>>
>>>>>> On Sep 28, 2014, at 12:13 PM, Spencer florence <spencerflorence at gmail.com> wrote:
>>>>>>
>>>>>>> would something like this work?
>>>>>>>
>>>>>>> #lang typed/racket
>>>>>>>
>>>>>>> (struct (U) number+unit ([amount : Real] [unit : U]))
>>>>>>>
>>>>>>> (define-type Weight-Unit (U 'kg 'g 'mg '?g))
>>>>>>> (define-type Weight (number+unit Weight-Unit))
>>>>>>> (define-predicate weight? Weight)
>>>>>>>
>>>>>>> (: make-weight : Real Weight-Unit -> Weight)
>>>>>>> (define (make-weight n u)
>>>>>>> (number+unit n u))
>>>>>>>
>>>>>>> (: +/weight : Weight Weight -> Weight)
>>>>>>> ;; something something needs unit conversion
>>>>>>> (define (+/weight w1 w2)
>>>>>>> (number+unit (+ (number+unit-amount w1)
>>>>>>> (number+unit-amount w1))
>>>>>>> (number+unit-unit w1)))
>>>>>>>
>>>>>>> (+/weight (make-weight 1 'kg) (make-weight 1 'kg))
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>> On Sun, Sep 28, 2014 at 11:03 AM, Alexander D. Knauth <alexander at knauth.org> wrote:
>>>>>>>
>>>>>>> Because the struct is representing a unit (kilograms, meters, seconds, etc.), and a unit has a dimension (mass, length, time, etc.) and I want the type-checker to be able to know what the dimension of a unit is so that the types of functions can specify the dimension that something should have.
>>>>>>> The real solution to this would probably be bounded polymorphism, but I was wondering if there was some other way to do it with occurrence typing in the guard or something like that.
>>>>>>>
>>>>>>> On Sep 28, 2014, at 11:48 AM, Sam Tobin-Hochstadt <samth at cs.indiana.edu> wrote:
>>>>>>>
>>>>>>> > Why not do this with the type, instead of making this polymorphic?
>>>>>>> >
>>>>>>> > Sam
>>>>>>> >
>>>>>>> > On Fri, Sep 26, 2014 at 7:35 PM, Alexander D. Knauth
>>>>>>> > <alexander at knauth.org> wrote:
>>>>>>> >> Is it possible to have a struct that does certain things according to the
>>>>>>> >> guard?
>>>>>>> >> #lang typed/racket
>>>>>>> >>
>>>>>>> >> (struct (a) foo ([a : a]) #:transparent
>>>>>>> >> #:guard (lambda (a _)
>>>>>>> >> (unless (exact-integer? a)
>>>>>>> >> (error 'foo "expected Integer, given ~v" a))
>>>>>>> >> a))
>>>>>>> >>
>>>>>>> >> (ann (foo (ann 1 Any)) (foo Integer))
>>>>>>> >>
>>>>>>> >> (: x : (foo Any))
>>>>>>> >> (define x (foo 1))
>>>>>>> >>
>>>>>>> >> (ann (foo-a x) Integer)
>>>>>>> >>
>>>>>>> >> ;. Type Checker: Polymorphic function `foo1' could not be applied to
>>>>>>> >> arguments:
>>>>>>> >> ;Argument 1:
>>>>>>> >> ; Expected: a
>>>>>>> >> ; Given: Any
>>>>>>> >> ;
>>>>>>> >> ;Result type: (foo a)
>>>>>>> >> ;Expected result: (foo Integer)
>>>>>>> >> ; in: (foo (ann 1 Any))
>>>>>>> >> ;. Type Checker: Polymorphic function `foo-a' could not be applied to
>>>>>>> >> arguments:
>>>>>>> >> ;Argument 1:
>>>>>>> >> ; Expected: (foo a)
>>>>>>> >> ; Given: (foo Any)
>>>>>>> >> ;
>>>>>>> >> ;Result type: (a : ....)
>>>>>>> >> ;Expected result: Integer
>>>>>>> >> ; in: (foo-a x)
>>>>>>> >>
>>>>>>> >> On Sep 25, 2014, at 9:42 PM, Alexander D. Knauth <alexander at knauth.org>
>>>>>>> >> wrote:
>>>>>>> >>
>>>>>>> >> What I?m trying to accomplish is something more like this:
>>>>>>> >> #lang typed/racket
>>>>>>> >>
>>>>>>> >> (require "dimensions.rkt")
>>>>>>> >>
>>>>>>> >> (struct (d) unit ([name : Any] [scalar : Positive-Real] [dimension : d])
>>>>>>> >> #:transparent
>>>>>>> >> #:guard (lambda (name scalar dimension _)
>>>>>>> >> (unless (dimension? dimension)
>>>>>>> >> (error 'unit "expected Dimension, given ~v" dimension))
>>>>>>> >> (values name scalar dimension)))
>>>>>>> >>
>>>>>>> >> (define-type (Unitof d) (unit d))
>>>>>>> >>
>>>>>>> >> (define-type Unit (Unitof Dimension))
>>>>>>> >>
>>>>>>> >> (define Unit? (make-predicate Unit))
>>>>>>> >>
>>>>>>> >> (define-type Unitish
>>>>>>> >> (U (Unitof Any)
>>>>>>> >> Dimension
>>>>>>> >> Positive-Real))
>>>>>>> >>
>>>>>>> >> (: ->unit : (All (d) (case-> [(Unitof d) -> (Unitof d)]
>>>>>>> >> [Unitish -> Unit])))
>>>>>>> >> (define (->unit u)
>>>>>>> >> (cond [(unit? u)
>>>>>>> >> (unless (Unit? u) ; this should never happen anyway because of the
>>>>>>> >> guard
>>>>>>> >> (error '->unit "expected (Unitof Dimension), given ~v" u))
>>>>>>> >> u]
>>>>>>> >> [(dimension? u) (unit u 1 u)]
>>>>>>> >> [(positive-real? u) (unit u u dimensionless-dimension)]))
>>>>>>> >>
>>>>>>> >>
>>>>>>> >> On Sep 25, 2014, at 6:19 PM, Sam Tobin-Hochstadt <samth at cs.indiana.edu>
>>>>>>> >> wrote:
>>>>>>> >>
>>>>>>> >> No, I don't think you can do this. Can you say more about what you're
>>>>>>> >> trying to accomplish?
>>>>>>> >>
>>>>>>> >> Sam
>>>>>>> >>
>>>>>>> >> On Thu, Sep 25, 2014 at 6:15 PM, Alexander D. Knauth
>>>>>>> >> <alexander at knauth.org> wrote:
>>>>>>> >>
>>>>>>> >> Do any of you have any advice for getting a function like this to
>>>>>>> >> type-check?
>>>>>>> >> #lang typed/racket
>>>>>>> >>
>>>>>>> >> (: check-int : (All (a) (case-> [a -> a]
>>>>>>> >> [Any -> Integer])))
>>>>>>> >> (define (check-int int)
>>>>>>> >> (unless (exact-integer? int)
>>>>>>> >> (error 'check-int "expected Integer, given ~v" int))
>>>>>>> >> int)
>>>>>>> >>
>>>>>>> >> ;. Type Checker: type mismatch
>>>>>>> >> ; expected: a
>>>>>>> >> ; given: Integer in: int
>>>>>>> >>
>>>>>>> >>
>>>>>>> >>
>>>>>>> >> ____________________
>>>>>>> >> Racket Users list:
>>>>>>> >> http://lists.racket-lang.org/users
>>>>>>> >>
>>>>>>> >>
>>>>>>> >> ____________________
>>>>>>> >> Racket Users list:
>>>>>>> >> http://lists.racket-lang.org/users
>>>>>>> >>
>>>>>>> >>
>>>>>>>
>>>>>>>
>>>>>>> ____________________
>>>>>>> Racket Users list:
>>>>>>> http://lists.racket-lang.org/users
>>>>>>>
>>>>>>>
>>>>>>
>>>>>> ____________________
>>>>>> Racket Users list:
>>>>>> http://lists.racket-lang.org/users
>>>>>
>>>>
>>>
>>
>
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: <http://lists.racket-lang.org/users/archive/attachments/20140928/d95c74e9/attachment.html>
>
> End of users Digest, Vol 109, Issue 73
> **************************************