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
