Stream: Coq users

Topic: Continuations in coq


view this post on Zulip Julin S (Apr 04 2023 at 07:54):

How are continuations usually represented in coq?

Saw here that throwas 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.

view this post on Zulip Julin S (Apr 04 2023 at 08:02):

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.

view this post on Zulip Paolo Giarrusso (Apr 04 2023 at 10:29):

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

view this post on Zulip Julin S (Apr 05 2023 at 04:11):

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 *)

view this post on Zulip Paolo Giarrusso (Apr 05 2023 at 09:19):

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).

view this post on Zulip Paolo Giarrusso (Apr 05 2023 at 09:21):

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.

view this post on Zulip Paolo Giarrusso (Apr 05 2023 at 09:22):

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

view this post on Zulip Paolo Giarrusso (Apr 05 2023 at 09:25):

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