newtype/datatype (was efficiency)

[Dylan Thurston]

--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--