John Launchbury <[EMAIL PROTECTED]> writes:
> [...] a "polymorphic" seq cripples parametricity (theorems for free).
> Already, because fix is polymorphic, the relations in the parametricity
> theorem are forced to be strict which throws away some interesting
> theorems.
Indeed, fix shouldn't be unconditionally polymorphic either. Suppose we
allow bottom-less (but still chain-complete) domains and non-strict
(but still inductive) relations, and specify which ones must contain a
designated bottom:
class Pointed a where
bottom :: a -- least element
instance Pointed b => Pointed(a -> b) where
bottom x = bottom
fix :: Pointed a => (a -> a) -> a
The relational interpretation of the Pointed class is that the relation
must relate the bottoms, i.e. strictness.
By definition, lifted sum types are always Pointed. Unlifted sum types
are Pointed iff they have only one constructor and all its arguments
are Pointed: the bottom of the new type is a tuple of bottoms.
We also need bottoms for the solution of recursive domain equations, so
we have the restriction: in any cycle of mutually recursively defined
data types, at least one must be Pointed. But in deciding which types
are Pointed, we take the largest consistent assignment. For example,
the following type is Pointed and therefore legal:
newtype Pointed a => Seq a = Pair a (Seq a)
Back to fix: if we take (a typed version of) Curry's definition
data SelfApp a = Fun(SelfApp a -> a)
fix z = z(Fun z)
where z(Fun x) = f(x(Fun x))
then fix gets the above type because z analyses a lifted type, and
therefore has a Pointed result type. If we use an unlifted definition
newtype Pointed a => SelfApp a = Fun(SelfApp a -> a)
where the Pointed condition is necessary to get Pointed(SelfApp a), we
get the same type for fix as before. The free theorem from this type
is Scott induction, and any two functions satisfying it are equal.
The result would be slightly more general types (and thus stronger free
theorems), e.g.
reverse :: [a] -> [a] -- no Pointed constraint
foldr :: Pointed b => (a -> b -> b) -> b -> [a] -> b
whereas currently each type variable implicitly carries a Pointed
constraint.
-- Ross Paterson
