[Haskell-cafe] Existential quantification of environments.

[Keean Schupke]

If I have a function:

   f x y = add x y

and I want to type the function in isolation, then the type of 'add' is 
essentially carried in the environment... Lets say I want to make this 
type explicit in the type signature (where f is valid for any a where 
there is an add function on a - ignoring the class that Haskell would 
require for the overloading):

   add :: Int -> Int -> Int
   add :: Float -> Float -> Float

   f :: forall a . exists (add :: a -> a -> a) => a -> a -> a

or a step further:

   class Add a where
      add :: a -> a -> a
   instance Add Int where ...
   instance Add Float where ...

   f :: forall a . Add a => a -> a -> a

This seems to suggest:

    Add a == exists (add :: a -> a -> a)

Does this seem in any way right? It seems that the definition of 'f' 
does require the existance of 'add'. That is the definition is valid iff 
there exists a function called 'add' of the correct type. Also doesn't 
the existential quantifier stop you looking inside 'add' - obviously you 
cannot inspect the definition as it may not be defined (yet?), but 
presumably you can still apply 'add'.

    Regards,
    Keean.