Existential type in higher order function

Question

I've got a function whose job is to compute some optimal value of type a wrt some value function of type a -> v

type OptiF a v = (a -> v) -> a

Then I have a container that wants to store such a function together with another function which uses the values values:

data Container a = forall v. (Ord v) => Cons (OptiF a v) (a -> Int)

The idea is that whoever implements a function of type OptiF a v should not be bothered with the details of v except that it's an instance of Ord.

So I've written a function which takes such a value function and a container. Using the OptiF a v it should compute the optimal value wrt val and plug it in the container's result function:

optimize :: (forall v. (Ord v) => a -> v) -> Container a -> Int
optimize val (Cons opti result) = result (opti val)

So far so good, but I can't call optimize, because

callOptimize :: Int
callOptimize = optimize val cont
   where val = (*3)
         opti val' = if val' 1 > val' 0 then 100 else -100
         cont = Cons opti (*2)

does not compile:

Could not deduce (v ~ Int)
from the context (Ord v)
  bound by a type expected by the context: Ord v => Int -> v
  at bla.hs:12:16-32
  `v' is a rigid type variable bound by
      a type expected by the context: Ord v => Int -> v at bla.hs:12:16
Expected type: Int
  Actual type: Int
Expected type: Int -> v
  Actual type: Int -> Int
In the first argument of `optimize', namely `val'
In the expression: optimize val cont

where line 12:16-32 is optimize val cont.

Am I misunderstanding existential types in this case? Does the forall v in the declaration of optimize mean that optimize may expect from a -> v whatever v it wants? Or does it mean that optimize may expect nothing from a -> v except that Ord v?

What I want is that the OptiF a v is not fixed for any v, because I want to plug in some a -> v later on. The only constraint I'd like to impose is Ord v. Is it even possible to express something like that using existential types (or whatever)?

I managed to achieve that with an additional typeclass which provides an optimize function with a similar signature to OptiF a v, but that looks much uglier to me than using higher order functions.

Answer 1

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 in Ord 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 Ords 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)