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

[Robert Dockins]

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