better nested inductive functions

Stream: lean4

[James Gallicchio]

I got annoyed writing mutual definitions for my nested inductive types, so I came up with this instead:

inductive Sexp
| atom : String → Sexp
| sexp : List Sexp → Sexp

def List.subtypeSize [SizeOf α] : (L : List α) → List {a : α // sizeOf a < sizeOf L}
| [] => []
| x::xs =>
  have : sizeOf x < sizeOf (x::xs) := by
    simp
    calc sizeOf x
      _ < sizeOf x + 1 := Nat.lt_succ_self _
      _ = 1 + sizeOf x := by rw [Nat.add_comm]
      _ ≤ 1 + sizeOf x + sizeOf xs := Nat.le_add_right _ _
  ⟨x, this⟩ :: xs.subtypeSize.map (fun ⟨a,h⟩ =>
    ⟨a, by
      simp
      calc sizeOf a
      _ < sizeOf xs := h
      _ ≤ 1 + sizeOf x + sizeOf xs := Nat.le_add_left _ _⟩)

def Sexp.toString : Sexp → String
| .atom s => s.quote
| .sexp ss =>
  let strings := ss.subtypeSize.map (fun ⟨s,h⟩ =>
    have : sizeOf s < 1 + sizeOf ss := Nat.le_trans h (Nat.le_add_left _ _)
    s.toString)
  "(" ++ String.intercalate "," strings ++ ")"
termination_by toString s => sizeOf s

which, to my eye, reads wayyyyy better than copying the definition of map in here.

this subtypeSize function can be derived from pmap and map. and in terms of overhead, hopefully pmap and runtime-idempotent map can eventually be stripped away by the compiler. thoughts?

[James Gallicchio]

(and, has this strategy for nested inductive definitions already been discussed somewhere?)

[James Gallicchio]

I also assume (?) that the nested inductive positivity requirement is related to having a LawfulFunctor instance -- is that true?

[Mario Carneiro]

There are non-strictly-positive inductives which have a lawful functor instance. I think the general connection you are looking for is described in the QPF paper Jeremy, Simon and I wrote a while back - http://www.contrib.andrew.cmu.edu/~avigad/Papers/qpf.pdf

[Lukas Stevens]

Is anyone working on this or planning to work on such a datatype package in the future?

[James Gallicchio]

Qpfs are in mathlib (docs#Qpf), but I don't think anyone is working on actually metaprogramming our way to nice coinductive and nested inductive types yet.

[Lukas Stevens]

I'm genuinely curious because as an Isabelle user I find this semantic approach quite elegant. The metaprogramming that is necessary in Isabelle, though, not so much. I imagine the more powerful logic of Lean makes the implementation more pleasant but it's still a lot of work to make it user friendly, of course.

[James Gallicchio]

That seems right. It's definitely doable, and not even too hard in Lean. But hard enough for me to not want to do it... I would definitely use it if someone implemented though :)

[James Gallicchio]

I think someone did start some metaprogramming, so maybe wait to see if Mario knows more about any partial work in that direction.

[Henrik Böving]

@Siddharth Bhat wants to eventually make the existing mutual and nested inductives nicer for his PhD

[Lukas Stevens]

Type theory or logic people might be especially interested in Bindings as Bounded Natural Functors, which is a way to bake binders into datatype definitions. A student that mainly Dmitriy and I supervised implemented this in Isabelle and is planning to use it to formalise type theory in Isabelle. Can QPFs support this as well?

[Mario Carneiro]

QPFs are very similar to BNFs, yes. I think the difference is that QPFs also support quotients, although it's been a while since I looked at this

[Sebastian Ullrich]

There's https://github.com/alexkeizer/QpfTypes by @Alex Keizer

[Alex Keizer]

Yes! It's still work-in-progress, and is a bit hard to work with since it depends on an outdated fork of Mathlib. If people are interested in it, I can put some effort into bringing that al up to date with the 4.0 release of Lean, and seeing if I can upstream the mathlib changes now that the port is over.

[Alex Keizer]

Also, feel free to ask me questions about it!

[Alex Keizer]

Lukas Stevens said:

Type theory or logic people might be especially interested in Bindings as Bounded Natural Functors, which is a way to bake binders into datatype definitions. A student that mainly Dmitriy and I supervised implemented this in Isabelle and is planning to use it to formalise type theory in Isabelle. Can QPFs support this as well?

You mean Jan van Brügge, right? I've spoken to him a few times. We haven't really dug into all the details, but it seems that QPFs are indeed similar enough that it would work.

[James Gallicchio]

do you have a sense yet of the runtime cost of building & matching data/codata compared to inductives?

[Lukas Stevens]

Alex Keizer said:

Lukas Stevens said:

Type theory or logic people might be especially interested in Bindings as Bounded Natural Functors, which is a way to bake binders into datatype definitions. A student that mainly Dmitriy and I supervised implemented this in Isabelle and is planning to use it to formalise type theory in Isabelle. Can QPFs support this as well?

You mean Jan van Brügge, right? I've spoken to him a few times. We haven't really dug into all the details, but it seems that QPFs are indeed similar enough that it would work.

Yes that was Jan.

[Alex Keizer]

James Gallicchio said:

do you have a sense yet of the runtime cost of building & matching data/codata compared to inductives?

Probably a bit worse. Especially codata's runtime behaviour could be optimized quite a bit more.
For data the biggest issue might be that data is stored in functions, which is probably not optimal either