[prev in list] [next in list] [prev in thread] [next in thread]
List: racket-dev
Subject: Re: [racket-dev] A proposal for parametric opaque types in Typed Racket
From: Alexis King <lexi.lambda () gmail ! com>
Date: 2015-01-31 5:33:31
Message-ID: 5AC61E9B-6266-4D9E-8D75-B1FEFF46348D () gmail ! com
[Download RAW message or body]
[Attachment #2 (multipart/alternative)]
Okay, now I see what you're saying. That's a reasonable point, and it's worth \
considering. Thanks for bearing with me.
> On Jan 30, 2015, at 13:24, Alexander D. Knauth <alexander@knauth.org> wrote:
>
>
> On Jan 30, 2015, at 3:59 PM, Alexis King <lexi.lambda@gmail.com \
> <mailto:lexi.lambda@gmail.com>> wrote:
> > No, the typechecker can't make any assumptions about the results of opaque types. \
> > If you explicitly instantiate a Posn with the type Real, the typechecker should \
> > only guarantee the result will be Real. Annotate the type as (U 1 2), though, and \
> > obviously it would need to ensure that remains invariant.
>
> How about this program:
> untyped.rkt:
> #lang racket
> (provide (all-defined-out))
> (define (make-posn x y) (list 3 y)) ; bad
> typed.rkt:
> #lang typed/racket
> ; make Posn parametric
> (define-type (Posn X Y) (List X Y))
> (require/typed "untyped.rkt"
> [make-posn (All (X Y) X Y -> (Posn X Y))])
> (: p : (Posn Real Real))
> (define p (make-posn 1 2))
> This gives this error:
> . . make-posn: broke its contract
> promised: X3
> produced: 3
> in: the car of
> the range of
> (parametric->/c
> (X3 Y4)
> (->*
> (X3 Y4)
> ()
> (values (cons/c X3 (cons/c Y4 g6)))))
> contract from: (interface for make-posn)
> blaming: (interface for make-posn)
> (assuming the contract is correct)
> at: …./typed.rkt:5.16
>
> I think it's a good thing that it checks that it actually gives you the value that \
> you gave it, and not just something like 3 even if it happens to match the type you \
> want. And I think parametric opaque types should behave in a similar way, and to \
> do that you would need the opaque value to be wrapped in another opaque structure, \
> which would store either the contracts or the set of values that would pass the \
> contracts or something like that.
> >
> > > On Jan 30, 2015, at 12:30, Alexander D. Knauth <alexander@knauth.org \
> > > <mailto:alexander@knauth.org>> wrote:
> > >
> > > On Jan 30, 2015, at 1:53 PM, Alexis King <lexi.lambda@gmail.com \
> > > <mailto:lexi.lambda@gmail.com>> wrote:
> > > > No, it doesn't need to be wrapped in an opaque structure. Wrapping it in an \
> > > > opaque structure would add a layer of indirection for absolutely no gain. \
> > > > Remember, the value itself is already, by definition, opaque. The only way \
> > > > typed code can manipulate the value is by passing it to other functions \
> > > > imported via require/typed.
> > > > This means that contracts only need to be generated wherever those functions \
> > > > are called. This can be done without wrapping or unwrapping anything because \
> > > > all the information required to generate those contracts is known at \
> > > > expansion-time. The typechecker simply needs to insert the relevant contracts \
> > > > at the relevant locations.
> > >
> > > Imagine a program like this:
> > > #lang typed/racket
> > > (require typed/lang/posn)
> > > (: p : (Posn Real Real)) ; I'm assuming Posn is parametric over 2 tvars, not 1
> > > (define p (posn 1 2))
> > > (: x : Real)
> > > (define x (posn-x p))
> > > As far as the type checker would check, it would check that the result of \
> > > posn-x is a Real, but I think that the runtime contract it should also check \
> > > that it returns 1, because posn could have been instantiated as (Posn 1 2). \
> > > #lang typed/racket (require typed/lang/posn/mutable) ; like typed/lang/posn, \
> > > but providing mutation too (: p : (Posn Real Real))
> > > (define p (posn 1 2))
> > > (: x : Real)
> > > (define x (posn-x p))
> > > (set-posn-x! p 3)
> > > (: x2 : Real)
> > > (define x2 (posn-x p))
> > > Here, even though the type checker only cares that it's a number, it should \
> > > check that x2 definition returns either 1 or 3, since both were provided as x \
> > > values for the posn p.
> > > For it to keep track of these at runtime, (and it would have to be runtime) the \
> > > contracts would have to be with the actual posn value in an opaque structure, \
> > > which would have contracts sort of like (new-∀/c) that would check these \
> > > things, although I don't think it would have to wrap the inner values, but just \
> > > record them so that when posn-x is called on one of these things, it checks \
> > > that it was one of the values that was passed in to either a constructor or \
> > > setter function.
> > > > > On Jan 30, 2015, at 07:27, Alexander D. Knauth <alexander@knauth.org \
> > > > > <mailto:alexander@knauth.org>> wrote:
> > > > > On Thu, Jan 29, 2015, at 09:03 PM, Alexis King wrote:
> > > > > > It isn't wrapped in an opaque structure. That wasn't a part of my \
> > > > > > proposal, and while I didn't think of it until you brought it up, I still \
> > > > > > think it's unnecessary and doesn't add any convenience.
> > > > >
> > > > > I think the opaque structures would be necessary for the kind of "sharing \
> > > > > wrappers between functions" that you describe just before section 2.1, \
> > > > > except that instead of the sub-values being wrapped on the untyped side, \
> > > > > the whole thing is wrapped on the typed side, and there is a contract that \
> > > > > wraps it and unwraps it when it goes from untyped to typed and back.
> > > > > For parametric types, they have to also work if the type was constrained to \
> > > > > the exact set of values that were provided, which means that if you provide \
> > > > > two numbers, say 1 and 2, it has to return a posn with not just any two \
> > > > > numbers, but values of the type (U 1 2), since A could have been \
> > > > > constrained to (U 1 2). So it has to be wrapped somehow, and I think \
> > > > > wrapping it on the typed side makes more sense.
> > > > > > Perhaps I'm not understanding you properly, but your "one-length string" \
> > > > > > idea sounds like it has little to do with this opaque type problem and \
> > > > > > more to do with the fact that you want refinement types in Typed Racket. \
> > > > > > I do, too! But I don't think hacking the opaque type system is going to \
> > > > > > help you with that.
> > > > >
> > > > > Well, yeah, refinement types would be the "real" solution for this \
> > > > > particular example, but if I do want to constrain it to strings of length \
> > > > > 1, opaque types are the only option for now, and they actually work fine. \
> > > > > My point was you couldn't do this type of thing with the opaque structures \
> > > > > and you would probably get weird errors if you tried. (See below because \
> > > > > there might be a solution?)
> > > > > > (Also, as for the box example, I'm actually a little surprised that \
> > > > > > doesn't contract error. Seems like a bug to me, but perhaps I'm missing \
> > > > > > some idiosyncrasies of the type system. Either way, it's precisely that \
> > > > > > kind of craziness I was referring to when I compared casting parametric \
> > > > > > opaque types to casting mutable types.)
> > > > >
> > > > > There is a bug report for it here, and the solution proposed by Sam \
> > > > > Tobin-Hochstadt would be for cast to generate 2 contracts, one for the \
> > > > > original type, one for the new type, but that never got implemented. \
> > > > > http://bugs.racket-lang.org/query/?cmd=view&pr=13626 \
> > > > > <http://bugs.racket-lang.org/query/?cmd=view&pr=13626>
> > > > > Actually now that I think about it the two-contract solution might be able \
> > > > > to solve the previous problem, since the original contract could unwrap the \
> > > > > value before it is passed to the new contract? I'm not sure though. The \
> > > > > value inside the cast would be from the typed side, then it is passed \
> > > > > through the orig contract as if it were going to the typed side,
> > >
> > > This was a typo, I meant to say "as if it were going to the untyped side"
> > >
> > > > > which would unwrap it, and then that unwrapped value would be passed to the \
> > > > > new contract as if it were flowing from the untyped side to the typed side. \
> > > > >
> > > > > >
> > > > > > > On Jan 29, 2015, at 20:50, Alexander D. Knauth <alexander@knauth.org \
> > > > > > > <mailto:alexander@knauth.org>> wrote:
> > > > > > >
> > > > > > > On Jan 29, 2015, at 11:34 PM, Alexis King <lexi.lambda@gmail.com \
> > > > > > > <mailto:lexi.lambda@gmail.com>> wrote:
> > > > > > > > > But the problem is that if it's an opaque type then it can't unwrap \
> > > > > > > > > it once the value is returned from make-posn.
> > > > > > > >
> > > > > > > > Yes, that's precisely the problem. Your point about implementing \
> > > > > > > > everything as single-valued structs on the typed side is an \
> > > > > > > > interesting one, though I don't think it ultimately solves any \
> > > > > > > > problems. The fact that the typed side knowsnothingabout the contents \
> > > > > > > > of the value is what makes this such a tricky problem.
> > > > > > > > As for this:
> > > > > > > >
> > > > > > > > > But then you couldn't do any operations on it except those that you \
> > > > > > > > > use import with require/typed, right?
> > > > > > > >
> > > > > > > > That's completely correct. That's why it's "opaque."
> > > > > > > >
> > > > > > > > > And what happens if you use cast on one of these things?
> > > > > > > >
> > > > > > > > That's a little more interesting. Usingcaston an object of this type \
> > > > > > > > would never fail (unless, of course, it didn't actually satisfy the \
> > > > > > > > basicposn?predicate), but it would possibly introduce failures in the \
> > > > > > > > future since it would affect the contracts generated \
> > > > > > > > forposn-xandposn-y, for example.
> > > > > > > > To make that more clear, casting a(Posn Real)to a(Posn String)would \
> > > > > > > > work fine until you tried to callposn-xon the instance, in which case \
> > > > > > > > it would raise a contract error. Note that this isn't really any \
> > > > > > > > different from casting mutable data types.
> > > > > > >
> > > > > > > But if it were wrapped in an opaque structure, then that structure \
> > > > > > > wouldn't satisfy the posn? predicate, unless of course the posn? \
> > > > > > > predicate has a contract that unwraps it. So all of the operations on \
> > > > > > > it would have to have contracts that would unwrap it. This might \
> > > > > > > actually make sense if the type is meant to be actually opaque, but if \
> > > > > > > it's an opaque type that represents a normal non-opaque value, then it \
> > > > > > > will still work as an opaque type, but it won't be a normal non-opaque \
> > > > > > > value anymore on the typed side.
> > > > > > > But the reason I asked about cast was because normally I can use cast \
> > > > > > > with a value that has an opaque type, but it's wrapped on the typed \
> > > > > > > side in this opaque structure, then the contracts on the cast would see \
> > > > > > > this opaque structure instead of the actual value.
> > > > > > > I'm thinking of an opaque typed representing a string with length 1, \
> > > > > > > which I can use as long as I use either (cast x String) or (assert x \
> > > > > > > string?) whenever I pass it to a string operation. But if it were an \
> > > > > > > opaque type, I don't think I could do that. There could be a \
> > > > > > > 1string->string function that could take one of these 1strings and \
> > > > > > > convert it to a string, but that seems like it should be unnecessary, \
> > > > > > > but made necessary by this opaque structure thing.
> > > > > > > And for "this isn't really any different from casting mutable data \
> > > > > > > types," look at this: #lang typed/racket
> > > > > > > (: b : (Boxof Number))
> > > > > > > (define b (box 1))
> > > > > > > (set-box! (cast b (Boxof (U Number String))) "I am a string")
> > > > > > > (ann (unbox b) Number) ;"I am a string" ; not a contract error
> > > > > > >
> > > > > > >
> > > > > > > >
> > > > > > > > > On Jan 29, 2015, at 20:20, Alexander D. Knauth \
> > > > > > > > > <alexander@knauth.org <mailto:alexander@knauth.org>> wrote:
> > > > > > > > > Furthermore, even if the wrappers were shared between functions, \
> > > > > > > > > untyped code would recieved wrapped values, which would render them \
> > > > > > > > > quite useless.
> > > > > > > > > If it's not an opaque type, but something like a list, then this \
> > > > > > > > > works, and the untyped code receiving wrapped values isn't a \
> > > > > > > > > problem here: #lang typed/racket
> > > > > > > > > ; make Posn parametric
> > > > > > > > > (define-type (Posn A) (List A A))
> > > > > > > > > (provide Posn)
> > > > > > > > > (require/typed/provide
> > > > > > > > > "untyped.rkt"
> > > > > > > > > [make-posn (All (A) A A -> (Posn A))]
> > > > > > > > > [posn-x (All (A) (Posn A) -> A)]
> > > > > > > > > [posn-y (All (A) (Posn A) -> A)]
> > > > > > > > > [real-posn? [(Posn Any) -> Boolean]])
> > > > > > > > > > (define p (make-posn 1 2))
> > > > > > > > > (make-posn #<A6> #<A6>) ; a printf that I put in make-posn from \
> > > > > > > > > "untyped.rkt"
> > > > > > > > > > p
> > > > > > > > > - : (Listof Positive-Byte) [more precisely: (List Positive-Byte \
> > > > > > > > > Positive-Byte)] '(1 2) ; unwrapped
> > > > > > > > > > (posn-x p)
> > > > > > > > > - : Integer [more precisely: Positive-Byte]
> > > > > > > > > 1
> > > > > > > > > > (posn-y p)
> > > > > > > > > - : Integer [more precisely: Positive-Byte]
> > > > > > > > > 2
> > > > > > > > > > (real-posn? p)
> > > > > > > > > - : Boolean
> > > > > > > > > #t
> > > > > > > > >
> > > > > > > > > Even though for a short time it's wrapped, it's unwrapped as soon \
> > > > > > > > > as make-posn returns, and then after that if it flows into untyped \
> > > > > > > > > code again it's not wrapped and functions like real-posn? work \
> > > > > > > > > fine.
> > > > > > > > > But the problem is that if it's an opaque type then it can't unwrap \
> > > > > > > > > it once the value is returned from make-posn.
> > > > > > > > > And I don't think parametric opaque types could solve this unless \
> > > > > > > > > all posns themselves were wrapped with an opaque struct on the \
> > > > > > > > > typed side, which I guess does make sense now that I think about \
> > > > > > > > > it. But then you couldn't do any operations on it except those \
> > > > > > > > > that you use import with require/typed, right? Or not? And what \
> > > > > > > > > happens if you use cast on one of these things?
> > > > > > > > >
> > > > > > > > > On Jan 29, 2015, at 9:25 PM, Alexis King <lexi.lambda@gmail.com \
> > > > > > > > > <mailto:lexi.lambda@gmail.com>> wrote:
> > > > > > > > > > I recently ran into a problem in which opaque types (types \
> > > > > > > > > > imported from untyped code) cannot by parameterized by Typed \
> > > > > > > > > > Racket. I initially encountered this problem in my attempt to \
> > > > > > > > > > port 2htdp/image to TR \
> > > > > > > > > > <https://github.com/lexi-lambda/racket-2htdp-typed/issues/1>.
> > > > > > > > > > After some further consideration, I'm interested in adding \
> > > > > > > > > > support to make something like this possible, which would \
> > > > > > > > > > certainly have additional benefits beyond this specific use-case. \
> > > > > > > > > > I've outlined my proposal here: \
> > > > > > > > > > http://lexi-lambda.github.io/racket-parametric-opaque-types/ \
> > > > > > > > > > <http://lexi-lambda.github.io/racket-parametric-opaque-types/>
> > > > > > > > > > Any feedback, suggestions, or advice would be appreciated, \
> > > > > > > > > > especially from those who are familiar with Typed Racket's \
> > > > > > > > > > internals.
> > > > > > > > > > Thank you,
> > > > > > > > > > Alexis
> > > > > > > > > > _________________________
> > > > > > > > > > Racket Developers list:
> > > > > > > > > > http://lists.racket-lang.org/dev \
> > > > > > > > > > <http://lists.racket-lang.org/dev>
>
[Attachment #5 (unknown)]
<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;" class=""><div class="">Okay, now I see what \
you're saying. That's a reasonable point, and it's worth considering. Thanks for \
bearing with me.</div><br class=""><div><blockquote type="cite" class=""><div \
class="">On Jan 30, 2015, at 13:24, Alexander D. Knauth <<a \
href="mailto:alexander@knauth.org" class="">alexander@knauth.org</a>> \
wrote:</div><br class="Apple-interchange-newline"><div class=""><meta \
http-equiv="Content-Type" content="text/html charset=utf-8" class=""><div \
style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: \
after-white-space;" class=""><br class=""><div class=""><div class="">On Jan 30, \
2015, at 3:59 PM, Alexis King <<a href="mailto:lexi.lambda@gmail.com" \
class="">lexi.lambda@gmail.com</a>> wrote:</div><br \
class="Apple-interchange-newline"><blockquote type="cite" class=""><meta \
http-equiv="Content-Type" content="text/html charset=utf-8" class=""><div \
style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: \
after-white-space;" class=""><div class="">No, the typechecker can't make any \
assumptions about the results of opaque types. If you explicitly instantiate a <font \
face="Courier" class="">Posn</font> with the type <font face="Courier" \
class="">Real</font>, the typechecker should only guarantee the result will be <font \
face="Courier" class="">Real</font>. Annotate the type as <font face="Courier" \
class="">(U 1 2)</font>, though, and obviously it would need to ensure that remains \
invariant.</div></div></blockquote><div class=""><br class=""></div><div class="">How \
about this program:</div><div class="">untyped.rkt:</div><div class=""><div \
class="">#lang racket</div><div class="">(provide (all-defined-out))</div><div \
class="">(define (make-posn x y) (list 3 y)) ; bad</div></div><div \
class="">typed.rkt:</div><div class=""><div class="">#lang typed/racket</div><div \
class=""><div class="">; make Posn parametric</div><div class="">(define-type (Posn X \
Y) (List X Y))</div><div class="">(require/typed "untyped.rkt"</div><div \
class=""> [make-posn (All (X Y) \
X Y -> (Posn X Y))])</div><div class="">(: p : (Posn Real Real))</div><div \
class="">(define p (make-posn 1 2))</div></div></div><div class="">This gives this \
error:</div><div class=""><div class="">. . make-posn: broke its contract</div><div \
class=""> promised: X3</div><div class=""> produced: 3</div><div \
class=""> in: the car of</div><div class=""> the range \
of</div><div class=""> (parametric->/c</div><div \
class=""> (X3 Y4)</div><div class=""> \
(->*</div><div class=""> (X3 Y4)</div><div \
class=""> ()</div><div class=""> \
(values (cons/c X3 (cons/c Y4 g6)))))</div><div class=""> contract from: \
(interface for make-posn)</div><div class=""> blaming: (interface for \
make-posn)</div><div class=""> (assuming the contract is \
correct)</div><div class=""> at: …./typed.rkt:5.16</div><div class=""><br \
class=""></div><div class="">I think it's a good thing that it checks that it \
actually gives you the value that you gave it, and not just something like 3 even if \
it happens to match the type you want. And I think parametric opaque types \
should behave in a similar way, and to do that you would need the opaque value to be \
wrapped in another opaque structure, which would store either the contracts or the \
set of values that would pass the contracts or something like that. \
</div></div><br class=""><blockquote type="cite" class=""><div \
style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: \
after-white-space;" class=""><br class=""><div class=""><blockquote type="cite" \
class=""><div class="">On Jan 30, 2015, at 12:30, Alexander D. Knauth <<a \
href="mailto:alexander@knauth.org" class="">alexander@knauth.org</a>> \
wrote:</div><br class="Apple-interchange-newline"><div class=""><div \
style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: \
normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: \
auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; \
widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br \
class="Apple-interchange-newline">On Jan 30, 2015, at 1:53 PM, Alexis King <<a \
href="mailto:lexi.lambda@gmail.com" class="">lexi.lambda@gmail.com</a>> \
wrote:</div><br class="Apple-interchange-newline" style="font-family: Helvetica; \
font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; \
letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; \
text-indent: 0px; text-transform: none; white-space: normal; widows: auto; \
word-spacing: 0px; -webkit-text-stroke-width: 0px;"><blockquote type="cite" \
style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: \
normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: \
auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; \
widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><div \
class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: \
after-white-space;"><div class="">No, it doesn't need to be wrapped in an opaque \
structure. Wrapping it in an opaque structure would add a layer of indirection for \
absolutely no gain. Remember, the value itself is already, by definition,<span \
class="Apple-converted-space"> </span><i class="">opaque</i>. The only way typed \
code can manipulate the value is by passing it to other functions imported via<span \
class="Apple-converted-space"> </span><font face="Courier" \
class="">require/typed</font>.</div><div class=""><br class=""></div><div \
class="">This means that contracts only need to be generated wherever those functions \
are called. This can be done without wrapping or unwrapping anything because all the \
information required to generate those contracts is known at expansion-time. The \
typechecker simply needs to insert the relevant contracts at the relevant \
locations.</div></div></blockquote><div style="font-family: Helvetica; font-size: \
12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: \
normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; \
text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; \
-webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: \
Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: \
normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: \
start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; \
word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">Imagine a program like \
this:</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; \
font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: \
normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; \
white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: \
0px;" class="">#lang typed/racket</div><div style="font-family: Helvetica; font-size: \
12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: \
normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; \
text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; \
-webkit-text-stroke-width: 0px;" class="">(require typed/lang/posn)</div><div \
style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: \
normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: \
auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; \
widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">(: p : \
(Posn Real Real)) ; I'm assuming Posn is parametric over 2 tvars, not 1</div><div \
style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: \
normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: \
auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; \
widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">(define p \
(posn 1 2))</div><div style="font-family: Helvetica; font-size: 12px; font-style: \
normal; font-variant: normal; font-weight: normal; letter-spacing: normal; \
line-height: normal; orphans: auto; text-align: start; text-indent: 0px; \
text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; \
-webkit-text-stroke-width: 0px;" class="">(: x : Real)</div><div style="font-family: \
Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: \
normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: \
start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; \
word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">(define x (posn-x \
p))</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; \
font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: \
normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; \
white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: \
0px;" class="">As far as the type checker would check, it would check that the result \
of posn-x is a Real, but I think that the runtime contract it should also check that \
it returns 1, because posn could have been instantiated as (Posn 1 2).</div><div \
style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: \
normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: \
auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; \
widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">#lang \
typed/racket</div><div style="font-family: Helvetica; font-size: 12px; font-style: \
normal; font-variant: normal; font-weight: normal; letter-spacing: normal; \
line-height: normal; orphans: auto; text-align: start; text-indent: 0px; \
text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; \
-webkit-text-stroke-width: 0px;" class="">(require typed/lang/posn/mutable) ; like \
typed/lang/posn, but providing mutation too</div><div style="font-family: Helvetica; \
font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; \
letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; \
text-indent: 0px; text-transform: none; white-space: normal; widows: auto; \
word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">(: p : (Posn Real \
Real))</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; \
font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: \
normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; \
white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: \
0px;" class="">(define p (posn 1 2))</div><div style="font-family: Helvetica; \
font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; \
letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; \
text-indent: 0px; text-transform: none; white-space: normal; widows: auto; \
word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">(: x : Real)</div><div \
style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: \
normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: \
auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; \
widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">(define x \
(posn-x p))</div><div style="font-family: Helvetica; font-size: 12px; font-style: \
normal; font-variant: normal; font-weight: normal; letter-spacing: normal; \
line-height: normal; orphans: auto; text-align: start; text-indent: 0px; \
text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; \
-webkit-text-stroke-width: 0px;" class="">(set-posn-x! p 3)</div><div \
style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: \
normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: \
auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; \
widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">(: x2 : \
Real)</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; \
font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: \
normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; \
white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: \
0px;" class="">(define x2 (posn-x p))</div><div style="font-family: Helvetica; \
font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; \
letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; \
text-indent: 0px; text-transform: none; white-space: normal; widows: auto; \
word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">Here, even though the \
type checker only cares that it's a number, it should check that x2 definition \
returns either 1 or 3, since both were provided as x values for the posn p.</div><div \
style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: \
normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: \
auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; \
widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br \
class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: \
normal; font-variant: normal; font-weight: normal; letter-spacing: normal; \
line-height: normal; orphans: auto; text-align: start; text-indent: 0px; \
text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; \
-webkit-text-stroke-width: 0px;" class="">For it to keep track of these at runtime, \
(and it would have to be runtime) the contracts would have to be with the actual posn \
value in an opaque structure, which would have contracts sort of like (new-∀/c) \
that would check these things, although I don't think it would have to wrap the inner \
values, but just record them so that when posn-x is called on one of these things, it \
checks that it was one of the values that was passed in to either a constructor or \
setter function. </div><br style="font-family: Helvetica; font-size: 12px; \
font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: \
normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; \
text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; \
-webkit-text-stroke-width: 0px;" class=""><blockquote type="cite" style="font-family: \
Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: \
normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: \
start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; \
word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><div class="" \
style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: \
after-white-space;"><div class=""><blockquote type="cite" class=""><div class="">On \
Jan 30, 2015, at 07:27, Alexander D. Knauth <<a href="mailto:alexander@knauth.org" \
class="">alexander@knauth.org</a>> wrote:</div><div class=""><div class=""><div \
class=""> </div><div class="">On Thu, Jan 29, 2015, at 09:03 PM, Alexis King \
wrote:<br class=""></div><blockquote type="cite" class=""><div class="">It isn't \
wrapped in an opaque structure. That wasn't a part of my proposal, and while I didn't \
_________________________
Racket Developers list:
http://lists.racket-lang.org/dev
[prev in list] [next in list] [prev in thread] [next in thread]
Configure |
About |
News |
Add a list |
Sponsored by KoreLogic