[racket] TR disappearing types?

From: Sam Tobin-Hochstadt (samth at ccs.neu.edu)
Date: Wed Feb 22 17:34:19 EST 2012

On Wed, Feb 22, 2012 at 3:51 PM, Neil Toronto <neil.toronto at gmail.com> wrote:
> The following program types without trouble:
> #lang typed/racket
> (struct: (a) Foo ())
> (: make-foo (All (a) (a -> (Foo a))))
> (define (make-foo x)
>  (Foo))
> (ann (make-foo 1) : (Foo String))
> It doesn't seem like it should, though. If this is the right behavior, is
> there a way to get a `Foo' parameterized on type `a' without actually
> storing the value? I'm trying to use TR to check programs that can't
> actually be run (i.e. written in a lambda calculus extended with uncountable
> sets).

What you're seeing is that TR currently implements type instantiation
with substitution, and so encodings like 'phantom types' don't work.
This isn't a soundness hole, but it's something that I'm willing to
change if there are programs you'd like to write that you can't.  Can
you give a more complete example?
sam th
samth at ccs.neu.edu

Posted on the users mailing list.