Hi,
> > Sadly, this example shows that Haskell 1.4 does not have a principal
> > typing property. Your function has the type
> >
> > all' :: Eq a => (a -> Bool) -> [a] -> Bool
> >
> > As well as:
> >
> > all' :: Eq a => (a -> Bool) -> F a -> Bool
> >
> > (for a suitable Monad F). But Haskell is not capable of finding the one
> > type that contains them all:
> >
> > all' :: (Monad m, Eq (m a)) => (a -> Bool) -> m a -> Bool
> What is the reason for that? It is a language design choice or is there a
> fundamental reason like, say, that allowing such things make the type
> system undecidable?
I can not speak for the designers of Haskell 1.3/1.4, but it seems
likely that the introduction of constructor class into Haskell 1.3
lead to the problem. Before then only simple type variables could be
abstracted over in the definition of a class (i.e. only type variables
of kind *). On the introduction of monads, functors, etc. into Haskell
1.3 this was no longer the case. This then implied that it was
possible for the type system to infer a type of the form (c a), for
example, where c is a type variable ranging over constructors and has
kind * -> *. This meant that the type inference system may infer a
type of the form c a => tau , which can not be reduced, at least in
Haskell 1.3/1.4, to a type of the form C a => tau. If however, no
context reduction is preformed, unless specified by the user,
princiality returns and everything continiues as normal. And yes the
system is completly decidable.
Another useful benfit of not preforming context reduction unless
specified is that overlapping instances can also be supported with out
any further technical difficulities.
Best wishes
Ben
--------
Benedict R. Gaster.
Languages and Programming Group, University of Nottingham.
A thing of beauty is a joy forever -- John Keats (1795--1821).
