On Wed, Jan 16, 2002 at 11:25:43PM -0500, Ken Shan wrote:
Every type "t" in Haskell can be denotationally modeled by a complete partial order (CPO), which we will notate as "[t]". In fact, every type in standard Haskell corresponds to a -pointed- CPO, meaning a CPO with a least element "bottom".
We can avoid smash products and coalesced sums by analysing [t] as being the lifting of a not-necessarily-pointed cpo T[[t]]: [t] = lift (T[[t]]) We can define T[[t]] by induction over t, using the following operations on cpos (not necessarily having a bottom element): lift D = D plus a new bottom element D x E = cartesian product of D and E D + E = disjoint union of D and E D -> E = the cpo of continuous functions from D to E 1 = the one-element cpo 0 = the empty cpo For primitive types like Int, Integer, Double, etc, T[[t]] is just a discrete cpo (i.e. a set, with no bottom element). For Haskell's function type, we have T[[s -> t]] = [s] -> [t] For a data declaration data D = c1 | ... | cn we have T[[D]] = C[[c1]] + ... + C[[cn]] C[[K a1 ... an]] = A[[a1]] x ... x A[[an]] C[[K]] = 1 -- the identity for cartesian product A[[t]] = [t] A[[! t]] = T[[t]] For a newtype declaration newtype N = K t we have T[[N]] = T[[t]] To take the original questions, newtype Empty a = E () data Empty' a = E' newtype Pair v w a = P (v a, w a) data Pair' v w a = P' (v a) (w a) we have T[[Empty]] = T[[()]] = 1 T[[Empty']] = C[[E']] = 1 T[[Pair v w a]] = T[[(v a, w a)]] = [v a] x [w a] T[[Pair' v w a]] = C[[P' (v a) (w a)]] = [v a] x [w a] So semantically they're the same. I suspect the reason Chris used newtype is that GHC knows about the predefined tuple types and does some extra optimizations on them, but doing this for user-defined type constructors across module boundaries is a bit harder. Similarly, given newtype M = MC t data N = NC !t we have T[[M]] = T[[t]] = T[[N]], though as you pointed out, pattern matching is defined differently for the two types. (The formal semantics in the Report seems to be missing the relevant rule, though its informal semantics is clear on this point.) As for recursive types, I don't know a simple presentation of the general case, but if there's no recursion through the first argument of a -> type it's just the smallest cpo such that the two sides are isomorphic. For example, for data Nat = Zero | Succ Nat we have T[[Nat]] ~= 1 + lift (T[[Nat]]) or [Nat] ~= lift (1 + [Nat]) The elements of [Nat] are _|_, Zero, Succ _|_, Succ Zero, etc and, to make it complete, an extra element Succ (Succ (Succ ...)) which is the least upper bound of the chain _|_ <= Succ _|_ <= Succ (Succ _|_) <= ... On the other hand, for data Nat = Zero | Succ !Nat we have T[[Nat]] ~= 1 + T[[Nat]] i.e. the elements of T[[Nat] are equivalent to the natural numbers, and [Nat] has an extra bottom element. Another example (from Patrik Jansson): newtype Void = Void Void then T[[Void]] is the least cpo such that T[[Void]] = T[[Void]] so it is the empty cpo 0, and [Void] is a one-element cpo. Another definition of the same cpo is data Void = Void !Void and many more are possible, even without GHC's extension.