Please take me off the list Thanks
On Sun, Sep 28, 2014 at 11:00 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) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Sun, 28 Sep 2014 23:00:17 -0400 > From: "Alexander D. Knauth" <[email protected]> > To: racket users list <[email protected]> > Subject: Re: [racket] typed racket, filters, and polymorphism > Message-ID: <[email protected]> > Content-Type: text/plain; charset="utf-8" > > I just realized that typed racket seems to ignore the guard anyway, so I > could do something like this and convince the type-checker that any value I > want has any type that I want: > > (struct (a) foo ([a : a]) > #:guard (lambda (a _) "this value")) > > (: x : (foo 1)) > (define x (foo 1)) > >> (foo-a x) > - : Integer [more precisely: One] > "this value? > > > On Sep 28, 2014, at 10:41 PM, Benjamin Greenman <[email protected]> wrote: > >> I was able to get something very similar to your example program to compile. >> >> (struct (a) foo ([a : a]) #:transparent >> #:guard (lambda (a _) >> (define a* a) ;; a* not "polluted" by occurrence typing >> (unless (exact-integer? a) >> (error 'foo "expected Integer, given ~v" a)) >> a*)) ;; we return a value of type a, so the typechecker >> is happy >> >> From here, you can safely cast a foo-a into an Integer. It's not type safe >> to ann because we (deliberately) don't have the occurrence typing >> information, but we the programmers can be sure that the casts will never >> fail. >> >> (cast (foo (ann 1 Any)) (foo Integer)) >> > (foo 1) >> >> >> >> On Sun, Sep 28, 2014 at 10:29 PM, Matthias Felleisen <[email protected]> >> wrote: >> >> 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/baf5ed5d/attachment.html> > > End of users Digest, Vol 109, Issue 74 > ************************************** ____________________ Racket Users list: http://lists.racket-lang.org/users
