This is something that's easy to get wrong.
What you have in the signature of optimize
is not an existential, but a universal.
...since existentials are somewhat outdated anyway, let's rewrite your data to GADT form, which makes the point clearer as the syntax is essentially the same as for polymorphic functions:
data Container a where
(:/->) :: Ord v => -- come on, you can't call this `Cons`!
OptiF a v -> (a->Int) -> Container a
Observe that the Ord
constraint (which implies that here's the forall v...
) stands outside of the type-variable–parameterised function signature, i.e. v
is a parameter we can dictate from the outside when we want to construct a Container
value. In other words,
For all
v
inOrd
there exists the constructor(:/->) :: OptiF a v -> (a->Int) -> Container a
which is what gives rise to the name "existential type". Again, this is analog to an ordinary polymorphic function.
On the other hand, in the signature
optimize :: (forall v. (Ord v) => a -> v) -> Container a -> Int
you have a forall
inside the signature term itself, which means that what concrete type v
may take on will be determined by the callee, optimize
, internally – all we have control over from the outside is that it be in Ord
. Nothing "existential" about that, which is why this signature won't actually compile with XExistentialQuantification
or XGADTs
alone:
<interactive>:37:26:
Illegal symbol '.' in type
Perhaps you intended -XRankNTypes or similar flag
to enable explicit-forall syntax: forall <tvs>. <type>
val = (*3)
obviously doesn't fulfill (forall v. (Ord v) => a -> v)
, it actually requires a Num
instance which not all Ord
s have. Indeed, optimize
shouldn't need the rank2 type: it should work for any Ord
-type v
the caller might give to it.
optimize :: Ord v => (a -> v) -> Container a -> Int
in which case your implementation doesn't work anymore, though: since (:/->)
is really an existential constructor, it needs to contain only any OptiF
function, for some unknown type v1
. So the caller of optimize has the freedom to choose the opti-function for any particular such type, and the function to be optimised for any possibly other fixed type – that can't work!
The solution that you want is this: Container
shouldn't be existential, either! The opti-function should work for any type which is in Ord
, not just for one particular type. Well, as a GADT this looks about the same as the universally-quantified signature you originally had for optimize
:
data Container a where
(:/->) :: (forall v. Ord v => OptiF a v) -> (a->Int) -> Container a
With that now, optimize works
optimize :: Ord v => (a -> v) -> Container a -> Int
optimize val (opti :/-> result) = result (opti val)
and can be used as you wanted
callOptimize :: Int
callOptimize = optimize val cont
where val = (*3)
opti val' = if val' 1 > val' 0 then 100 else -100
cont = opti :/-> (*2)