[Haskell-cafe] Is there a notion for identity?
Tim Walkenhorst
tim.walkenhorst at gmx.de
Sun Jan 8 06:43:31 EST 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
More information about the Haskell-Cafe
mailing list