Problem with continuations and typing

Previous Topic Next Topic
classic Classic list List threaded Threaded
1 message Options
Reply | Threaded
Open this post in threaded view

Problem with continuations and typing


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

(please see SFKT.hs) and

As we can see, FR stream indeed takes success and the failure
continuations. This is emphasized at the beginning of the first

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

Haskell-Cafe mailing list
[hidden email]