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 <matth...@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 <spencerflore...@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 >>>> <alexan...@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 <sa...@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 >>>> > <alexan...@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 <alexan...@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 <sa...@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 >>>> >> <alexan...@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 >> >
____________________ Racket Users list: http://lists.racket-lang.org/users
