[racket] typed racket, filters, and polymorphism

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
>
>