A Type 1 inductive type

Stream: general

[Tanner Swett]

I feel like I just leveled up: I just wrote my first ever inductive type that required me to use a higher universe, and it's also my first ever mutually inductive type :big_smile:

Here it is:

mutual
  inductive StackFrame : (α β : Type) → Type 1 where
    | eval : StackFrame Expr Expr
    | func {α β γ : Type} (f : α → β) (g : α → Stack β γ) : StackFrame α γ

  inductive Stack : (α β : Type) → Type 1 where
    | empty (α : Type) : Stack α α
    | push {α β γ : Type} (top : StackFrame α β) (rest : Stack β γ) : Stack α γ
end

The type Stack here represents a call stack. A func stack frame consists of two components: a function to run immediately to produce an intermediate result, and a function producing a collection of stack frames which will further process the intermediate result.

This _does_ need to be in Type 1, right? A Stack can contain functions with arbitrary domain and codomain types, which means that a Stack needs to contain Types, and anything with Types in it has to live in Type 1 or higher.

[Mario Carneiro]

Yes, this has to be in Type 1 as written, although usually this is a bad sign / to be avoided. Usually you can avoid it in this kind of situation by classifying some family of types that you actually care to consider, which can be indexed by a normal inductive type instead of by a universe

[Tanner Swett]

Yup. I figured it would be cool to be able to write implementation functions in do notation, which means I need a monad, and I've discovered that that means that the call stack can get "polluted" with arbitrary types, so I need this.