[Haskell-cafe] Musings on type systems

[wren ng thornton]

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