[racket] typed racket, filters, and polymorphism

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
<alexander at 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 <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
>>> 
>>> 
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20140928/784e05a1/attachment-0001.html>