On Wed, Feb 22, 2012 at 3:51 PM, Neil Toronto <neil.toro...@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 sa...@ccs.neu.edu ____________________ Racket Users list: http://lists.racket-lang.org/users
