{- 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