On 02/22/2012 03:34 PM, Sam Tobin-Hochstadt wrote:
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?
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 ⊥
____________________
Racket Users list:
http://lists.racket-lang.org/users
