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