Mutually recursive inductive types

Stream: new members

[Sam Stites]

Hi all,
I'm trying to use Lean to do some language design and experimentation.

I'm just starting with an untyped lambda calculus which looks a little like:

constants (real : Type)

structure var := (Var : string)
structure fn  := (Fn : string)

inductive primval : Type
  | Real : real → primval
  | Bool : bool → primval
  | MyList : list myexpr → primval

inductive primop : Type
  | Op : string → primop

  -- number ops
  | Mul : primop
  | Sub : primop
  | Div : primop
  | Add : primop
  | GT : primop
  | LT  : primop

  -- bool ops
  | Or  : primop
  | And  : primop

inductive myexpr : Type
  | Primval : primval → myexpr
  | Primop : primop → myexpr
  | Let : var → myexpr → myexpr → myexpr
  | V : var → myexpr
  | F : fn → myexpr
  | If (pred : myexpr) : myexpr → myexpr → myexpr
  | Lambda (vs : list var) (body : myexpr)
  | App (op : myexpr) (args : list myexpr)

Unfortunately, MyList : list myexpr → primval doesn't have myexpr in scope -- I guess lean doesn't hoist definitions?

How would you go about doing this? Alternatively, is a resource on writing embedded DSLs in lean?

Oh, also, where is real?

[Kenny Lau]

```lean
[code goes here]
```

[Kenny Lau]

import data.real.basic

[Kenny Lau]

you can have mutual inductive types

[Reid Barton]

In this case, though, the path of least resistance is most likely to "inline" primval into myexpr, given that you use it only once

[Reid Barton]

(A list of any-values-whatsoever isn't so "primitive" anyways, is it?)

[Sam Stites]

Thanks @Kenny Lau! Am I doing something wrong here, then? This example fails to compile.

@Reid Barton I can't inline as I'm aiming for something slightly more complex.

[Reid Barton]

Check the section of TPIL on mutual inductive types

[Kevin Buzzard]

https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html#mutual-recursion

[Reid Barton]

they have their own syntax, and they are handled by translation into an indexed inductive type so they are less pleasant to handle

[Kevin Buzzard]

and https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html#mutual-and-nested-inductive-types

[Sam Stites]

Perfect! Thank you!

[Reid Barton]

don't say you weren't warned :smiling_devil:

[Jannis Limperg]

Not long ago, I asked @Gabriel Ebner a question about some mutual inductives and his answer was something along the lines of, "don't ever use them, they don't work". In that spirit: Has anyone actually used mutual inductives successfully?

[Reid Barton]

(At a high level, the situation is: the Lean kernel does not support mutually inductive types; so either you have to use mutual or manage the translation yourself, each with its own downsides)

[Reid Barton]

Apparently there is exactly one use in mathlib, in a file I've never looked at

[Reid Barton]

oh but they are mutually inductive Props, which probably makes life simpler

[Reid Barton]

Maybe they are usable if you only care about programming and not proving?

[Reid Barton]

Heh, these search results are also representative I think: https://github.com/flypitch/flypitch/search?q=mutual&unscoped_q=mutual

[Sam Stites]

Ultimately, I'm hoping to formally verify some DSLs so hopefully these don't fall apart too fast

[Reid Barton]

One use in a subdirectory old/, and a comment in the real code explaining that they are not convenient

[Scott Morrison]

Every attempt I've made to use them has worked at first, and them quickly led to despair (usually the definitional equations not being usable for some reason), and me asking the experts here "how do I write this without mutual inductives"?

[hakanaras]

How can I achieve what I'm trying to do here:

mutual

  structure HostField where
    name : String
    type : HostType
    default? : Option (Default type)

  structure HostProduct where
    name : String
    fields : List HostField

  inductive HostType where
    | string : HostType
    | product : HostProduct -> HostType

  inductive Default : HostType -> Type where
    | string : String -> Default HostType.string

end

I know that it's not possible to use one mutual inductive type as a parameter for another. I just want to know how this could be achieved instead. ("This" being that I want to provide a default value of the type in HostField.type sometimes)

Also I know the difference between parameters and indices on inductive/structure types, but what is the difference between parameters and indices on constructors? Don't they behave the same for the most part?

[Rob Simmons]

Would it represent your intent to paramaterize the types by the type of their default value?

mutual

  structure HostField' a where
    name : String
    type : HostType' a
    default? : Option a

  structure HostProduct' a where
    name : String
    fields : List (HostField' a)

  inductive HostType' a where
    | string : HostType' a
    | product : HostProduct' a -> HostType' a

end

def HostField := HostField' String
def HostProduct := HostProduct' String
def HostType := HostType' String

[hakanaras]

Not really. In practice there are lots of different constructors of HostType. This was just a minimized example.

So one HostProduct can have several fields with different default value types.

[Jason Reed]

Just taking a guess here, but in the absence of induction-induction I would try independently defining untyped values in a separate mutual like

mutual

structure FieldVal : Type where
    name : String
    val : Val

inductive Val : Type where
  | strVal : String → Val
  | recVal : List FieldVal → Val

end

mutual

  structure FieldTy where
    name : String
    type : Ty
    default? : Option Val

  inductive Ty where
    | strTy : Ty
    | recordTy : List FieldTy → Ty

end

and then defining what it means for a Val to be well-typed at a Ty, and a FieldVal at a FieldTy. But maybe there's some cleverer way to approximate what you want in Lean while still maintaining the intrinsic typing in your default? : Option (Default type). To me it smells very intrinsically induction-induction-ish though.

[Jason Reed]

Messages like this suggest to me "falling back to less-indexed representations then defining well-formedness predicates on them after the fact" (which is how I'd characterize my guess above) is in fact a standard way to cope with this in Lean.

[hakanaras]

I've tried a bunch of stuff, but at every turn I either run into a problem with non-strictly-positive types or constructors with local variables, or it ends up not being ergonomic to use.

I ended up having an inductive type HostVal and HostField.type has type HostType ⊕ HostVal. And each HostVal belongs to one HostType obviously.

[Jakub Nowak]

Should default value be part of the type though? That would make types with different default values not defeq. I would say default value is property of a definition of a type, or its constructors, not of type.
I vaguely recall having made similar design decision as you when writing interpreter for my language, and later having to refactor.
Actually, Lean has default value as part of type, so it's likely to be ok. Maybe my case was something different.