inference with functional dependencies

Ken Shan ken@digitas.harvard.edu
Tue, 14 Aug 2001 05:24:28 -0400


--uQr8t48UFsdbeI+V
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Content-Transfer-Encoding: quoted-printable

On 2001-08-13T18:08:08-0400, Avi Pfeffer wrote:
> Inferring equality between types when there are functional dependencies
> seems to be less powerful than I expected.  Here's a simple example:
>=20
> class Eq b =3D> C a b | a -> b
>=20
> data T a =3D forall b . C a b =3D> T b
> data U a =3D forall b . C a b =3D> U b
>=20
> compare :: T a -> U a -> Bool
> compare (T x) (U y) =3D x =3D=3D y

Hrm, is it possible for you to define instead

    data T a b =3D C a b =3D> T a b
    data U a b =3D C a b =3D> U a b

and propagate the dependency inference of "a -> b" upward in your
program?  Or even simply say

    data T a b =3D T a b
    data U a b =3D U a b

and put the C constraint further higher up in your program?  Just a
thought...

--=20
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
I saw my inner child once, on a milk carton.

--uQr8t48UFsdbeI+V
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

iD8DBQE7eO5LzjAc4f+uuBURAqppAKCZ2ySs66O26KxEtZbh3YHdHtojugCbBTAF
eZ9aEnF/mh5g3DtP351cEBM=
=RZlz
-----END PGP SIGNATURE-----

--uQr8t48UFsdbeI+V--