No, I think we just need to add bounded polymorphism to TR. Sam
On Sun, Sep 28, 2014 at 12:02 PM, 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
