[racket] TR disappearing types?

On 02/22/2012 03:34 PM, Sam Tobin-Hochstadt wrote:
> 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?

Oh, that's what they're called. I should have remembered them from crazy 
Haskell metaprogramming.

Would changing it speed up type-checking? :)

Anyway, I've worked around it. Here's how:


#lang typed/racket

(struct: (a) Foo ([rep : (-> a)]))

(: make-foo (All (a) (a ->  (Foo a))))
(define (make-foo x)
   (Foo (λ () (error 'make-foo "phantom (woo!)"))))

;; TR appropriately barfs on this:
(ann (make-foo 1) : (Foo String))


Neil ⊥