[Haskell-cafe] How to understand the 'forall' ?

[Daniil Elovkov]

Ryan Ingram wrote:
> On Tue, Sep 8, 2009 at 12:44 PM, Daniil
> Elovkov<daniil.elovkov at googlemail.com> wrote:
>> Existential is a perfect word, because it really is
>> data S = exists a. Show a => S [a].
> 
> If you were going to make "exists" a keyword, I think you would write
> it like this:
> 
>> data S = ConsS (exists a. Show a => [a])
> 
> To contrast:
> 
>> data GhcS = forall a. Show a => ConsGhcS [a]
>> data T = ConsT (forall a. Show a => [a])
> 
> This gives these constructors:
> 
>> ConsS :: forall a. (Show a => [a] -> S)
>> ConsGhcS :: forall a. (Show a => [a] -> S)  -- same
>> ConsT :: (forall a. Show a => [a]) -> T -- higher-rank type!

Yes, this last one can confuse somebody who tries to understand the 
difference between existential quantification and first-class 
polymorphism. Because it looks like the former, but really is the latter.

> T isn't very useful, it has to be able to provide a list of *any*
> instance of Show, so probably [] is all you get.  But you can do
> something similar:
> 
>> data N = ConsN (forall a. Num a => [a])
> 
> Now you get
> 
>> ConsN :: (forall a. Num a => [a]) -> N
> 
> and you can legally do
> 
>> n = ConsN [1,2,3]
> 
> since [1,2,3] == [fromInteger 1, fromInteger 2, fromInteger 3] ::
> forall a. Num a => [a]
> 
> Conceptually, an "S" holds *some* instance of Show, so the user of a
> constructed S can only use methods of Show; they don't have any
> further knowledge about what is inside.  But a N holds *any* instance
> of Num, so the user of the data can pick which one they want to use;
> Integer, Rational, Double, some (Expr Int) instance made by an
> embedded DSL programmer, etc.

Well, that seems to be exactly how I worded it, but with the examples of 
data constructor vs function signature, rather than 2 data constructors.

> Of course, there are some ways to recover information about what types
> are inside the existential using GADTs or Data.Dynamic.  But those
> need to be held in the structure itself.  For example:


This is quite amazing. What follows is almost a literal copy of my code, 
which isn't open :) Even the names are very close!

In my version eqTyp is unify :)

Hmm, sometimes I think that Haskell allows expressing an intension in so 
many ways (and I'm sure it's true), but this...

>> data Typ a where
>>    TBool :: Typ Bool
>>    TInt :: Typ Int
>>    TFunc :: Typ a -> Typ b -> Typ (a -> b)
>>    TList :: Typ a -> Typ [a]
>>    TPair :: Typ a -> Typ b -> Typ (a,b)
> 
> Now you can create an existential type like this:
> 
>> data Something = forall a. Something (Typ a) a
> 
> and you can extract the value if the type matches:
> 
>> data TEq a b where Refl :: TEq a a
>> extract :: forall a. Typ a -> Something -> Maybe a
>> extract ta (Something tb vb) = do
>>    Refl <- eqTyp ta tb
>>    return vb
> 
> This desugars into
> 
> ] extract ta (Something tb vb) =
> ]    eqTyp ta tb >>= \x ->
> ]      case x of
> ]         Refl -> return vb
> ]         _ -> fail "pattern match failure"
> 
> which, since Refl is the only constructor for TEq, simplifies to
> 
> ] extract ta (Something tb vb) = eqTyp ta tb >>= \Refl -> Just vb
> 
> The trick is that the pattern match on Refl proves on the right-hand
> side that "a" is the same type as that held in the existential, so we
> have successfully extracted information from the existential and can
> return it to the caller without breaking encapsulation.  Here's the
> helper function eqTyp; it's pretty mechanical:
> 
>> eqTyp :: Typ a -> Typ b -> Maybe (TEq a b)
>> eqTyp TBool TBool = return Refl
>> eqTyp TInt TInt = return Refl
>> eqTyp (TFunc a1 b1) (TFunc a2 b2) = do
>>    Refl <- eqTyp a1 a2
>>    Refl <- eqTyp b1 b2
>>    return Refl
>> eqTyp (TList a1) (TList a2) = do
>>    Refl <- eqTyp a1 a2
>>    return Refl
>> eqTyp (TPair a1 b1) (TPair a2 b2) = do
>>    Refl <- eqTyp a1 a2
>>    Refl <- eqTyp b1 b2
>>    return Refl
>> eqTyp _ _ = Nothing
> 
> Here's a simple test:
> 
>> test = Something (TFun TInt TBool) (\x -> x == 3)
>> runTest = fromJust (extract (TFun TInt TBool) test) 5
> 
> runTest == False, of course.
> 
>   -- ryan