[racket] typed racket, filters, and polymorphism

You might be able to unwrap such things for a local context, but then you need to wrap it again on the way out. That cost might become quite high if it happens in a loop. Then again Racket programs rely on this a lot too (as do many dynamically typed programs) so it might not be a cost that kills performance completely. But do be aware of how others deal with this issue -- Matthias







On Sep 28, 2014, at 10:03 PM, Alexander D. Knauth wrote:

> 
> 
> 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/d95c74e9/attachment-0001.html>