How are continuations usually represented in coq?

Saw here that `throw`

as in sml won't be possible in coq.

Yet there are lot of works with coq which deal with cps. (Tried going through a few, but couldn't make head or tail out of them..)

How is it usually done?

I was trying to convert STLC to an equivalent CPS form.

I was trying to replicate the coq code from this.

STLC part looks something like:

```
Inductive type :=
| Bool: type
| Arrow: type -> type -> type.
Section stlc.
Context {V:type->Type}.
Inductive term : type -> Type :=
| Var: forall {t:type}, V t -> term t
| App: forall {t1 t2:type},
term (Arrow t1 t2) -> term t1 -> term t2
| Abs: forall {t1 t2:type},
(V t1 -> term t2) -> term (Arrow t1 t2)
| Tru: term Bool
| Fls: term Bool.
End stlc.
Arguments term: clear implicits.
```

One must refine the question to answer it — Gallina doesn't support continuations natively, but that doesn't stop you from formalizing an _object_ language with continuations

Could this be considered a form of cps? A random toy example.

```
Inductive op : Type :=
| Add: nat -> nat -> op
| Mul: nat -> nat -> op.
Inductive term : Type :=
| Halt: nat -> term
| Bind: op -> (nat -> term) -> term.
(*
(2+3) * (4+5)
*)
Example eg1 : term :=
Bind (Add 2 3) (fun x=>
Bind (Add 4 5) (fun y=>
Bind (Mul x y) (fun z=>
Halt z))).
Definition opDe (o:op) : nat :=
match o with
| Add x y => x + y
| Mul x y => x * y
end.
Fixpoint termDe (t:term) : nat :=
match t with
| Halt r => r
| Bind o k => termDe (k (opDe o))
end.
Compute termDe eg1. (* = 45 : nat *)
```

That's CPS, but I don't think this term qualifies as "syntax", it's rather a mix of syntactic terms and semantic values — not even as a form of HOAS: the function takes a value, not a term, and it's too easy to write, say, Bind (Add 2 2) (fun x => Add (x + 2) 4).

Who cares? This is a subtle subject, but when manipulating this program, you wouldn't be able to pattern-match on the (x + 2) syntax, since you can only match on syntax you define with inductives, not on Coq terms.

In fact, you'd even struggle to visit the function argument of Bind; in HOAS it's possible.

As a concrete test: if you want to define syntax that you can use for metaprogramming (say, program transformations, non-standard interpreters, syntactic proofs) you should be able to also write a pretty-printer.

Last updated: Jun 13 2024 at 04:03 UTC