[Haskell-cafe] Problem with continuations and typing

[oleg at pobox.com]

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'.