[Haskell-cafe] Musings on type systems
wren ng thornton
wren at freegeek.org
Sat Nov 20 01:52:32 EST 2010
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.
More information about the Haskell-Cafe