The problem with typing continuations -in my opinion - stems from the fact that nearly all discussion of continuation starts from a functional context/view/programming language and often also in an untyped language/formalism.
Additionally, CPS ends with "style" suggesting that it's fully expressible in the original programming language. But if we truly type it after a style transformation we need to introduce polymorphism everywhere, see e.g. the first example for Haskell on https://en.m.wikipedia.org/wiki/Continuation-passing_style
If we use CPS as an IR, typing the continuations as functions is wrong and unnecessary - a continuation does not return anything and more precise: it does not return. This means it's type is constructed just from it's argument type(s). In an IR we can simply add constructs for continuations and their types.
A lambda \x:Nat.5 has type Nat -> Nat, or in one non-infix syntax: ΠNat.Nat (https://en.m.wikipedia.org/wiki/Lambda_cube). A continuation c with argument Nat simply has type `Cont Nat` a type constructor taking the argument type.
A `Cont Nat` isn't something you would see in a CPS IR, because it's mostly useless: it's type describes a computation that takes an argument and then diverges. The only place such a continuation has, would be as the single `exit` continuation of the program provided to the main entry point of the program. More useful is e.g. a `Cont (Nat, Cont Bool)` and this brings us the "passing" part of CPS.
Some like to use the syntax `Nat -> !` and that highlights the non-returning nature, but I think this is again too confusing in the context of functional programming - just leave out the `->`.
See also https://okmij.org/ftp/continuations/undelimited.html and note that it argues that the untyped call/cc operator might be the origin of the confusion: it represents the captured continuation as a function and a continuation also has an application operation like a function, but it's semantics are different.
As far as I can tell, there's very few formal treatments of continuations that don't start from the lambda calculus. The only two papers I've found are on the Continuation Calculus (https://arxiv.org/abs/1309.1257, https://arxiv.org/abs/1409.3313) with no other follow up.
Additionally, CPS ends with "style" suggesting that it's fully expressible in the original programming language. But if we truly type it after a style transformation we need to introduce polymorphism everywhere, see e.g. the first example for Haskell on https://en.m.wikipedia.org/wiki/Continuation-passing_style
If we use CPS as an IR, typing the continuations as functions is wrong and unnecessary - a continuation does not return anything and more precise: it does not return. This means it's type is constructed just from it's argument type(s). In an IR we can simply add constructs for continuations and their types.
A lambda \x:Nat.5 has type Nat -> Nat, or in one non-infix syntax: ΠNat.Nat (https://en.m.wikipedia.org/wiki/Lambda_cube). A continuation c with argument Nat simply has type `Cont Nat` a type constructor taking the argument type.
A `Cont Nat` isn't something you would see in a CPS IR, because it's mostly useless: it's type describes a computation that takes an argument and then diverges. The only place such a continuation has, would be as the single `exit` continuation of the program provided to the main entry point of the program. More useful is e.g. a `Cont (Nat, Cont Bool)` and this brings us the "passing" part of CPS.
Some like to use the syntax `Nat -> !` and that highlights the non-returning nature, but I think this is again too confusing in the context of functional programming - just leave out the `->`.
See also https://okmij.org/ftp/continuations/undelimited.html and note that it argues that the untyped call/cc operator might be the origin of the confusion: it represents the captured continuation as a function and a continuation also has an application operation like a function, but it's semantics are different.
As far as I can tell, there's very few formal treatments of continuations that don't start from the lambda calculus. The only two papers I've found are on the Continuation Calculus (https://arxiv.org/abs/1309.1257, https://arxiv.org/abs/1409.3313) with no other follow up.