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

Tim Walkenhorst tim.walkenhorst at gmx.de
Mon Jan 9 04:09:32 EST 2006


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



More information about the Haskell-Cafe mailing list