Is there a notion for identity?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

Is there a notion for identity?

Tim Walkenhorst-2
{- 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 mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Is there a notion for identity?

Marc Weber
On Sun, Jan 08, 2006 at 12:43:31PM +0100, Tim Walkenhorst wrote:
> {- 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).

If you haven't seen this thread already:
"Detecting Cycles in Datastructures" covering exactly your topic, I
think..
You can use google groups to find it. It's from okt.

Marc
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Is there a notion for identity?

Bugzilla from robdockins@fastmail.fm
In reply to this post by Tim Walkenhorst-2
On Sunday 08 January 2006 06:43 am, Tim Walkenhorst wrote:
> {- 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).

Another poster has already replied with a link to a long answer.  The short
answer is "no, not really".

An attempted rationale:

The semantics of such an "identity" operator are unclear.  The operator could
be a test for leibenz equality (ie, structural equality, ie replaceability in
all contexts), but such an operator cannot be decidable (proof due to
Church), so that wouldn't help in your situation anyway.  The general
usefulness of such an operator is debatable.

We could instead provide an implementation-dependent operation that tests for
identical heap location, but such an operator would give different results
with different Haskell implementations and would be sensitive to
optimizations.  That would either be a horribly broken operator or (to fix
the brokeness) greatly constrain the avaliable optimizations and
implementation strategies.



For the problem at hand (involving the STLC), you will not be able to type
omega because omega is a non-normalizing closed term and STLC has the strong
normalization property.  You will have to move to a more expressive calculus
to type omega.


Rob Dockins
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Is there a notion for identity?

Tim Walkenhorst-2
Thanks for all infos.

I'll apply that Ref-datatype from the "observable sharing" paper
to my problem and see where this brings me. I'm also looking
into the solution Paul Hudak presented in the
"Detecting Cycles in Datastructures" thread in october.

> For the problem at hand (involving the STLC), you will not be able to type
> omega because omega is a non-normalizing closed term and STLC has the strong
> normalization property.  You will have to move to a more expressive calculus
> to type omega.

I guess the infinite omega-"type" I'm using is not a type in
the same way as infinity is not a number. You cannot reach it
by structural induction. Therefore the strong normalization
property will not work for infinite types (or none-types if
you prefer). I admit that allowing infinite types basically
means moving to a more expressive calculus. Probably the
best thing is to introduce the recursion operator mu explicitly
and avoid the cyclic structures. I just thought it would
be interesting to play around with infinite stuctures in this
context.

Thanks again,
Tim

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Is there a notion for identity?

Bugzilla from robdockins@fastmail.fm
On Monday 09 January 2006 04:09 am, Tim Walkenhorst wrote:

> Thanks for all infos.
>
> I'll apply that Ref-datatype from the "observable sharing" paper
> to my problem and see where this brings me. I'm also looking
> into the solution Paul Hudak presented in the
> "Detecting Cycles in Datastructures" thread in october.
>
> > For the problem at hand (involving the STLC), you will not be able to
> > type omega because omega is a non-normalizing closed term and STLC has
> > the strong normalization property.  You will have to move to a more
> > expressive calculus to type omega.
>
> I guess the infinite omega-"type" I'm using is not a type in
> the same way as infinity is not a number. You cannot reach it
> by structural induction.

Right.  This is something that seems to cause confusion for people
occasionally.  I myself didn't understand this subtle point until I did some
work with the with the proof assistant Coq which differentiates between
inductive and coinductive definitions.  Haskell datatypes are actually
coinductive, which are are related to sets of objects created by a maximal
fixpoint (rather than the more usual least fixpoint).  This means that
Haskell datatypes admit more values than their inductive cousins, and can
cause unintuitive results like this where you can create things that
"shouldn't exist" according to the literature, like a type for omega in STLC.

> Therefore the strong normalization
> property will not work for infinite types (or none-types if
> you prefer). I admit that allowing infinite types basically
> means moving to a more expressive calculus. Probably the
> best thing is to introduce the recursion operator mu explicitly
> and avoid the cyclic structures.

That would be my recommendation.  Cyclic datastructures bend my mind and tend
to be hard to work with; I personally try to avoid them except for a few
idiomatic uses involving lists.

> I just thought it would
> be interesting to play around with infinite stuctures in this
> context.
>
> Thanks again,
> Tim
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe