haskell-cafe@haskell.org
[Top] [All Lists]

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

Subject: Re: [Haskell-cafe] How to understand the 'forall' ?
From: Daniil Elovkov
Date: Wed, 09 Sep 2009 12:08:34 +0400
Ryan Ingram wrote:
On Tue, Sep 8, 2009 at 12:44 PM, Daniil
Elovkov<daniil.elovkov@xxxxxxxxxxxxxx> 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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@xxxxxxxxxxx
http://www.haskell.org/mailman/listinfo/haskell-cafe

<Prev in Thread] Current Thread [Next in Thread>