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: Oct 13 2024 at 01:02 UTC