[racket] typed racket, filters, and polymorphism

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 <samth at 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
> <alexander at 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 <alexander at 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 <samth at 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
>> <alexander at 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
>> 
>>