Existential type wrappers necessity
existential-type, haskell, higher-rank-types, polymorphism
Solution
There are two issues you have to consider regarding the handling of existential types:
- If you store "anything that can be `show`n," you have to store the thing that can be shown along with how to show it.
- An actual variable can only ever have one single type.
The first point is why you have to have existential type wrappers, because when you write this:
data Showable = Show a => Showable a
What actually happens is that something like this gets declared:
data Showable a = Showable (instance of Show a) a
I.e. a reference to the class instance of `Show a` is stored along with the value `a`. Without this happening, you can't have a function that unwraps a `Showable`, because that function wouldn't know how to show the `a`.
The second point is why you get some type quirkiness sometimes, and why you can't bind existential types in `let` bindings, for example.
You also have an issue with your reasoning in your code. If you have a function like `forall a . Show a => (Int -> a)` you get a function that, given any integer, will be able to produce any kind of showable value that the caller chooses. You probably mean `exists a . Show a => (Int -> a)`, meaning that if the function gets an integer, it will return some type for which there exists a `Show` instance.
Problem
Turns out that it is surprisingly difficult to use existential/rank-n types correctly despite the very simple idea behind them. Why are wrapping existential types into `data` types is necessary? I have the following simple example: ``` {-# LANGUAGE RankNTypes, ImpredicativeTypes, ExistentialQuantification #-} module Main where c :: Double c = 3 -- Moving `forall` clause from here to the front of the type tuple does not help, -- error is the same lists :: [(Int, forall a. Show a => Int -> a)] lists = [ (1, \x -> x) , (2, \x -> show x) , (3, \x -> c^x) ] data HRF = forall a. Show a => HRF (Int -> a) lists' :: [(Int, HRF)] lists' = [ (1, HRF $ \x -> x) , (2, HRF $ \x -> show x) , (3, HRF $ \x -> c^x) ] ``` If I comment out the definition of `lists`, the code compiles successfully. If I do not comment it out, I'm getting the following errors: ``` test.hs:8:21: Could not deduce (a ~ Int) from the context (Show a) bound by a type expected by the context: Show a => Int -> a at test.hs:8:11-22 `a' is a rigid type variable bound by a type expected by the context: Show a => Int -> a at test.hs:8:11 In the expression: x In the expression: \ x -> x In the expression: (1, \ x -> x) test.hs:9:21: Could not deduce (a ~ [Char]) from the context (Show a) bound by a type expected by the context: Show a => Int -> a at test.hs:9:11-27 `a' is a rigid type variable bound by a type expected by the context: Show a => Int -> a at test.hs:9:11 In the return type of a call of `show' In the expression: show x In the expression: \ x -> show x test.hs:10:21: Could not deduce (a ~ Double) from the context (Show a) bound by a type expected by the context: Show a => Int -> a at test.hs:10:11-24 `a' is a rigid type variable bound by a type expected by the context: Show a => Int -> a at test.hs:10:11 In the first argument of `(^)', namely `c' In the expression: c ^ x In the expression: \ x -> c ^ x Failed, modules loaded: none. ``` Why is this happening? Shouldn't the second example be equivalent to the first one? What is the difference between these usages of n-rank types? Is it possible at all to leave out extra ADT definition and use only simple types when I want such kind of polymorphism?