[racket] typed racket, filters, and polymorphism

If you want the type checker to ensure your program is unit-correct, I assume you also want no run-time residual of the dimensions but that is in conflict with wanting a structure because it imposes a run-time cost. Are you sure you want a unit? -- Matthias






On Sep 28, 2014, at 1:37 PM, Alexander D. Knauth wrote:

> No because I want the unit to be a struct that has a dimension field, not a symbol with various dimensions defined as unions of units.
> I want the unit to be based on the dimension, not the other way around, so that new units can be made that have the same dimension.
> 
> I have something like the number+unit struct (I called it measure), but I’ll work on more that after I have the unit struct figured out.  
> 
> On Sep 28, 2014, at 12:13 PM, Spencer florence <spencerflorence at gmail.com> wrote:
> 
>> 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 
>> 
>> 
> 
> ____________________
>  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/0821b16d/attachment-0001.html>