Fri, 5 Nov 1999 10:00:25 +0100 (MET), Koen Claessen <[EMAIL PROTECTED]> pisze:
> data Expr a = Val a | forall b . Apply (Expr (b -> a)) (Expr b)
------------------------------------------------------------------------
data Expr a = Val a | forall b. Apply (Expr (b -> a)) (Expr b)
data Expr' a = Val' a | Apply' (Expr' a) (Expr' ())
deriving Eq
exprToExpr' :: Expr a -> Expr' a
exprToExpr' (Val a) = Val' a
exprToExpr' a@(Apply f b) = Apply' (structure (eval a) f)
(structure () b)
structure :: b -> Expr a -> Expr' b
structure x (Val _) = Val' x
structure x (Apply f b) = Apply' (structure x f) (structure () b)
eval :: Expr a -> a
eval (Val a) = a
eval (Apply f b) = eval f (eval b)
------------------------------------------------------------------------
Now, try to find values x, y :: Expr Int such that they are different
(i.e. there exists a function f :: Expr Int -> Int such that
f x /= f y, because you can't easily compare Exprs directly[1]), but
exprToExpr' x == exprToExpr' y. Differences in divergence don't count.
If I am right and didn't make an error, this impossibility shows
that in this case existentials are not really needed, because you
can convert to a type without existentials without loosing information.
--------
[1] GHC fails instead of giving an error when asked for deriving Eq
on Expr. I'm submitting a report to glasgow-haskell-bugs.
--
__("< Marcin Kowalczyk * [EMAIL PROTECTED] http://qrczak.ids.net.pl/
\__/ GCS/M d- s+:-- a22 C+++>+++$ UL++>++++$ P+++ L++>++++$ E-
^^ W++ N+++ o? K? w(---) O? M- V? PS-- PE++ Y? PGP->+ t
QRCZAK 5? X- R tv-- b+>++ DI D- G+ e>++++ h! r--%>++ y-
