[racket] typed racket, filters, and polymorphism

On Sep 28, 2014, at 8:25 PM, Matthias Felleisen <matthias at ccs.neu.edu> wrote:

> 	
> Your message points out where gradual typing badly fails. 
> 
> Type systems combine two nearly orthogonal ideas: (1) proving theorems about your program and (2) bridging the gap between abstract linguistic constructs and concrete machine implementations. In a sense, the design of a type system should always have the goal to eliminate as much run-time overhead as possible. 
> 
> In this specific case, you have two aspects of dimensionality: dimension per se (I am sure there is a word for it) and the chosen unit to represent it. So if you know that a number denotes a distance, you can choose mm, m, and km to represent it. If you want to represent an area, you choose mm^2, m^2, km^2. Now if you want to compute the area of a rectangle, you write
> 
>  area-of-rectangle :  Real [Distance in m] * Real [Distance in m] -> Real [Area in m^2]  
> 
> If someone writes (area-of-rectangle 1 [mm] 1 [km]), there is nothing wrong with it -- except that the type checker should insert a coercion from mm to m and from km to m (multiplying/dividing by 1,000). That is, a type system for this application ought to use the type elaboration process idea and translate code as it goes. 
> 
> This is quite comparable to the idea that a machine-oriented type system needs to insert a coercion from integer to real (for example) as Algol 60 and its degraded successors do. 

What I had in mind was for the structs to be available at run-time, but that ideally the optimizer could take them out for the intermediate operations and put them back for the final result.  

And then if this value goes into untyped code, then it knows at run-time that it has the unit (u* millimeter kilometer), which is unit=? to square-meter.  

Is this sort of like what happens with flonum unboxing?  



> 
> Our gradual type system lacks some (intensiona) expressive power, which is why you can't get close to this ideal. 
> 
> -- Matthias
> 
> 
> 
> 
> 
> 
> 
> 
> On Sep 28, 2014, at 8:14 PM, Alexander D. Knauth wrote:
> 
>> Yes I do want run-time residual of the dimensions, and yes I want a unit struct.  
>> 
>> Also if there’s run-time residual, then I can use predicates and occurrence typing, and it can also be used in untyped code with contracts instead of types.  
>> 
>> And also the type-checker would check if it is dimension-correct, but at run-time it would would still convert between different units of the same dimension, multiply and divide units, etc.  
>> 
>> On Sep 28, 2014, at 6:58 PM, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
>> 
>>> 
>>> 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/ca23ed92/attachment.html>