Using forall as a quantifier is very confusing. It implies predicate logic and, while I am sure there is a formal system of types, it is not a predicate logic. Here forall represents “don’t care” or “I’m not looking inside anyway so why should I care”. There is still a one-to-one mapping between the type formalism and model. Not at all the same concept as universal quantification which models as “all these possibilties”. There is one function which treats that data as a black box. If dynamic dispatch is needed for instances of a class the calling function doesn’t need to know about the details, even if the runtime has to add dispatch code (that haskell 98 would never need).
In pure haskell 98 you can think of parametrically polymorphic functions as always being specialized at their invocation point by the compiler, and so can be thought of as a kind of family of functions; a context for which universal quantification makes a warped kind of sense; provided you quantify outside of the type specification. i.e. forall x y. {map :: (x -> y) -> [x] -> [y]} is not unreasonable. But {map :: forall x y. (x -> y) -> [x] -> [y]} is just nonsense despite that being the official syntax. We are using the generic programming model from C++ where templates really do spawn a family of functions. Unlike C++ there is never any need to specialize the actual code unless the compiler is doing optimizations. Ad-hoc polymorphic functions via classes and instances also have a happy home in this model but without the possibility of run-time polymorphism.
This modelling make sense but breaks down when you try to account for the type system extensions that come after haskell 98. The forall quantifier is an anachronism. It should be replaced for he sake of clarity.
{-# OPTIONS_GHC -fglasgow-exts -fallow-incoherent-instances #-}
module Main where
-- playing with forall types
data Tree a = Node (Tree a) a (Tree a) | Null deriving (Ord,Eq,Show,Read)
llength, rlength, size :: (Num n) => Tree a -> n -- inferred
maxdepth :: (Num n, Ord n) => Tree a -> n -- inferred
breadth :: (Fractional n, Ord n) => Tree a -> n -- inferred
tnull :: Tree a -> Bool -- inferred
tsum :: (Num a) => Tree a -> a -- inferred
average :: (Fractional a) => Tree a -> a -- inferre
trigger :: (Num a) => Tree a -> Bool
tid :: Tree a -> Tree a
llength Null = 0
llength (Node l _ _) = 1 + llength l
rlength Null = 0
rlength (Node _ _ r) = 1 + rlength r
size Null = 0
size (Node l _ r) = 1 + (size l) + (size r)
maxdepth Null = 0
maxdepth (Node l _ r) = 1 + max (maxdepth l) (maxdepth r)
breadth a = size a / maxdepth a
tnull Null = True
tnull Node{} = False
tsum Null = 0
tsum (Node l a r) = tsum l + a + tsum r
average a = tsum a / size a
trigger = (45 ==) . tsum
tid = id
----
traverS :: Tree a -> ([a] -> [a])
traverse :: Tree a -> [a]
ordered :: (Ord a) => Tree a -> Bool
traverS Null = id
traverS (Node l a r) = traverS l . (a:) . traverS r
traverse = flip traverS []
ordered t = all (\(a,b) -> a (Tree a -> t) -> t -- inferred
eg' f = f eg
where eg = Node (Node (Node Null 1 (Node Null 2 Null)) 3 (Node Null 4 Null))
5
(Node (Node (Node (Node Null 6 Null) 7 Null) 8 Null) 9 Null)
eg''' :: (forall a. Tree a -> t) -> t
eg''' f = eg' f
egN' :: (forall a. (Num a) => Tree a -> t) -> t
egN' f = eg' f
egO' :: (forall a. (Ord a) => Tree a -> t) -> t
egO' f = eg' f
egw' :: Int -> (forall a. (WierdNess a) => Tree a -> t) -> t
egw' t f = case t of
0 -> f (eg :: Tree Integer)
1 -> f (eg :: Tree Int)
2 -> f (eg :: Tree Double)
3 -> f (eg :: Tree Float)
egW' :: (forall a. (WierdNess a) => Tree a -> IO t) -> IO [t]
egW' f = sequence [egw' t f| t Tree a
eg = eg' id
eg0 :: Tree Integer -- inferred
eg0 = eg' id
eg1 :: Tree Int
eg1 = eg' id
eg2 :: Tree Double
eg2 = eg' id
eg3 :: Tree Float
eg3 = eg' id
----
class (Num a) => WierdNess a
where showWierd :: Tree a -> ShowS
instance WierdNess Integer
where showWierd Null = ("" ++)
showWierd (Node l a r)
= ('{':) . showWierd l & shows a & showWierd r . ('}':)
where infixr 9 &
a & b = a .(", " ++). b
instance WierdNess Int
where showWierd Null = ("{}" ++)
showWierd (Node Null a Null) = ('{':) . shows a . ('}':)
showWierd (Node Null a r) = ('{':) . shows a . showWierd r . ('}':)
showWierd (Node l a Null)= ('{':) . showWierd l . shows a . ('}':)
showWierd (Node l a r)
= ('{':) . showWierd l . shows a . showWierd r . ('}':)
instance WierdNess Double
where showWierd a = shows a
instance WierdNess Float
where showWierd a = shows a
type Weird a = Tree a -> IO (Tree a)
type Weeee a = Tree a -> IO ()
weird :: (WierdNess a) => Weird a
weeee :: (WierdNess a) => Weeee a
weird a = putStrLn (showWierd a "") >> return a
weeee a = putStrLn (showWierd a "")
----
main = do
print (eg' llength)
egW' weeee