[Haskell-cafe] pointer equality

[Steffen Schuldenzucker]

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