On Thu, Jan 17, 2002 at 12:16:14PM +0000, Ross Paterson wrote: > 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 Haskell's function type, we have > > T[[s -> t]] = [s] -> [t]
If I understand it correctly, this makes
\x.undefined :: a -> b
different from
undefined :: a -> b
For instance, in this setup, the CPO
[()->()]
has four elements, in a totally ordered CPO; in increasing order, they
are
undefined
const undefined
id
const ()
Is it really clear the first two ('undefined' and 'const undefined') are
different? Ken says they are observationally equivalent.
--Dylan Thurston
msg01191/pgp00000.pgp
Description: PGP signature
