Continuations

[mnieper]

I will comment on the two issues that I think are most important first:

We also have to decide in which way we want to model I/O in a pure language.

I'd prefer to leave it in Scheme, at least for now. This ties in with streams, which tie in with data/codata.

Handling I/O in Scheme means that the Scheme procedures we want to call will be necessarily impure (because I/O is called for side effects). We therefore have to isolate this bit of impurity as otherwise impurity will creep into the whole language. So, we don't win much by pushing I/O on the other side of the FFI border.

In order to fence in the impurity from I/O, any I/O procedure can be modeled as a function T x World -> S x World, which conceptually states the world interface. The type system can the hide the World state in a monad or use some other tricks to make it more pleasant to use, but the underlying mechanism wouldn't change. Any foreign Scheme procedure that does I/O will have to be typed using the World type, at least implicitly.

Of course, just having a World type is not enough. The type system has to forbid that World states can be shared, but is only used in an at most linear fashion. In Haskell, this is done by hiding it in the I/O monad. In Clean, this is done through uniqueness types.

So the upshot is this: Whether I/O is done by Scheme or Steme procedures/functions does not answer the question how I/O is modeled in a pure language or how we want to model it.

There are two issues here. Scheme has resumable exceptions in the form of raise-continuably. However, the proof obligation imposed on a Steme programmer when some random Scheme exception handler is at the top of the stack that it will return a value of a particular type will, I think, be too difficult. In general, calling unknown first-class procedures is tricky because you don't know what you are targeting, and especially for a construct meant to operate across abstraction boundaries. So let's say we confine ourselves to raise only.

Because it is an effect. See pp. 31-34 of "Tackling the Awkward Squad" for better explanations than I can give. In brief, though: what is the type of (throw x1) + throw(x2)? It depends on the order of evaluation, which is something neither Haskell nor Scheme (nor indeed C) guarantees, though CL and Java do. By returning an imprecise exception, something that might have type x1 or x2, you can throw exceptions anywhere but can catch them only in the IO monad, where indeterminacy is expected.

Forbidding raise-continuable would be throwing the baby out with the bathwater, I think. For a returning raise-continuation, the situation is not different to calling some function that is bound in the dynamic environment. If the handling of the exception reaches across the interface between Steme and Scheme, it is as if we bind a Scheme procedure in the dynamic environment, which has to be associated some type as it is with all FFI procedures.

As for raise, there isn't a problem if it is modeled correctly: In a lazy language like Haskell, when started, the program receives (conceptually) a world state value. The typing system guarantees that this value will be used at most once. In a strict language, which is dual, the initial world state value becomes under duality a final continuation that accepts a world state. The only way to halt the program is to finally call this final continuation. Here, the typing system has to guarantee that the world state when delivered to the final continuation hasn't been used more than once.

Now raise may terminate a program, so it needs a world state as otherwise it cannot, eventually, pass to the final continuation. Thus, code like (+ (raise x1) (raise x2)) won't be accepted by the type checker as the world state would have to be duplicated. In other words, raise is like an I/O procedure in that it takes a world state. It doesn't deliver a value, though, because it is a continuation. Those parts of Steme that potentially raise exceptions therefore have to be declared at such and will be handled in a definite sequential order.

The procedure raise-continuable is different. It doesn't need a world state because it returns.

Originally posted by @mnieper in https://github.com/pre-srfi/static-scheme/issues/1#issuecomment-722932879

[mnieper]

As I argued above, the final continuation (or primordial, if you want) should accept a world state so that purity can be preserved while allowing side effects (e.g. due to direct I/O or calling impure Scheme procedures). This implies that Scheme's call/cc, whose classical (polymorphic) type is ((α → β) → α) → α would become a call/cc with type ((World → α → β) → α) → α. In other words, the continuation has to be passed the world state because the continuation will eventually reach the final one.

This makes delimited continuations all the more so attractive because a delimited continuation is, well, delimited, and doesn't extend to the final state of the program. It's interesting to see how clear the difference between the two concepts becomes in this context.

[arvyy]

Handling I/O in Scheme means that the Scheme procedures we want to call will be necessarily impure

Alternatively it could mean that for IO, the calls would always be initiated on Scheme side, which would collect input in impure ways and pass them to pure side of Steme. This could be seen as explicit implementation of "Functional core, Imperative shell" philosophy (eg. https://www.destroyallsoftware.com/talks/boundaries). Feasibility of such approach would largely depend on painless ability to intermix Scheme/Steme alot in same software semantic unit.

[mnieper]

Handling I/O in Scheme means that the Scheme procedures we want to call will be necessarily impure

Alternatively it could mean that for IO, the calls would always be initiated on Scheme side, which would collect input in impure ways and pass them to pure side of Steme. This could be seen as explicit implementation of "Functional core, Imperative shell" philosophy (eg. https://www.destroyallsoftware.com/talks/boundaries). Feasibility of such approach would largely depend on painless ability to intermix Scheme/Steme alot in same software semantic unit.

This would mimic the Haskell I/O monad, wouldn't it? The "Scheme shell" would be what happens in the I/O monad.

That's a reasonable approach but it reduces the applicability of pure Steme code.

[johnwcowan]

That is the approach I favor, with a major exception: Steme can call Scheme, as Haskell can call C, IF (a) the Steme programmer type-annotates the Scheme call AND (b) the Steme programmer can prove (outside the system) that the Scheme procedure is pure.

I think that the best use of @lassik's the (which comes from CL) is to annotate Steme calls: (the String (some-function)), for example, is a guarantee to the Steme compiler that some-function is pure and returns a String. It's a little more awkward in English, but it can be extended to (the (type ...) expression) when multiple values are expected.

In addition, arguments have to be annotated as well, so if we use the here also, we get (the Set (set-xor (the Set a) (the Set b)). Of course, most of the time the Steme types of a Scheme procedure are always the same, so we also allow a global declaration like (define-the Quaternion (quaternion-add (the Quaternion) (the Quaternion)), but only to save typing (now you can say simply (quaternion-add a b)) and to help with consistency (defining in every place explicitly risks missing one if the type needs to be changed. Being able to wrap arguments and calls to Scheme procedures is logically sufficient. (If the expression is a Steme one, then the is just a consistency check at compile time. I think.

[lassik]

It's important to make a distinction between three kinds of annotations:

• Optional type (type inference works fine without, but can infer a confusing type, or the user wants to type it for documentation)
• Required (type system can't figure something out by itself and needs help from the user)
• Assumed (user promises that some FFI function has the given type)

In the first two cases, the type system always notices at compile time if the user gives a type that won't work.

In the third case, the type system trusts that the user gave the correct type but cannot check. Big difference.

I'd favor a separate annotation keyword for assumed types.

[lassik]

We could have something like Gambit's (c-lambda (input-type ...) output-type body) for the FFI.

[lassik]

If the language is restricted so that FFI procedures always come from a Scheme library, then there's no need to put any FFI annotations in a static library. They can be put where the import or export is.

[johnwcowan]

Global declarations of Scheme procedures should go in define-steme-library forms.

[mnieper]

This original question of this thread, namely how to implement (and type) raise and call/cc in a pure language seemed to have been hijacked. Please let's use this thread for the original topic (which should resolved one way or the other) and open another issue for the rest.

[lassik]

Unfortunately GitHub doesn't seem to have a feature to move comments from one issue to another. I've missed that plenty of times.

[mnieper]

I am closing this issue for the time being as I think the algebraic effect handlers as discussed in #19 are a much better alternative compared with Haskell's monads or the approach of threading a world state through the impure parts of the program and relying on uniqueness typing for the world state. Contrary to these approaches, algebraic effects are modular and separate interface from implementation. By default, algebraic effect handlers support delimited continuations. call/cc could be added (it would probably have to yield an operator), but I could live without call/cc when we have delimited continuations as these seem to be enough to model everything useful first-class continuation are usually used for.