On Tue, Sep 8, 2009 at 12:44 PM, Daniil Elovkov<daniil.elov...@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! 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. 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: > 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe