Please take me off the list Thanks
On Sun, Sep 28, 2014 at 8:26 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 20:14:43 -0400 > From: "Alexander D. Knauth" <[email protected]> > To: Matthias Felleisen <[email protected]> > Cc: Spencer florence <[email protected]>, racket users list > <[email protected]>, Sam Tobin-Hochstadt <[email protected]> > Subject: Re: [racket] typed racket, filters, and polymorphism > Message-ID: <[email protected]> > 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 <[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/f86df9a7/attachment-0001.html> > > ------------------------------ > > Message: 2 > Date: Sun, 28 Sep 2014 20:25:45 -0400 > From: Matthias Felleisen <[email protected]> > To: "Alexander D. Knauth" <[email protected]> > Cc: racket users list <[email protected]>, Benjamin Greenman > <[email protected]> > Subject: Re: [racket] typed racket, filters, and polymorphism > Message-ID: <[email protected]> > 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 <[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/d777b137/attachment.html> > > End of users Digest, Vol 109, Issue 72 > ************************************** ____________________ Racket Users list: http://lists.racket-lang.org/users
