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
