<p>I was trying to implement algebraic effects in my language, but I was caught into the same problem that some papers about CPS try to solve in a expression like <code>shift (k -&gt; k)</code>: I can't return a continuation that is polymorphic in the return type like a <code>raise : String -&gt; {Exception} a</code> because that would create a continuation of type <code>forall a. a -&gt; T</code> where T is type of the scrutinee of the handler. I cannot assume that <code>a</code> is a variable open to unification because it would be wrong, but if I assume that it's a skolem and return the continuation, the skolem would go out of context.</p>

<types><effect-systems>
How to give a type to a continuation that is polymorphic in the parameter?
<p>First, some terminological quibbles about the phrasing of your question. You write</p>
<blockquote>
<p>I can't return a continuation that is polymorphic in the return type like a <code>raise : String -&gt; {Exception} a</code></p>
</blockquote>
<p>but this is not correct. An operation like <code>raise</code> is very much <em>not</em> a continuation, it is an algebraic operation.</p>
<p>However, I imagine that what you mean is that the continuation <em>of</em> an operation like <code>raise</code> may expect to receive a value of any type. This is true, but this does not mean that the continuation should be similarly universally quantified! In fact, that would be the opposite of correct, and this is not at all unique to algebraic effects. We can see precisely the same duality with an ordinary (higher-rank) function that uses <a href="https://en.wikipedia.org/wiki/Continuation-passing_style" rel="noreferrer">continuation-passing style</a>:</p>
<pre class="lang-hs prettyprint-override"><code>f :: (forall a. String -&gt; (a -&gt; T) -&gt; T) -&gt; T
f raise = raise &quot;bang&quot; (\x -&gt; g (x + 1))
</code></pre>
<p>The implementor of this function may instantiate <code>raise</code> at any type, so the caller will receive a continuation with an argument type that is <em>existentially</em> quantified, not universally quantified. That is, if we write</p>
<pre class="lang-hs prettyprint-override"><code>f (\msg k -&gt; ...)
</code></pre>
<p>then <code>k</code> essentially has type <code>exists a. a -&gt; T</code> within the body of the lambda. Of course, it is impossible to ever call such a function, as <code>a</code> could be absolutely anything, so it might as well be uninhabited. This difference in perspective is essentially a <a href="https://en.wikipedia.org/wiki/Covariance_and_contravariance_(computer_science)" rel="noreferrer">variance</a> issue.</p>
<p>How precisely you choose to typecheck such uses depends on the nature of your type system. If your language directly supports existential quantification, you could perhaps give the continuation an existential type directly. However, many languages do not directly support existential quantification, so it must be encoded some other way. You allude to <a href="https://en.wikipedia.org/wiki/Skolem_normal_form" rel="noreferrer">skolemization</a> in your question, which is a perfectly legitimate approach here. You write</p>
<blockquote>
<p>I assume that it's a skolem and return the continuation, the skolem would go out of context.</p>
</blockquote>
<p>but there is no reason that this must be true. If you consider typechecking a call to <code>f</code> defined above, the skolem is scoped to the lambda passed to <code>f</code>. Likewise, the skolem introduced to represent this existential in an algebraic effect handler must be scoped to the handler itself.</p>

CC BY-SA 4.0
2023-08-13T19:59:18.673Z
2023-08-13T20:08:44.730Z
2023-08-13T20:08:44.730Z
Alexis King
# How to give a type to a continuation that is polymorphic in the parameter?
Posted by: username_0 on 2023-08-13
I was trying to implement algebraic effects in my language, but I was caught into the same problem that some papers about CPS try to solve in a expression like `shift (k -> k)`: I can't return a continuation that is polymorphic in the return type like a `raise : String -> {Exception} a` because that would create a continuation of type `forall a. a -> T` where T is type of the scrutinee of the handler. I cannot assume that `a` is a variable open to unification because it would be wrong, but if I assume that it's a skolem and return the continuation, the skolem would go out of context.
**Tags:** types effect-systems
---
## 1 answers
### Answer by username_1 on 2023-08-13. Score: 6 | Accepted answer
First, some terminological quibbles about the phrasing of your question. You write

I can't return a continuation that is polymorphic in the return type like a raise : String -> {Exception} a

but this is not correct. An operation like raise is very much not a continuation, it is an algebraic operation.
However, I imagine that what you mean is that the continuation of an operation like raise may expect to receive a value of any type. This is true, but this does not mean that the continuation should be similarly universally quantified! In fact, that would be the opposite of correct, and this is not at all unique to algebraic effects. We can see precisely the same duality with an ordinary (higher-rank) function that uses continuation-passing style:
f :: (forall a. String -> (a -> T) -> T) -> T
f raise = raise "bang" (\x -> g (x + 1))

The implementor of this function may instantiate raise at any type, so the caller will receive a continuation with an argument type that is existentially quantified, not universally quantified. That is, if we write
f (\msg k -> ...)

then k essentially has type exists a. a -> T within the body of the lambda. Of course, it is impossible to ever call such a function, as a could be absolutely anything, so it might as well be uninhabited. This difference in perspective is essentially a variance issue.
How precisely you choose to typecheck such uses depends on the nature of your type system. If your language directly supports existential quantification, you could perhaps give the continuation an existential type directly. However, many languages do not directly support existential quantification, so it must be encoded some other way. You allude to skolemization in your question, which is a perfectly legitimate approach here. You write

I assume that it's a skolem and return the continuation, the skolem would go out of context.

but there is no reason that this must be true. If you consider typechecking a call to f defined above, the skolem is scoped to the lambda passed to f. Likewise, the skolem introduced to represent this existential in an algebraic effect handler must be scoped to the handler itself.
---
