nested recursion

Stream: general

[Kana]

is it possible to write such function?

inductive rec
| mk : list (string × rec) → rec

-- unexpected occurrence of recursive function
def rec.map (f : rec → rec) : rec → rec
| (rec.mk xs) := rec.mk (prod.map id rec.map <$> xs)

[Mario Carneiro]

nested inductives are not really supported in lean, they are compiled (badly) to inductive types. It's better to roll your own inductive type if you want the right recursion principle

[Mario Carneiro]

although you can also sort of ignore the foundational issues if you use meta inductive

[Mario Carneiro]

which is probably fine if this is intended for code execution

[Kana]

I want just to write has_repr instance for such type

[Kana]

Maybe there is some way to derive that instance?

[Mario Carneiro]

I think it's best to imagine that the inductive line itself failed

[Mario Carneiro]

you can't define any functions by structural recursion on this type without a lot of manual work

[Mario Carneiro]

So my question for you is whether you want a type you can run functions on in the VM, or a type you can prove things about by induction/recursion

[Mario Carneiro]

If it is the former, the solution is easy:

inductive rec
| mk : list (string × rec) → rec

meta def rec.map (f : rec → rec) : rec → rec
| (rec.mk xs) := rec.mk (prod.map id rec.map <$> xs)

[Mario Carneiro]

or, probably better,

meta inductive rec
| mk : list (string × rec) → rec

meta def rec.map (f : rec → rec) : rec → rec
| (rec.mk xs) := rec.mk (prod.map id rec.map <$> xs)

[Kana]

Okay. I have such type

inductive value
  | string : string → value
  | object : list (string × value) → value
  | array : list value → value
  | number : ℕ → value
  | bool : bool → value
  | null : value

and all what I want is just to print value of this type via #eval, so I want has_repr or has_to_string instance, but I can't write it

[Kana]

thanks, I will try meta

[Mario Carneiro]

If you want to prove things about it, you should unfold the nested inductive into a plain inductive:

inductive rec
| nil : rec
| cons : string → rec → rec → rec

def rec.map (f : rec → rec) : rec → rec
| rec.nil := rec.nil
| (rec.cons s x xs) := rec.cons s x.map xs.map

[Mario Carneiro]

A cheating way to fix your json type is to unfold the object and array constructors into nil/cons

inductive value
| string : string → value
| object_nil : value
| object_cons : string → value → value → value
| array_nil : value
| array_cons : value → value → value
| number : ℕ → value
| bool : bool → value
| null : value

The problem with this is that there are some values of this type that are not valid json, for instance array_cons v object_nil. For most code this doesn't matter since it's being validated into a more precise type anyway, but it's possible to encode this invariant as a predicate or as an index in the type

[Mario Carneiro]

But from your description I think meta is the way to go, termination checking doesn't matter for your use case

[Kana]

Thanks! meta works great for me