On 07/21/2011 10:30 AM, Pedro Vasconcelos wrote:
On Wed, 20 Jul 2011 12:48:48 -0300
Thiago Negri<evoh...@gmail.com> wrote:
Is it possible to implement (==) that first check these thunks before
evaluating it? (Considering both arguments has pure types).
E.g.,
Equivalent thunks, evaluates to True, does not need to evaluate its
arguments: [1..] == [1..]
Thunks are just expressions and equality of expressions is undecidable
in any Turing-complete language (like any general-purpose programming
language). Note that syntactical equality is not sufficient because
(==) should be referentially transparent.
I think the following code pretty much models what Thiago meant for a
small subset of haskell that constructs possibly infinite lists. Thunks
are made explicit as syntax trees. 'Cycle' is the syntactic symbol for a
function whose definition is given by the respective case in the
definition of 'evalOne'.
(I chose cycle here instead of the evalFrom example above to because it
doesn't need an Enum constraint).
The interesting part is the definition of 'smartEq'.
import Data.List (unfoldr)
import Data.Function (on)
-- let's say we have syntactic primitives like this
data ListExp a = Nil | Cons a (ListExp a) | Cycle (ListExp a)
deriving (Eq, Ord, Read, Show)
-- derives syntactic equality
conss :: [a] -> ListExp a -> ListExp a
conss xs exp = foldr Cons exp xs
fromList :: [a] -> ListExp a
fromList xs = conss xs Nil
-- eval the next element, return an expression defining the tail
-- (if non-empty)
evalOne :: ListExp a -> Maybe (a, ListExp a)
evalOne Nil = Nothing
evalOne (Cons h t) = Just (h, t)
evalOne e@(Cycle exp) = case eval exp of
[] -> Nothing
(x:xs) -> Just (x, conss xs e)
eval :: ListExp a -> [a]
eval = unfoldr evalOne
-- semantic equality
evalEq :: (Eq a) => ListExp a -> ListExp a -> Bool
evalEq = (==) `on` eval
-- semantic equality, but check syntactic equality first.
-- In every next recursion step, assume the arguments of the current
recursion
-- step to be equal. We can do that safely because two lists are equal iff
-- they cannot be proven different.
smartEq :: (Eq a) => ListExp a -> ListExp a -> Bool
smartEq a b = smartEq' a b []
smartEq' :: (Eq a) => ListExp a -> ListExp a -> [(ListExp a, ListExp a)]
-> Bool
smartEq' a b eqPairs = if a == b || (a, b) `elem` eqPairs
then True
else case (evalOne a, evalOne b) of
(Just _, Nothing) -> False
(Nothing, Just _) -> False
(Nothing, Nothing) -> True
(Just (h1, t1), Just (h2, t2)) -> h1 == h2 && smartEq' t1 t2 ((a,
b):eqPairs)
Examples:
*Main> smartEq (Cycle $ fromList [1]) (Cycle $ fromList [1,1])
True
*Main> smartEq (Cons 1 $ Cycle $ fromList [1]) (Cycle $ fromList [1])
True
*Main> smartEq (Cons 2 $ Cycle $ fromList [1]) (Cycle $ fromList [1])
False
Any examples for hangups of 'smartEq' are greatly appreciated, I
couldn't produce any so far.
-- Steffen
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
