2 ms·

It's not in the abstract, but towards the end of the paper: > Our analysis suggests that the language of A-normal forms is a good intermediate representation f

by mrkeen 3y ago

It's not in the abstract, but towards the end of the paper: > Our analysis suggests that the language of A-normal forms is a good intermediate representation for compilers. I messed around with both CPS and ANF transforms for a while. Here are more approachable treatments of them: https://matt.might.net/articles/by-example-continuation-passing-style/ https://matt.might.net/articles/a-normalization/ I wasn't sure which one I'd end up using. I suspected CPS would make it easier to do tail-call optimisation, which is very important to me. But once I implemented CPS, I found I could not figure out how to assign a type to the continuation term that CPS introduces. I had no such typing problem with ANF, so that's what I continued with. I haven't tried the tail-call optimisation in ANF yet.

k_g_b_ 3y ago
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 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 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 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/1309.1257, https://arxiv.org/abs/1409.3313 https://arxiv.org/abs/1409.3313) with no other follow up.

by mrkeen 3y ago

k_g_b_ 3y ago

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 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 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 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/1309.1257, https://arxiv.org/abs/1409.3313 https://arxiv.org/abs/1409.3313) with no other follow up.