The Racket users mailing list ()

Neil Toronto | 22 Feb 21:51

TR disappearing types?

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

Neil ⊥
____________________
  Racket Users list:
  http://lists.racket-lang.org/users

headers

Sam Tobin-Hochstadt | 22 Feb 23:34

Re: TR disappearing types?

On Wed, Feb 22, 2012 at 3:51 PM, Neil Toronto <neil.toronto@...> 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@...

____________________

(Continue reading)

headers

Neil Toronto | 23 Feb 00:05

Re: 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.

(Continue reading)