forall quantifier

Simon Peyton-Jones IMCEAEX-_O=MICROSOFT_OU=NORTHAMERICA_CN=RECIPIENTS_CN=428592@microsoft.com
Fri, 6 Jun 2003 08:15:15 +0100


|   classify :: Eq b =3D> [a->b] -> [a] -> [[[a]]]
|   classify cs xs =3D ...
|=20
| where for each classifying function in cs, I would get the xs
| partitioned accordingly.  E.g.
|=20
|   classify [fst,snd] [(1,0), (1,2), (2,0)]
|=20
| would yield
|=20
|   [ [(1,0), (1,2)], [(2,0)] -- classified by `fst`
|   , [(1,0), (2,0)], [(1,2)]] -- classified by `snd`
|=20
| Now, obviously, the problem is that fst and snd, being passed in a
| list, needs to be of the same type; this complicates classifying a
| list of type [(Int,Bool)], for instance=B9.

Use existentials

	data Classifier a =3D forall b. Ord b =3D> CL (a->b)

	classify :: [Classifier a] -> [a] -> [[[a]]]
	classify cls as =3D map (classify1 as) cls

	classify1 :: Classifier a -> [a] -> [[a]]
	classify1 (CL f) as =3D ... classify as using f....


Think of a classifier (CL f) as a pair of=20
		a) a function f:a->b
		b) an Ord dictionary for comparing b's


I forget whether I've aired this on the list, but I'm seriously thinking =
that we
should change 'forall' to 'exists' in existential data constructors like =
this one.=20
One has to explain 'forall' every time.  But we'd lose a keyword.

Simon