Re: [racket-dev] A proposal for parametric opaque types in Typed Racket

2015-01-30 Thread Alexander D. Knauth

On Jan 30, 2015, at 3:59 PM, Alexis King lexi.lam...@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 alexan...@knauth.org wrote:
 
 
 On Jan 30, 2015, at 1:53 PM, Alexis King lexi.lam...@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 alexan...@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” 
 

Re: [racket-dev] A proposal for parametric opaque types in Typed Racket

2015-01-30 Thread Alexis King
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.

 On Jan 30, 2015, at 07:27, Alexander D. Knauth alexan...@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=viewpr=13626 
 http://bugs.racket-lang.org/query/?cmd=viewpr=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, 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 alexan...@knauth.org 
 mailto:alexan...@knauth.org wrote:
  
  
 On Jan 29, 2015, at 11:34 PM, Alexis King lexi.lam...@gmail.com 
 mailto:lexi.lam...@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 

Re: [racket-dev] A proposal for parametric opaque types in Typed Racket

2015-01-30 Thread Alexander D. Knauth

On Jan 30, 2015, at 1:53 PM, Alexis King lexi.lam...@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 alexan...@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=viewpr=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 

[racket-dev] A proposal for parametric opaque types in Typed Racket

2015-01-29 Thread Alexis King
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


Re: [racket-dev] A proposal for parametric opaque types in Typed Racket

2015-01-29 Thread Alexis King
I think you’re reading too far into what I’m proposing, though I admit I 
probably didn’t give enough context. I’ve been talking with Sam about this 
issue on IRC, so he knows what I’m talking about, but I’ll try and clarify here.

This entire thing is just a fix for the problem described in Section 2 
http://lexi-lambda.github.io/racket-parametric-opaque-types/#(part._.Extending_parametricity_to_opaque_types).
 When using require/typed to import “opaque” types from untyped code, the 
imported types cannot be polymorphic. This entire proposal is simply a way to 
make that possible.

In Section 2.1, A is used in a number of places, but it is just a type 
parameter. See the typed struct definition in Section 1. A does not refer to a 
specific type but any type. Posn essentially becomes a new type combinator than 
can make new types by supplying it with any other type.

The other functions imported in Section 2.1 simply make use of Typed Racket’s 
polymorphic type utilities to make use of the fact that Posn is now a 
polymorphic type. The concepts here are simple. No semantics are being changed, 
it’s just extending parameterization to opaque types.

Sections 2.3 and 2.2, in contrast, are simply describing mechanisms for 
implementing the functionality outlined in 2.1.

Now to answer your points.

 - Should an A only be a base type like String or Symbol

A can by any type. It’s a type parameter. (Posn A) is like (Boxof A).

 - Do you mean to infer the type of the first thing put into the struct as the 
 exact type for everything else?

No, not really. Remember that Posn is an opaque type. TR has no idea it’s 
actually implemented as a struct. Perhaps the JSExpr example given in Section 3 
will help to illustrate that generality. This will just leverage the existing 
polymorphic type inference mechanisms TR already provides.

 - Would first class members prevent me from filling a struct with members 
 of (define-type (Option A) (U 'None (Some A))), where Some is a struct with 
 one field?

No, as I said, you can supply any type for A. By “first class member” of the 
type system, I simply meant that these types would have to be built-in to TR as 
a special case—they cannot be derived from the existing type constructs 
provided by TR. This is similar to how structure types are “first class” in 
TR—the struct form is “magical” and cannot be reimplemented in terms of other 
TR primitives.

I hope that helps to make things a little more clear.

 On Jan 29, 2015, at 19:44, Benjamin Greenman bl...@cornell.edu wrote:
 
 This has bothered me too, but I've realized that I was on the wrong track.
 
 The string a and symbol 'b are not different types. A struct (Foo a 'b), 
 or (list a 'b), is a homogeneous data structure of type (U String Symbol) 
 just like Alexander said. This really upsets me -- I like the Hindley Milner 
 world where the compiler warns me if I make a list [1, two] and forces me 
 to wrap the int and string into a new datatype. But Typed Racket is not HM.
 
 About the proposal, I'm confused about what the syntax in Section 2.1 should 
 do -- what is a first class member of Typed Racket's type system?
 - Should an A only be a base type like String or Symbol
 - Do you mean to infer the type of the first thing put into the struct as the 
 exact type for everything else?
 - Would first class members prevent me from filling a struct with members 
 of (define-type (Option A) (U 'None (Some A))), where Some is a struct with 
 one field?
 
 I totally agree that something needs fixing, but I'm not sure what.
 
 
 
 On Thu, Jan 29, 2015 at 10:13 PM, Alexis King lexi.lam...@gmail.com 
 mailto:lexi.lam...@gmail.com wrote:
 Or Any for that matter. I know. The fact that it could be literally anything 
 was sort of the point.
 
 On Jan 29, 2015, at 19:10, Alexander D. Knauth alexan...@knauth.org 
 mailto:alexan...@knauth.org wrote:
 
 Um, for this:
 (module 
 http://docs.racket-lang.org/reference/module.html#%28form._%28%28quote._~23~25kernel%29._module%29%29
  typed typed/racket/base
 (provide 
 http://docs.racket-lang.org/reference/require.html#%28form._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._provide%29%29
  (struct-out 
 http://docs.racket-lang.org/reference/require.html#%28form._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._struct-out%29%29
  Foo))
 (struct 
 http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._struct%29%29
  [A] Foo ([x : 
 http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._~3a%29%29
  A] [y : 
 http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._~3a%29%29
  A]) #:transparent))
 
 (Foo a 'b)
 Should be fine because Foo could be instantiated at the type (U String 
 Symbol).
 
 On Jan 29, 2015, at 9:25 PM, Alexis King lexi.lam...@gmail.com 
 mailto:lexi.lam...@gmail.com wrote:
 
 I 

Re: [racket-dev] A proposal for parametric opaque types in Typed Racket

2015-01-29 Thread Alexander D. Knauth

On Jan 29, 2015, at 11:34 PM, Alexis King lexi.lam...@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 
 knows nothing about 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. Using cast on an object of this type would 
 never fail (unless, of course, it didn’t actually satisfy the basic posn? 
 predicate), but it would possibly introduce failures in the future since it 
 would affect the contracts generated for posn-x and posn-y, for example.
 
 To make that more clear, casting a (Posn Real) to a (Posn String) would work 
 fine until you tried to call posn-x on 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 alexan...@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.lam...@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.
 
 After some further consideration, I’m interested in adding support to make 
 something like this possible, which 

Re: [racket-dev] A proposal for parametric opaque types in Typed Racket

2015-01-29 Thread Alexander D. Knauth
Um, for this:
(module typed typed/racket/base
(provide (struct-out Foo))
(struct [A] Foo ([x : A] [y : A]) #:transparent))

(Foo a 'b)
Should be fine because Foo could be instantiated at the type (U String Symbol).

On Jan 29, 2015, at 9:25 PM, Alexis King lexi.lam...@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.
 
 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/
 
 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

_
  Racket Developers list:
  http://lists.racket-lang.org/dev


Re: [racket-dev] A proposal for parametric opaque types in Typed Racket

2015-01-29 Thread Alexis King
 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 knows 
nothing about 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. Using cast on an object of this type would 
never fail (unless, of course, it didn’t actually satisfy the basic posn? 
predicate), but it would possibly introduce failures in the future since it 
would affect the contracts generated for posn-x and posn-y, for example.

To make that more clear, casting a (Posn Real) to a (Posn String) would work 
fine until you tried to call posn-x on the instance, in which case it would 
raise a contract error. Note that this isn’t really any different from casting 
mutable data types.

 On Jan 29, 2015, at 20:20, Alexander D. Knauth alexan...@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.lam...@gmail.com 
 mailto:lexi.lam...@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
 

_
  Racket Developers list:
  http://lists.racket-lang.org/dev


Re: [racket-dev] A proposal for parametric opaque types in Typed Racket

2015-01-29 Thread Benjamin Greenman
This has bothered me too, but I've realized that I was on the wrong track.

The string a and symbol 'b are not different types. A struct (Foo a
'b), or (list a 'b), is a homogeneous data structure of type (U String
Symbol) just like Alexander said. This really upsets me -- I like the
Hindley Milner world where the compiler warns me if I make a list [1,
two] and forces me to wrap the int and string into a new datatype. But
Typed Racket is not HM.

About the proposal, I'm confused about what the syntax in Section 2.1
should do -- what is a first class member of Typed Racket's type system?
- Should an A only be a base type like String or Symbol
- Do you mean to infer the type of the first thing put into the struct as
the exact type for everything else?
- Would first class members prevent me from filling a struct with members
of (define-type (Option A) (U 'None (Some A))), where Some is a struct
with one field?

I totally agree that something needs fixing, but I'm not sure what.



On Thu, Jan 29, 2015 at 10:13 PM, Alexis King lexi.lam...@gmail.com wrote:

 Or Any for that matter. I know. The fact that it could be literally
 anything was sort of the point.

 On Jan 29, 2015, at 19:10, Alexander D. Knauth alexan...@knauth.org
 wrote:

 Um, for this:
 (module
 http://docs.racket-lang.org/reference/module.html#%28form._%28%28quote._~23~25kernel%29._module%29%29
  typed typed/racket/base(provide
 http://docs.racket-lang.org/reference/require.html#%28form._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._provide%29%29
  (struct-out
 http://docs.racket-lang.org/reference/require.html#%28form._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._struct-out%29%29
  Foo))(struct
 http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._struct%29%29
  [A] Foo ([x :
 http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._~3a%29%29
  A] [y :
 http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._~3a%29%29
  A]) #:transparent))

 (Foo a 'b)
 Should be fine because Foo could be instantiated at the type (U String
 Symbol).

 On Jan 29, 2015, at 9:25 PM, Alexis King lexi.lam...@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/

 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




 _
   Racket Developers list:
   http://lists.racket-lang.org/dev


_
  Racket Developers list:
  http://lists.racket-lang.org/dev


Re: [racket-dev] A proposal for parametric opaque types in Typed Racket

2015-01-29 Thread Alexander D. Knauth
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.lam...@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.
 
 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/
 
 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

_
  Racket Developers list:
  http://lists.racket-lang.org/dev


Re: [racket-dev] A proposal for parametric opaque types in Typed Racket

2015-01-29 Thread Alexis King
Or Any for that matter. I know. The fact that it could be literally anything 
was sort of the point.

 On Jan 29, 2015, at 19:10, Alexander D. Knauth alexan...@knauth.org wrote:
 
 Um, for this:
 (module 
 http://docs.racket-lang.org/reference/module.html#%28form._%28%28quote._~23~25kernel%29._module%29%29
  typed typed/racket/base
 (provide 
 http://docs.racket-lang.org/reference/require.html#%28form._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._provide%29%29
  (struct-out 
 http://docs.racket-lang.org/reference/require.html#%28form._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._struct-out%29%29
  Foo))
 (struct 
 http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._struct%29%29
  [A] Foo ([x : 
 http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._~3a%29%29
  A] [y : 
 http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._~3a%29%29
  A]) #:transparent))
 
 (Foo a 'b)
 Should be fine because Foo could be instantiated at the type (U String 
 Symbol).
 
 On Jan 29, 2015, at 9:25 PM, Alexis King lexi.lam...@gmail.com 
 mailto:lexi.lam...@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
 

_
  Racket Developers list:
  http://lists.racket-lang.org/dev


Re: [racket-dev] A proposal for parametric opaque types in Typed Racket

2015-01-29 Thread Alexis King
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.

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.

(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.)

 On Jan 29, 2015, at 20:50, Alexander D. Knauth alexan...@knauth.org wrote:
 
 
 On Jan 29, 2015, at 11:34 PM, Alexis King lexi.lam...@gmail.com 
 mailto:lexi.lam...@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 
 knows nothing about 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. Using cast on an object of this type would 
 never fail (unless, of course, it didn’t actually satisfy the basic posn? 
 predicate), but it would possibly introduce failures in the future since it 
 would affect the contracts generated for posn-x and posn-y, for example.
 
 To make that more clear, casting a (Posn Real) to a (Posn String) would work 
 fine until you tried to call posn-x on 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 alexan...@knauth.org 
 mailto:alexan...@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