Please take me off the list Thanks
On Sun, Sep 28, 2014 at 10:29 PM, <[email protected]> wrote: > Send users mailing list submissions to > [email protected] > > 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 > [email protected] > > You can reach the person managing the list at > [email protected] > > 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" <[email protected]> > To: Matthias Felleisen <[email protected]> > Cc: racket users list <[email protected]> > Subject: Re: [racket] typed racket, filters, and polymorphism > Message-ID: <[email protected]> > Content-Type: text/plain; charset="utf-8" > > > > On Sep 28, 2014, at 8:25 PM, Matthias Felleisen <[email protected]> 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 <[email protected]> >>> 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 >>>>> <[email protected]> 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 >>>>>> <[email protected]> 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 <[email protected]> >>>>>> 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 >>>>>> > <[email protected]> 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 >>>>>> >> <[email protected]> >>>>>> >> 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 >>>>>> >> <[email protected]> >>>>>> >> 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 >>>>>> >> <[email protected]> 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 <[email protected]> > To: "Alexander D. Knauth" <[email protected]> > Cc: racket users list <[email protected]> > Subject: Re: [racket] typed racket, filters, and polymorphism > Message-ID: <[email protected]> > 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 <[email protected]> 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 <[email protected]> >>>> 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 >>>>>> <[email protected]> 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 >>>>>>> <[email protected]> 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 >>>>>>> <[email protected]> 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 >>>>>>> > <[email protected]> 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 >>>>>>> >> <[email protected]> >>>>>>> >> 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 >>>>>>> >> <[email protected]> >>>>>>> >> 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 >>>>>>> >> <[email protected]> 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 > ************************************** ____________________ Racket Users list: http://lists.racket-lang.org/users
