[racket] users Digest, Vol 109, Issue 72

Please take me off the list

Thanks

On Sun, Sep 28, 2014 at 8:26 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 20:14:43 -0400
> From: "Alexander D. Knauth" <alexander at knauth.org>
> To: Matthias Felleisen <matthias at ccs.neu.edu>
> Cc: Spencer florence <spencerflorence at gmail.com>, racket users list
>         <users at racket-lang.org>, Sam Tobin-Hochstadt <samth at cs.indiana.edu>
> Subject: Re: [racket] typed racket, filters, and polymorphism
> Message-ID: <B52D6D46-C9C1-46D6-9F1E-46800DB7B23C at knauth.org>
> Content-Type: text/plain; charset="utf-8"
>
> 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/f86df9a7/attachment-0001.html>
>
> ------------------------------
>
> Message: 2
> Date: Sun, 28 Sep 2014 20:25:45 -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>, Benjamin Greenman
>         <blg59 at cornell.edu>
> Subject: Re: [racket] typed racket, filters, and polymorphism
> Message-ID: <C3486009-3F00-4717-BD42-E18FF074FD4B at ccs.neu.edu>
> Content-Type: text/plain; charset="utf-8"
>
>
> 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.
>
> 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/d777b137/attachment.html>
>
> End of users Digest, Vol 109, Issue 72
> **************************************