<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div>I just realized that typed racket seems to ignore the guard anyway, so I could do something like this and convince the type-checker that any value I want has any type that I want:</div><div><div><br></div><div>(struct (a) foo ([a : a])</div><div> #:guard (lambda (a _) "this value"))</div><div><br></div><div>(: x : (foo 1))</div><div>(define x (foo 1))</div></div><div><br></div><div><div>> (foo-a x)</div><div>- : Integer [more precisely: One]</div><div>"this value”</div></div><div><br></div><br><div><div>On Sep 28, 2014, at 10:41 PM, Benjamin Greenman <<a href="mailto:blg59@cornell.edu">blg59@cornell.edu</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div dir="ltr">I was able to get something very similar to your example program to compile.<div><br></div><div><div><font face="courier new, monospace">(struct (a) foo ([a : a]) #:transparent </font></div><div><font face="courier new, monospace"> #:guard (lambda (a _)</font></div><div><font face="courier new, monospace"> (define a* a) ;; a* not "polluted" by occurrence typing</font></div><div><font face="courier new, monospace"> (unless (exact-integer? a) </font></div><div><font face="courier new, monospace"> (error 'foo "expected Integer, given ~v" a)) </font></div><div><font face="courier new, monospace"> a*)) ;; we return a value of type a, so the typechecker is happy</font></div></div><div><br></div><div>From here, you can safely cast a foo-a into an Integer. It's not type safe to ann because we (deliberately) don't have the occurrence typing information, but we the programmers can be sure that the casts will never fail.</div><div><br></div><div><font face="courier new, monospace">(cast (foo (ann 1 Any)) (foo Integer))<br></font></div><div><font face="courier new, monospace">> (foo 1)</font></div><div><br></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Sep 28, 2014 at 10:29 PM, Matthias Felleisen <span dir="ltr"><<a href="mailto:matthias@ccs.neu.edu" target="_blank">matthias@ccs.neu.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><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><div class="h5"><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><blockquote type="cite"><div style="word-wrap:break-word"><div><br></div><br><div><div>On Sep 28, 2014, at 8:25 PM, Matthias Felleisen <<a href="mailto:matthias@ccs.neu.edu" target="_blank">matthias@ccs.neu.edu</a>> wrote:</div><br><blockquote type="cite"><div style="word-wrap:break-word"><div><span style="white-space:pre-wrap"> </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"><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><blockquote type="cite"><div style="word-wrap:break-word"><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" target="_blank">matthias@ccs.neu.edu</a>> wrote:</div><br><blockquote type="cite"><div style="word-wrap:break-word"><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><blockquote type="cite"><div style="word-wrap:break-word"><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" target="_blank">spencerflorence@gmail.com</a>> wrote:</div><br><blockquote type="cite">
<span><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>(: +/weight : Weight Weight -> Weight)</div>
<div>;; 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><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"><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" target="_blank">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" target="_blank">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" target="_blank">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" target="_blank">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" target="_blank">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" target="_blank">http://lists.racket-lang.org/users</a>
<br>>>
<br>>>
<br>>> ____________________
<br>>> Racket Users list:
<br>>> <a href="http://lists.racket-lang.org/users" target="_blank">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" target="_blank">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" target="_blank">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></div></div></div></blockquote></div><br></div>
</blockquote></div><br></body></html>