Guarded recursive types (by desugaring?)

Stream: general

[Sebastian Graf]

Hi folks,

Ever since I had to resort to Guarded Cubical Agda last year to type-check a denotational semantics that I wrote a paper about and thus had to prove total, I wondered if I could have pulled off the same in Lean, and in doing so would even have been able to execute the resulting definition as well as have a bit more proof automation at my disposal.

If you are interested in the work I did and are not an ICFP'24 reviewer, expand the following section:

Links

Agda code here, paper preprint here).

What would I need in Lean to do the same? Well, I really need guarded recursive types in order to define a type like

data D where
  stuck : D
  fun : (▹ D →  D) → D
  step :  ▹ D →  D

Note the negative occurrence of D in the fun constructor that I guard under the later modality ▹ .
This would be rejected as an inductive type or in the usual notion of coinductive type alike.
But since the later modality guards the negative occurrence, any f I give to constructor fun must promise to guard evaluation of its argument behind a suitably lazy data constructor (such as step).
As a result, the above definition of D exists as a guarded recursive type.
It was quite a joy to define the semantics in this framework, because extracting a runnable interpreter from this formulation is as easy as reading ▹ as "thunk" and erasing ▹ D to Unit → D. (In Haskell, I can simply omit ▹.) Although this is all based on cutting edge type theory, it is so very simple to think about and use, at least compared to using domain theory to prove that my definition exists for some complicated Scott domain encoding of D.

Proofs are a different matter though, and my experience to conduct these proofs in Guarded Cubical Agda were painful, probably not least due to my inexperience with interactive theorem proving in general and the quirks of working at the intersection of two niche features.

---

So I would really like to see guarded recursive types in Lean, and have thought a bit about the technicalities to achieve that. It was pretty clear to me that extending the language accepted by the Kernel is out of the question. So I came up with the following strategy:

1. Implement a useful Guarded Recursive Type Theory in the surface syntax. Which, I don't know; I guess the research dust has to settle a bit to see what sticks. I certainly lack the context to judge. But let me list a bit of starting points for a survey: Recent advances of applying guarded recursion to dependent type theory are Guarded Dependent Type Theory and The clocks are ticking! No more delays (introducing "CloTT"). Later works introduced Guarded Cubical Agda and finally its most recent incarnation of Ticked Cubical Type Theory, used here. I'm quite out of my depth here, but the use of Cubical types is mainly to support ergonomic encoding of powerdomains, I believe. Is there potential to just stick to, e.g., Guarded Dependent Type Theory and improve it? I don't know, but I hope so.
2. When elaborating surface syntax into a core term, desugar the type theory into a framework using step-indexing. Details below.
3. When producing IR for code generation, desugar ▹ D to Unit -> D, or Thunk D.

That way, we get efficient guarded recursive types without paying a complexity toll in the Kernel. (At least that is my very naïve hope.)

That said, the big wildcards are of course (1) and (2).
(1) I frankly cannot substantiate any more than I tried for lack of knowledge.
For (2), I have an idea for how to desugar ▹ D into more elemental inductive types.
I think an encoding based on step-indexing will do. For example, Jeremy Siek encodes step-indexed logic in Agda here. Here is the most relevant excerpt:

Blog

Our Step-indexed Logic (SIL) includes first-order logic (i.e., a logic
with "and", "or", "implies", "for all", etc.). To distinguish its
connectives from Agda's, we add a superscript "o". So "and" is written
×ᵒ, "implies" is written →ᵒ, and so on. SIL also includes a
notion of time in which there is a clock counting down. The logic is
designed in such a way that if a formula P is true at some time then
P stays true in the future (at lower counts). So formulas are
downward closed. When the clock reaches zero, every formula becomes
true. Furthermore, the logic includes a "later" operator, written ▷ᵒ P, meaning that P is true one clock tick in the future. When we use
SIL to reason about the cast calculus, one clock tick will correspond
to one reduction step.

Just as Set is the type of true/false formulas in Agda, Setᵒ is
the type of true/false formulas in SIL. It is a record that bundles
the formula itself, represented with a function of type ℕ → Set,
with proofs that the formula is downward closed and true at zero.

record Setᵒ : Set₁ where
  field
    # : ℕ → Set
    down : downClosed #
    tz : # 0                -- tz short for true at zero
open Setᵒ public

For example, the "false" proposition is false at every time except zero.

⊥ᵒ : Setᵒ
⊥ᵒ = record { # = λ { zero → ⊤ ; (suc k) → ⊥ }
            ; down = ... ; tz = ... }

The result is basically a library for defining and using guarded recursive types, but one that indexes all finite prefixes of an infinite coinductive value, rather than encoding the coinductive value first class, so it's not really suitable for execution. I guess this is also what was discussed in the following thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.E2.9C.94.20Efficient.20coinduction/near/298282159 and this SO: https://mathoverflow.net/questions/407964/coinduction-for-all/408509#408509 (kudos @Marc Huisinga)

Perhaps (quite probably) the concrete idea I proposed isn't so easily possible. But Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory should yield such a (perhaps complicated?) desugaring; to desugar, run the denotational semantics and embed its semantic domain as ordinary core term.

I pitched this idea to @Jakob von Raumer who suggested I reach out to the community to see whether people have been working in this direction already.

[Max Nowak 🐉]

At risk that I may not have understood what you're trying to do in sufficient depth: It sounds like guarded recursive types can be reduced to Lean's mutually inductive types. If you can define a "Syntax" (in the sense of the paper linked below) for guarded recursive types, and a reduction from that syntax to the syntax of mutually inductive types, then together with a semantics for mutually inductive types in Lean you also gain a semantics for your guarded recursive types. Maybe. I haven't fully thought it through.

[Enrico Borba]

Similarly I don't understand completely what you're trying to do, but I have a question: What is a negative type ▹ D? I see that you've said it can be erased to Unit → D, but this is equivalent to just identifying some element in D, which is just equivalent to D no?

[Edward van de Meent]

it might be equivalent, but not definitionally equal, which is precisely the difference that this is supposed to emphasise i think? i could be wrong though...

[Sebastian Graf]

a reduction from that syntax to the syntax of mutually inductive types

Yes, that is what I hope exists. I mean, if Lean can embed step-indexed logical relations as in the linked blog post (which is likely), it should be able to embed some flavour of guarded recursive types as well, at which point it is just a matter of offering good syntactic sugar in the source language (hopefully!).

What is a negative type ▹ D?

I didn't mean to say that ▹ D is a "negative type", so let me try again.
In the recursive type equation D = ▹ D -> D, the occurrence of D under ▹ is negative because it occurs to the left of an uneven number of (->). More formally, each recursively defined type gives rise to a signature functor such as, in this case, F a = ▹ a -> a, and D is the (guarded) fixed-point of this functor. Inductive types do not allow such negative recursive occurrences; an inductive type such as data T where MkT : (T -> T) -> T would be forbidden because a similar type can be exploited to recover general recursion (and thus violating strong normalisation of the type theory).
Common notions of coinductive types do not allow negative recursive occurrences either. But guarded recursive types allow negative occurrences, as long as they are guarded, by the later modality ▹ . That's tremendously useful to define dynamic processes such as transition systems, reactive systems (FRP), server processes, etc..

Once you have type-checked your program and proofs, it's OK to execute ▹ D as if it was Thunk D, ostensibly reintroducing the negative occurrence. That is because guarded recursive types guarantee that all programs that passed the type-checker must terminate when desugared this way.

Have a look at https://bentnib.org/productive.pdf to see how guarded recursive types might be useful in programming.
More recent guarded recursive type systems allow for more programs to be typed (in particular ones with negative occurrences, in contrast to this rather early paper). The same paradigm can be used to define efficient functional-reactive programming frameworks, as requested here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.E2.9C.94.20Efficient.20coinduction/near/298282159. Concretely, you could define (forgive my incorrect lean syntax)

data SF (α β : Type) : Type
| succ : (α → β) → (α → ▹  SF) → SF

ones : SF Unit Nat
ones = succ (fun _ => 1) (fun _ => ones)

ones encodes an infinite stream of 1.
Note that ones would never be possible as an inductive definition, because its recursive invokation does not decrease in any of its 0 arguments.
But guarded recursive types provide us with a nearly-general fixpoint combinator fix : (▹ α -> α) -> α, and the definition of ones above makes implicit use of that: the recursive occurrence of ones has type ▹ (SF Unit Nat), as this fixpoint combinator requires.
Obviously there are more interesting, higher-order types than this, such as my D from the OP.

[Jannis Limperg]

I don't have any concrete thoughts, but if you do embark on this journey, please think about defeq from the beginning. In DTT, it's very important that your encoding has the right definitional, not just propositional equations. This is, I believe, one reason why data type packages like Isabelle's have never caught on in DTT land, despite their conceptual advantages.

[Mario Carneiro]

Sebastian Graf said:

In the recursive type equation D = ▹ D -> D, the occurrence of D under ▹ is negative because it occurs to the left of an uneven number of (->). More formally, each recursively defined type gives rise to a signature functor such as, in this case, F a = ▹ a -> a, and D is the (guarded) fixed-point of this functor. Inductive types do not allow such negative recursive occurrences; an inductive type such as data T where MkT : (T -> T) -> T would be forbidden because a similar type can be exploited to recover general recursion (and thus violating strong normalisation of the type theory).

Just a note: Lean is already not strongly normalizing, this is not the problem. The problem is that such an inductive type would be unsound: you can use it to prove False. So the key question is: why are guarded inductive types not unsound in the same sense? And what is ▹ anyway?

[Mario Carneiro]

Sebastian Graf said:

ones encodes an infinite stream of 1.

How do you know this? Can you prove it, and if so what would the proof look like?

[Mario Carneiro]

What are the reasoning principles associated with ▹?

[Sebastian Graf]

why are guarded inductive types not unsound in the same sense?

There is a constructive encoding of this type theory in terms of the topos of trees, explicitly allowing these negative occurrences. See also https://arxiv.org/pdf/1611.09263.pdf:

Guarded recursive types with negative variance. A key feature of guarded recursive types
are that they support negative occurrences of recursion variables. This is important for applications
to models of program logics [ 7].

Of course, the type system restricts the way in which parameters of type ▹ D might be used; otherwise you would indeed be able to prove False.

And what is ▹ anyway?

See any of the work I cited; the definition varies. Later works define it in terms of Clock variables; sort of ▹ A = Nat -> A but properly restricted (downwards closed, etc.)

How do you know this? Can you prove it, and if so what would the proof look like?

I cannot prove it, for multiple reasons: It is not a well-formed program (yet?), it is not fully elaborated, I lack the formal background. But what I do know is: I want to write programs (and perhaps proofs) in this framework!

What are the reasoning principles associated with ▹?

I would have to delegate to one of the papers, such as The clocks are ticking! No more delays. Or the implementation in Guarded Cubical Agda. Perhaps my use of it here is helpful as well: https://github.com/sgraf812/abs-den/blob/main/agda/Semantics.agda. This is the trusted "Prelude" of Guarded Cubical Agda: https://github.com/sgraf812/abs-den/blob/main/agda/Later.agda, defining the Later modality among other things.

[Mario Carneiro]

My impression regarding clocked stuff is that this is actually a definition by recursion, not induction

[Mario Carneiro]

recursion has no restrictions regarding the recursive use appearing positively or anything like that, but they must occur at smaller arguments (= "later")

[Mario Carneiro]

However the missing thing here seems to be the base case, without which I think you are still in soundness trouble. If I define P := (▹ P -> False), is P inhabited or not?

[Mario Carneiro]

Sebastian Graf said:

How do you know this? Can you prove it, and if so what would the proof look like?

I cannot prove it, for multiple reasons: It is not a well-formed program (yet?), it is not fully elaborated, I lack the formal background. But what I do know is: I want to write programs (and perhaps proofs) in this framework!

Figuring out the answer to this question is a prerequisite for being able to define this framework, whether by a custom type checker or by a desugaring. You have to know what the desugaring is before you can write it in code

[Sebastian Graf]

As I said, I lack much of the formal background to give an informed answer to many of your questions.
I can answer this question, however:

If I define P := (▹ P -> False), is P inhabited or not?

Your P is indeed a well-formed guarded recursive type. But I'm pretty confident that it is not inhabited, for if there exists p : P, I can do p (later p) : False (where later : α -> ▹ α is the pure implementation of the Applicative instance of ▹).

It is not so hard to give a library implementation of ▹; Basically, any Type involving ▹ is mapped to Type' := Nat -> Type with a few restrictions, as outlined in the linked blog post, cf. Setᵒ:

downClosed :  (t : Type') -> (n : Nat) -> t (n+1) -> t n
bot : (t : Type') -> t 0
▹ : Type' -> Type'
(▹ A) 0 = Unit
(▹ A) (n+1) = (▹ A) n
later : A ->  ▹ A   -- I'm a bit doubtful this definition checks, but I hope you get the idea
later f 0 = unit
later f (n+1) = f n

So every Type' (even the lifting of False) starts out as inhabited at step/fuel 0. Presumably that is the "base case" that you wondered about? The blog post compares to induction on natural numbers, observing

In the world of [step-indexed logic], propositions are always true at zero, so the base case P 0 is not necessary.

To me, the point of this theory is that the step indices are completely hidden behind clock variables, and my hope is that clock variables can be erased for code generation.

If you want to see how the ones example is elaborated in detail, I suggest you look at "Section IV: EXAMPLE: PROGRAMMING WITH STREAMS" of https://pure.itu.dk/ws/portalfiles/portal/82163359/bahr17lics_paper.pdf, specifically the const function (which generalises ones). (Why isn't this Section 2 ...) Streams are simpler than signal functions SF, but I hope you can see that a similar elaboration is possible for the hypothetical Lean program ones.