## Stream: general

### Topic: Dependently Typed Folds for Nested Data Types

#### Sean Leather (Jul 05 2018 at 13:24):

@Sebastian Ullrich wrote:

With nested and mutual inductives moving into the kernel, there shouldn't be any need for an abstraction layer. Well, it's still not clear how nested inductives would be represented.

Would this paper help?

We present an approach to develop folds for nested data types using dependent types. We call such folds dependently typed folds, they have the following properties. (1) Dependently typed folds are defined by well-founded recursion and they can be defined in a total dependently typed language. (2) Dependently typed folds do not depend on maps, map functions and many terminating functions can be defined using dependently typed folds. (3) The induction principles for nested data types follow from the definitions of dependently typed folds and the programs defined by dependently typed folds can be formally verified. (4) Dependently typed folds exist for any nested data types and they can be specialized to the traditional higher-order folds. Using various of examples, we show how to program and reason about dependently typed folds. We also show how to obtain dependently typed folds in general and how to specialize them to the corresponding higher-order folds.

#### Sebastian Ullrich (Jul 05 2018 at 15:33):

@Sean Leather This seems to be about a different kind of nested types. Note that Bush cannot even be defined in Lean 3 because of universe constraints.

#### Sean Leather (Jul 05 2018 at 15:35):

What are the nested inductives that you're referring to?

#### Sebastian Ullrich (Jul 05 2018 at 15:36):

And conversely, the type Term from the first case study is just a regular inductive type according to Lean. I didn't compare the induction principles, though.

#### Sebastian Ullrich (Jul 05 2018 at 15:40):

@Sean Leather Any inductive type that is passed to another inductive type in its own definition, as in https://github.com/leanprover/lean/wiki/Inductive-datatypes#encoding-datatypes-that-contain-recursive-occurrences-nested-in-existing-datatypes

#### Sean Leather (Jul 05 2018 at 15:45):

Ok, right. That's the "simple" version of nested data types.

#### Mario Carneiro (Jul 06 2018 at 01:16):

Note that Bush cannot even be defined in Lean 3 because of universe constraints.

Actually this is an instance of non-uniform parameters, which I have figured out how to simulate in lean without any kernel extensions

#### Sean Leather (Jul 06 2018 at 05:49):

Actually this is an instance of non-uniform parameters, which I have figured out how to simulate in lean without any kernel extensions

@Mario Carneiro Please do share. Can you define a Bush type from constants?

#### Mario Carneiro (Jul 06 2018 at 05:49):

what do you mean from constants?

#### Sean Leather (Jul 06 2018 at 05:53):

I mean the sort of constants generated by the equation compiler.

#### Sean Leather (Jul 06 2018 at 05:54):

Err, maybe I'm using the wrong terminology. What do you call the process of taking an inductive to its constants?

#### Mario Carneiro (Jul 06 2018 at 06:11):

the constructors?

#### Mario Carneiro (Jul 06 2018 at 06:12):

To be precise, I can define a type Bush together with constructors of the stated types, the natural recursion principle, and a computation rule (as a provable equality, not definitional) while circumventing any universe inconsistencies

#### Sean Leather (Jul 06 2018 at 06:16):

To be precise, I can define a type Bush together with constructors of the stated types, the natural recursion principle, and a computation rule (as a provable equality, not definitional) while circumventing any universe inconsistencies

Yes, that's what I'd like to see.

#### Mario Carneiro (Jul 06 2018 at 08:35):

I think I will just give a rough sketch:

inductive {u} bushn (α : Type u) : nat → Type u
| zero : α → bushn 0
| nil {n} : bushn (n+1)
| cons {n} : bushn n → bushn (n+2) → bushn (n+1)

def bush (α : Type*) := bushn α 1

def bushn.equiv (α : Type*) : ∀ n : ℕ, bushn α n ≃ (bush^[n] α) := sorry

def bush.nil (α : Type*) : bush α := bushn.nil α
def bush.cons {α : Type*} (a : α) (b : bush (bush α)) : bush α :=
bushn.cons (bushn.zero a) ((bushn.equiv α 2).symm b)

def {u l} bush.rec {C : ∀ {α : Type u}, bush α → Sort l}
(C0 : ∀ α, C (bush.nil α))
(C1 : ∀ α a b, C b → C (@bush.cons α a b))
(α b) : @C α b := sorry

def bush.rec_nil {C} (C0 C1 α) :
@bush.rec @C C0 C1 α (bush.nil α) = C0 α := sorry

def bush.rec_cons {C} (C0 C1 α a b) :
@bush.rec @C C0 C1 α (bush.cons a b) =
C1 α a b (@bush.rec @C C0 C1 (bush α) b) := sorry


#### Sean Leather (Jul 06 2018 at 09:00):

At a glance, that looks similar to what's in the article I linked.

#### Mario Carneiro (Jul 06 2018 at 09:02):

Is it? I thought they assume that bush makes sense as an inductive without further justification, since Agda accepts it

#### Sean Leather (Jul 06 2018 at 09:04):

Copy-paste:

data BushN : Nat -> Set -> Set where
Base : {a : Set} -> a -> BushN Z a
NilBN : {a : Set} -> {n : Nat} -> BushN (S n) a
ConsBN : {a : Set} -> {n : Nat} -> BushN n a -> BushN (S (S n)) a -> BushN (S n) a


#### Mario Carneiro (Jul 06 2018 at 09:05):

Oh, I missed that

Last updated: May 14 2021 at 12:18 UTC