[Haskell-cafe] Is there a notion for identity?

8 Jan 2006

      {- Disclaimer: I'm rather new to Haskell and completely new to this board.
     I may not use the correct terminology in all cases, but I hope my 
     intention becomes clear when you have a look at the code-snippets. -}

Hey ho,

Is there any way two find out whether two variables refer to the
same cell? That is I'm looking for a notion of identity (compareable
to == in Java) as opposed to equality (== in Haskell).

The motivation is that I need to find out whether two infinite
structures are identical.

Consider this Haskell implementation of the simple typed lambda calculus
(STLC) with the primitive Type "TyUnit" and the primitive value "TmUnit":

data Type = TyUnit | TyArrow Type Type
  deriving (Show,Eq)

data Term = TmUnit | TmVar String | TmAbs String Type Term | TmApp Term Term
  deriving Show

{- Context is some LIFO structure which stores Argument-Type bindings: -}
data Context = {- ... -}
ctxEmpty    :: Context 
addBinding  :: Context -> String -> Type -> Context
getBinding  :: Context -> String -> Type

typeof :: Context -> Term -> Type
typeof _   TmUnit          = TyUnit
typeof ctx (TmVar s)       = getBinding ctx s
typeof ctx (TmAbs s ty1 t) = let ctx' = addBinding ctx s ty1
                                 ty2  = typeof ctx' t
                             in TyArrow ty1 ty2   
typeof ctx (TmApp t1 t2)   = let (TyArrow ttp tte) = typeof ctx t1
                                 tta               = typeof ctx t2
{- (1) problem here: -}       in if tta==ttp then tte 
                                 else error "..."  

-- eval omitted...

The STLC does not provide a notion for recursion as it stands. My
idea was to simulate recursion by using infinte structures 
of type Type.

Consider this definition of the omega-combinator:

omegaType :: Type
omegaType = TyArrow omegaType omegaType

omega, omegaAbs :: Term
omega = TmApp omegaAbs omegaAbs
omegaAbs = TmAbs "x" omegaType (TmApp (TmVar "x") (TmVar "x"))

Now it would be nice if "typeof ctxEmpty omega" would return
omegaType. Unfortunately it doesn't. Instead it loops on line
((1)), since omegaType and omegaType will never be compared to
be equal using (==).

If we had a function `sameAddress` we could write 
"tta `sameAddress` ttp || tta==ttp" instead of "tta==ttp"
in line ((1)). If I interpret the chapter about infinite
lists in the bird book correctly, this should be sound.
omegaType will be represented by a cyclic graph in
the runtime system and will therefore always refer to
the same cell.

The issue becomes a little more complicated if we
consider:

omegaType, omegaType' :: Type
omegaType  = TyArrow omegaType  omegaType
omegaType' = TyArrow omegaType' omegaType'

omega, omegaAbs, omegaAbs' :: Term
omega = TmApp omegaAbs omegaAbs'
omegaAbs  = TmAbs "x" omegaType  (TmApp (TmVar "x") (TmVar "x"))
omegaAbs' = TmAbs "x" omegaType' (TmApp (TmVar "x") (TmVar "x"))

In this case it wouldn't be clear whether 
" omegaType `sameAddress` omegaType' " should be True
or False, as a clever compiler might detect that
both are identical and make them refer to the same
address (, correct me if I'm wrong). This might
be a reason that there is no `sameAddress`.

My questions are: Is there any way to implement
"sameAddress" in Haskell? Or is it at least
possible to implement it with GHC using some 
compiler-specific notation?

Thanks,
Tim

[Haskell-cafe] Is there a notion for identity?

Tim Walkenhorst