Jerzy Karczmarczuk wrote:

I tried to cook-up a simple version of nondeterministic computations using the two-continuation model. I got stuck on an 'infinite type' error, and my question is: have you seen a *concrete* (really concrete) Haskell implementation of a similar model, I could inspire myself on? (I know a few theoretical works on that).

Yes, of course: the code for the LogicT paper http://pobox.com/~oleg/ftp/packages/LogicT.tar.gz (please see SFKT.hs) and http://www.haskell.org/pipermail/haskell/2005-October/016577.html http://www.haskell.org/pipermail/haskell/2005-October/016696.html As we can see, FR stream indeed takes success and the failure continuations. This is emphasized at the beginning of the first article.

But I would like to continue this exercice along these lines, without too much exotism (no monads, yet...), for my students. Do you have any simple work-around Introduce some algebraic constructors? Perhaps higher-rank polymorphism could do something (but then I would have to explain it to my folk...)

You're correct on both counts. We can emulate equi-recursive types with iso-recursive ones: e.g., plain Haskell list. Or, you may choose to use higher-ranked type (the FR stream). There is a third solution: use a small typing hole in Haskell to sneak in the real equi-recursive type. I have a feeling though you might not wish to explain the latter method to your students. This present question is actually related to your previous inquiry about expressing a predecessor in a simply-typed lambda-calculus. It cannot be expressed. We need either a recursive or higher-ranked type: predecessor is 'car'.