<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><br></div><div>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</div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><br><div><div>On Sep 28, 2014, at 10:03 PM, Alexander D. Knauth wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><meta http-equiv="Content-Type" content="text/html charset=utf-8"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div><br></div><br><div><div>On Sep 28, 2014, at 8:25 PM, Matthias Felleisen <<a href="mailto:matthias@ccs.neu.edu">matthias@ccs.neu.edu</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><span class="Apple-tab-span" style="white-space:pre"> </span></div><div>Your message points out where gradual typing badly fails. </div><div><br></div><div>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. </div><div><br></div><div>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</div><div><br></div><div> area-of-rectangle : Real [Distance in m] * Real [Distance in m] -> Real [Area in m^2] </div><div><br></div><div>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. </div><div><br></div><div>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. </div></div></blockquote><div><br></div><div>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. </div><div><br></div><div>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. </div><div><br></div><div>Is this sort of like what happens with flonum unboxing? </div><div><br></div><div><br></div><br><blockquote type="cite"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><br></div><div>Our gradual type system lacks some (intensiona) expressive power, which is why you can't get close to this ideal. </div><div><br></div><div>-- Matthias</div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><br><div><div>On Sep 28, 2014, at 8:14 PM, Alexander D. Knauth wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><meta http-equiv="Content-Type" content="text/html charset=utf-8"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div>Yes I do want run-time residual of the dimensions, and yes I want a unit struct. </div><div><br></div><div>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. </div><div><br></div><div>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. </div><br><div><div>On Sep 28, 2014, at 6:58 PM, Matthias Felleisen <<a href="mailto:matthias@ccs.neu.edu">matthias@ccs.neu.edu</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><br></div><div>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</div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><br><div><div>On Sep 28, 2014, at 1:37 PM, Alexander D. Knauth wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><meta http-equiv="Content-Type" content="text/html charset=utf-8"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div>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.</div><div>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.</div><div><br></div><div>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. </div><br><div><div>On Sep 28, 2014, at 12:13 PM, Spencer florence <<a href="mailto:spencerflorence@gmail.com">spencerflorence@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite">
<span id="mailbox-conversation"><div>would something like this work?</div>
<div><br></div>
<div>
<div>#lang typed/racket</div>
<div><br></div>
<div>(struct (U) number+unit ([amount : Real] [unit : U]))</div>
<div><br></div>
<div>(define-type Weight-Unit (U 'kg 'g 'mg 'μg))</div>
<div>(define-type Weight (number+unit Weight-Unit))</div>
<div>(define-predicate weight? Weight)</div>
<div><br></div>
<div>(: make-weight : Real Weight-Unit -> Weight)</div>
<div>(define (make-weight n u)</div>
<div> (number+unit n u))</div>
<div><br></div>
<div id="mb-reply">(: +/weight : Weight Weight -> Weight)</div>
<div id="mb-reply">;; something something needs unit conversion</div>
<div>(define (+/weight w1 w2)</div>
<div> (number+unit (+ (number+unit-amount w1)</div>
<div> (number+unit-amount w1))</div>
<div> (number+unit-unit w1)))</div>
<div><br></div>
<div>(+/weight (make-weight 1 'kg) (make-weight 1 'kg))</div>
</div></span><div class="mailbox_signature"><br></div>
<br><br><div class="gmail_quote"><p>On Sun, Sep 28, 2014 at 11:03 AM, Alexander D. Knauth <span dir="ltr"><<a href="mailto:alexander@knauth.org" target="_blank">alexander@knauth.org</a>></span> wrote:<br></p><blockquote class="gmail_quote" style="margin: 0px 0px 0px 0.8ex; border-left-width: 1px; border-left-color: rgb(204, 204, 204); border-left-style: solid; padding-left: 1ex; position: static; z-index: auto;"><p>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.
<br>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.
<br><br>On Sep 28, 2014, at 11:48 AM, Sam Tobin-Hochstadt <<a href="mailto:samth@cs.indiana.edu">samth@cs.indiana.edu</a>> wrote:
<br><br>> Why not do this with the type, instead of making this polymorphic?
<br>>
<br>> Sam
<br>>
<br>> On Fri, Sep 26, 2014 at 7:35 PM, Alexander D. Knauth
<br>> <<a href="mailto:alexander@knauth.org">alexander@knauth.org</a>> wrote:
<br>>> Is it possible to have a struct that does certain things according to the
<br>>> guard?
<br>>> #lang typed/racket
<br>>>
<br>>> (struct (a) foo ([a : a]) #:transparent
<br>>> #:guard (lambda (a _)
<br>>> (unless (exact-integer? a)
<br>>> (error 'foo "expected Integer, given ~v" a))
<br>>> a))
<br>>>
<br>>> (ann (foo (ann 1 Any)) (foo Integer))
<br>>>
<br>>> (: x : (foo Any))
<br>>> (define x (foo 1))
<br>>>
<br>>> (ann (foo-a x) Integer)
<br>>>
<br>>> ;. Type Checker: Polymorphic function `foo1' could not be applied to
<br>>> arguments:
<br>>> ;Argument 1:
<br>>> ; Expected: a
<br>>> ; Given: Any
<br>>> ;
<br>>> ;Result type: (foo a)
<br>>> ;Expected result: (foo Integer)
<br>>> ; in: (foo (ann 1 Any))
<br>>> ;. Type Checker: Polymorphic function `foo-a' could not be applied to
<br>>> arguments:
<br>>> ;Argument 1:
<br>>> ; Expected: (foo a)
<br>>> ; Given: (foo Any)
<br>>> ;
<br>>> ;Result type: (a : ....)
<br>>> ;Expected result: Integer
<br>>> ; in: (foo-a x)
<br>>>
<br>>> On Sep 25, 2014, at 9:42 PM, Alexander D. Knauth <<a href="mailto:alexander@knauth.org">alexander@knauth.org</a>>
<br>>> wrote:
<br>>>
<br>>> What I’m trying to accomplish is something more like this:
<br>>> #lang typed/racket
<br>>>
<br>>> (require "dimensions.rkt")
<br>>>
<br>>> (struct (d) unit ([name : Any] [scalar : Positive-Real] [dimension : d])
<br>>> #:transparent
<br>>> #:guard (lambda (name scalar dimension _)
<br>>> (unless (dimension? dimension)
<br>>> (error 'unit "expected Dimension, given ~v" dimension))
<br>>> (values name scalar dimension)))
<br>>>
<br>>> (define-type (Unitof d) (unit d))
<br>>>
<br>>> (define-type Unit (Unitof Dimension))
<br>>>
<br>>> (define Unit? (make-predicate Unit))
<br>>>
<br>>> (define-type Unitish
<br>>> (U (Unitof Any)
<br>>> Dimension
<br>>> Positive-Real))
<br>>>
<br>>> (: ->unit : (All (d) (case-> [(Unitof d) -> (Unitof d)]
<br>>> [Unitish -> Unit])))
<br>>> (define (->unit u)
<br>>> (cond [(unit? u)
<br>>> (unless (Unit? u) ; this should never happen anyway because of the
<br>>> guard
<br>>> (error '->unit "expected (Unitof Dimension), given ~v" u))
<br>>> u]
<br>>> [(dimension? u) (unit u 1 u)]
<br>>> [(positive-real? u) (unit u u dimensionless-dimension)]))
<br>>>
<br>>>
<br>>> On Sep 25, 2014, at 6:19 PM, Sam Tobin-Hochstadt <<a href="mailto:samth@cs.indiana.edu">samth@cs.indiana.edu</a>>
<br>>> wrote:
<br>>>
<br>>> No, I don't think you can do this. Can you say more about what you're
<br>>> trying to accomplish?
<br>>>
<br>>> Sam
<br>>>
<br>>> On Thu, Sep 25, 2014 at 6:15 PM, Alexander D. Knauth
<br>>> <<a href="mailto:alexander@knauth.org">alexander@knauth.org</a>> wrote:
<br>>>
<br>>> Do any of you have any advice for getting a function like this to
<br>>> type-check?
<br>>> #lang typed/racket
<br>>>
<br>>> (: check-int : (All (a) (case-> [a -> a]
<br>>> [Any -> Integer])))
<br>>> (define (check-int int)
<br>>> (unless (exact-integer? int)
<br>>> (error 'check-int "expected Integer, given ~v" int))
<br>>> int)
<br>>>
<br>>> ;. Type Checker: type mismatch
<br>>> ; expected: a
<br>>> ; given: Integer in: int
<br>>>
<br>>>
<br>>>
<br>>> ____________________
<br>>> Racket Users list:
<br>>> <a href="http://lists.racket-lang.org/users">http://lists.racket-lang.org/users</a>
<br>>>
<br>>>
<br>>> ____________________
<br>>> Racket Users list:
<br>>> <a href="http://lists.racket-lang.org/users">http://lists.racket-lang.org/users</a>
<br>>>
<br>>>
<br><br><br>____________________
<br> Racket Users list:
<br> <a href="http://lists.racket-lang.org/users">http://lists.racket-lang.org/users</a>
<br></p></blockquote></div><br></blockquote></div><br></div>____________________<br> Racket Users list:<br> <a href="http://lists.racket-lang.org/users">http://lists.racket-lang.org/users</a><br></blockquote></div><br></div></blockquote></div><br></div></blockquote></div><br></div></blockquote></div><br></div></blockquote></div><br></body></html>