# newtype/datatype (was efficiency)

**Dylan Thurston
**
dpt@math.harvard.edu

*Thu, 17 Jan 2002 14:58:02 -0500*

--eHhjakXzOLJAF9wJ
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Content-Transfer-Encoding: quoted-printable
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]]:
*>*=20
*>* [t] =3D lift (T[[t]])
*>*=20
*>* We can define T[[t]] by induction over t, using the following operations
*>* on cpos (not necessarily having a bottom element):
*>*=20
*>* lift D =3D D plus a new bottom element
*>* D x E =3D cartesian product of D and E
*>* D + E =3D disjoint union of D and E
*>* D -> E =3D the cpo of continuous functions from D to E
*>* 1 =3D the one-element cpo
*>* 0 =3D the empty cpo
*>* ...
*>* For Haskell's function type, we have
*>*=20
*>* T[[s -> t]] =3D [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
--eHhjakXzOLJAF9wJ
Content-Type: application/pgp-signature
Content-Disposition: inline
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.0.6 (GNU/Linux)
Comment: For info see http://www.gnupg.org
iD8DBQE8RyzKVeybfhaa3tcRAhZOAKCfAUBMO0Pbqeq3jlsAOI4lz8a9vQCdG5EK
MsR6uG3aLi6nWOrw1XTuGVc=
=P7gp
-----END PGP SIGNATURE-----
--eHhjakXzOLJAF9wJ--