[Haskell-cafe] Is there a notion for identity?
Robert Dockins
robdockins at fastmail.fm
Mon Jan 9 17:30:11 EST 2006
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
More information about the Haskell-Cafe
mailing list