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
