On 11/19/10 10:05 PM, Ryan Ingram wrote:
Not exactly; in the phantom type case, the two sets ARE disjoint in a way; there are no objects that are both Foo Int and Foo Bool (although there may be objects of type forall a. Foo a -- more on that later). Whereas the type keyword really creates two names for the same set.
Only "in a way". I'd say there certainly are values that inhabit multiple types. I'll write one right now: []. Oh, here's another: Nothing. Or even: return. Sure, these values are typically the same ones as the ones inhabiting universal types, but there's nothing terribly strange about values inhabiting multiple types. If we were strictly adhering to System F then we would have to explicitly distinguish between Nothing, Nothing @Int, and Nothing @Bool so we wouldn't have the same term belonging to multiple types. But *we don't* strictly adhere to System F, and generally speaking we like to pretend we're in Curry-style languages even when the implementation is Church-style behind the scenes. There are some nice metatheoretical benefits to using Church-style formalisms, but that doesn't mean Church was any more "right" than Curry. If Church were really "right" then we wouldn't care so much about doing type inference or about making it require as few annotations as possible, since the "right" thing would be to annotate the terms in the first place. It's mostly a philosophical issue (albeit with tangible metatheoretical ramifications), but there's value in both perspectives. -- Live well, ~wren