Haskell - constructing a type that uses existential quantification

2
votes

In the code below I have defined a data type F using existential quantification. I would like values of type F to hold functions that accept a single argument and produce, say, an Int as the result. The argument needs to implement a type class which I've called C, but left empty for now.

This is my first attempt at existential types. I am clearly doing something wrong as I don't seem to be able to create values of type F.

{-# LANGUAGE ExistentialQuantification #-}

class C a where

data F = forall a. C a => F (a->Int)

makeF :: F
makeF = F $ const 1

How can I fix this compile error?

No instance for (C a0) arising from a use of `F'
In the expression: F
In the expression: F $ const 1
In an equation for `makeF': makeF = F $ const 1
2
haskellexistential-type
I find that this sort of thing is easier to do with a GADT. You can have the existential quantification and the class constraint, but the syntax is so much cleaner and easier. – AndrewC
Thanks for the tip. I should really read up on GADTs too. – knick

2 Answers

3
votes

The problem is that const 1 has type forall a . C a => a -> Int. When you pass that to F we lose the opportunity to ever talk about the type a again excepting that it is an element of type C.

Unfortunately, we've never determined what a must be!

In particular, GHC handles existentials like this by passing in the dictionary for the typeclass C corresponding to whatever type actually ends up in the existential. Since we never provided GHC enough information to find that dictionary it gives us a type error.

So to fix this we must instantiate C somewhere

instance C Int

and then pass a function which determines that the forgotten type a actually is an instance of C

let x = F (const 1 :: Int -> Int)
1
votes

If you rewrite your F definition as below it will work:

{-# LANGUAGE RankNTypes #-}

class C a where

data F = F (forall a. C a => a -> Int)

makeF :: F
makeF = F $ const 1

I'm trying to understand why myself:

Your original type says "there exists a which is instance of C, and we have function a -> Int". So to construct existential type, we have to state which a we have:

{-# LANGUAGE ExistentialQuantification #-}

class C a where

data F = forall a. C a => F (a -> Int)

-- Implement class for Unit
instance C () where

makeF :: F
makeF = F $ (const 1 :: () -> Int)

These aren't exactly equivalent definitions:

data G = forall a . C a => G {
  value :: a         -- is a value! could be e.g. `1` or `()`
  toInt :: a -> Int, -- Might be `id`
}

data G' = G' {
  value' :: C a => a          -- will be something for every type of instance `C`
  toInt' :: C a => a -> Int, -- again, by parametericity uses only `C` stuff
}