[Haskell-cafe] Existential quantification of environments.
k.schupke at imperial.ac.uk
Tue Nov 22 05:39:09 EST 2005
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'.
More information about the Haskell-Cafe