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

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.lambda at 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 <alexander at 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.lambda at 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/dev/archive/attachments/20150129/1a5d253a/attachment-0001.html>