Re: [Haskell-cafe] pointer equality

21 Jul 2011

      On 07/21/2011 10:30 AM, Pedro Vasconcelos wrote:
...
On Wed, 20 Jul 2011 12:48:48 -0300
Thiago Negri  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

Re: [Haskell-cafe] pointer equality

Steffen Schuldenzucker