BEGIN 16_10_18_PrincipalTypeProperty.lhs

THE PRINCIPAL TYPE PROPERTY


An important feature of the Haskell's type system is that it satisfies
-- or tries to satisfy -- the so-called PRINCIPAL TYPE PROPERTY (PTP), 
which informally says that, given an untyped program expression M, 
Haskell's type-inference engine will infer the "most general type" t 
for M, if M is at all typable in the system.

This also means that, given any valid type t' for M, it will be the
case that t' is obtained from t by substitution, i.e., by substituting
appropriately defined types into the type variables in t.

That Haskell's type system satisfies the PTP is in fact only true in
theory. In practice, for various pragmatic reasons, it does not.

The way it is implemented, Haskell ALMOST satisfies the PTP, but not
always. There are obscure corners in the type system, which we will 
not examine here, which prevent Haskell from fully satisfying the PTP.

HERE IS AN EXAMPLE. Consider the functions "h" and "k":

> h x y = x + y

> k = \ x y -> x + y  -- \ x -> \ y -> x + y

Normally, we would expect "h" and "k" to behave identically, but they
don't. If we try to evaluate the following expressions: (h 3.2 6) and
(k 3.2 6), the first returns 9.2 as expected, while the second returns
an error message.  This happens because different types are inferred
for "h" and "k":

    h :: Num a => a -> a -> a
    k :: Integer -> Integer -> Integer

The type inferred for "h" is the most general, i.e., the principal, as
expected. But the typed inferred for "k" is NOT the most general. So,
the PTP is violated in the case of "k". To make things more confusing,
if we declare *explicitly* the type of "k" by making it the same as
that of "h":

> k' :: Num a => a -> a -> a
> k' = \ x y -> x + y

then we can evaluate (k' 3.2 6) without error. This also means that
the type explicitly requested for k' by the user is *more general* than
the type inferred for k by Haskell. It should be the other way around!

HERE IS A SECOND EXAMPLE. Once more consider the data type of binary
trees where only leaf nodes are labelled:

> data Tree a = L a | N (Tree Int) (Tree a)   
>               deriving (Show)

Note that, in the preceding definition of binary trees, the left subtree
of a node has type "(Tree Int)" whereas its right subtree has type
"(Tree a)".

The functions "foo" and "bar" below count the number of leaf nodes in
a binary tree.

> foo (L _) = 1
> foo (N t1 t2) = (foo t1) + (foo t2)

> bar1 :: Tree a -> Int
> bar1 (L _) = 1
> bar1 (N t1 t2) = (bar1 t1) + (bar1 t2)

> bar2 :: Num a => Tree b -> a
> bar2 (L _) = 1
> bar2 (N t1 t2) = (bar2 t1) + (bar2 t2)

The only difference between "foo", "bar1", and "bar2" is that the type of "foo"
is inferred by Haskell's type-inference engine, while the types of "bar1" and
"bar2" are explicitly declared. What we get is this:

  foo  :: Num a => Tree Int -> a
  bar1 :: Tree a -> Int
  bar2 :: Num a => Tree b -> a

The type of "foo" is less general than the type of "bar2", since 
"Num a => Tree Int -> a" is an instance of "Num a => Tree b -> a".
If Haskell truly satisfied the PTP, it would be the other way around!!
As for the types of "foo" and "bar1", neither is an instance of the
other.

HERE IS A THIRD EXAMPLE. Consider carefully the difference between the
definitions of functions "f" and "g" below:

> class IsNil a where
>   isNil :: a -> Bool

> instance IsNil Char where
>   isNil 'a' = True
>   isNil  _  = False

> instance (Num a, Ord a) => IsNil (Maybe a) where
>   isNil Nothing        = True 
>   isNil (Just x)              
>     | x <= 0           = True
>     | otherwise        = False

> instance IsNil [b] where
>   isNil [] = True
>   isNil _  = False

> f1 x y = let h = isNil
>          in  (h x, h y)
 
> -- f2 x y = let (h :: [c] -> Bool) = isNil
> --          in  (h x, h y)

> -- f3 (x :: [a]) (y :: [b]) = let (h :: [c] -> Bool) = isNil
> --         in  (h x, h y)

> -- f4 x y = let (h :: Char -> Bool) = isNil
> --          in  (h x, h y)

> -- f5 (x :: Maybe a) y = let h = isNil
> --                      in  (h x, h y)

(I commented out the definitions of f3 and f5 above because they caused
an error with HUGS "Haskell 98 does not support pattern type annotations".
I also commented out the definitions of f2 and f4 because they caused an
error with GHCI, but not with HUGS.)

In the definition of "f1" we have omitted all types. So, we should
expect the type-inference algorithm to produce a most general type
for "f1".  

By contrast, in the definition of "f2" -- and also "f3", "f4", and "f5" --
we have inserted some types, which in turns makes the type-inference 
algorithm produce a type consistent with the inserted types.

Here are the types inferred for "f1" and "f2": 

   f1 :: IsNil a => a -> a -> (Bool,Bool)
   f2 :: [a] -> [b] -> (Bool,Bool)

but, contrary to expectation, the type of "f2" is not an instance of
the type of "f1". Hence, the type of "f1" is in fact not a most general
type.

We will not explain the weird behavior described above. But if you
want to find out on your own, search the web for articles on the
"principal type property" and on the "monomorphism restriction" (this
is the name of the technical reason why the PTP is here violated by
Haskell).

END 16_10_18_PrincipalTypeProperty.lhs