newtype/datatype (was efficiency)

Dylan Thurston
Thu, 17 Jan 2002 14:58:02 -0500

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]]:
> 	[t] =3D 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 =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
> 	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
  const undefined
  const ()
Is it really clear the first two ('undefined' and 'const undefined') are
different?  Ken says they are observationally equivalent.

--Dylan Thurston

Content-Type: application/pgp-signature
Content-Disposition: inline

Version: GnuPG v1.0.6 (GNU/Linux)
Comment: For info see