3
$\begingroup$

I have the following recursive data structures that I need ToJson and FromJson implementations:

mutual
  inductive Bind : Type
  | mk (name : String) (type : Pi)
  inductive Pi : Type
  | mk (params : List Bind) (body : Option App)
  inductive App : Type
  | mk (head : String) (children : List Lam)
  inductive Lam : Type
  | mk (names : List String) (body : App)
end

The default behavior of deriving instance ToJson, FromJson for ... doesn't work, because the generated functions are not marked as mutually recursive, so Bind.toJson wants to use Pi.toJson but it is defined later, so it's 404.

I wish I can look into the deriving logic and fix it, or just copy the code being generated and change it into mutually recursive functions. How can I do that?

I've done some research on Zulip, and looks like support for mutual inductives for deriving of traits need to be added separately. But IDK how to do it.

Using Szumi's trick I can make ToJson work, but due to the nature of being indexed, FromJson doesn't really work because it's ultimately four parsing functions:

inductive Tag | bindT | piT | appT | lamT
open Tag
inductive Canon : Tag → Type
| bind (name : String) (type : Canon piT) : Canon bindT
| pi (params : List (Canon bindT)) (body : Option (Canon appT)) : Canon piT
| app (head : String) (children : List (Canon lamT)) : Canon appT
| lam (names : List String) (body : Canon appT) : Canon lamT
deriving instance ToJson, FromJson for Canon
$\endgroup$
5
  • $\begingroup$ Qiu told me about where the functions are, it's mkToJsonInstance and mkFromJsonInstance, but they're are somewhat involved... Hmmm... $\endgroup$
    – ice1000
    Commented May 15 at 3:40
  • 1
    $\begingroup$ deriving is when you do this automatically. The natural alternative is to just implement your own instance for the type class ToJson. Are you familiar with type classes in Lean? If so, try to write a function which directly constructs a Json object for your structure (first ignoring type classes). $\endgroup$
    – Jason Rute
    Commented May 15 at 5:28
  • $\begingroup$ @JasonRute that's precisely the thing I want to avoid, I want to reuse the code generation (modify the generated code) or fix the generation $\endgroup$
    – ice1000
    Commented May 15 at 5:32
  • $\begingroup$ I sort of answered your question, but honestly I realize now I don't know what your question is? How to see the automatically created code? How to write a custom derive handler? How to automatically derive FromJson for mutual? (I answered the first question. I think the second is advanced, and the third is maybe not implemented, but I don't know for sure.) $\endgroup$
    – Jason Rute
    Commented May 15 at 20:43
  • $\begingroup$ @JasonRute All three would answer my question, and I appreciate that! I am trying to patch the code right now. Are you aware of any deriving that supports mutuals? $\endgroup$
    – ice1000
    Commented May 15 at 21:44

1 Answer 1

3
$\begingroup$

First, some background, if not for the OP, for another user:

How to convert a type to JSON manually?

Just create a function of type Foo -> Lean.Json.

import Lean
open Lean

-- new definition
inductive Foo
| mk (n : Nat)

-- manually convert to Json
def fooToJson : Foo -> Json
| .mk n => Json.num n

#eval fooToJson (Foo.mk 0) -- 0

It is similar for reading from Json, but then one also may need use a monad to handle errors. See other PA stack exchange questions on the topic, e.g. here and here.

How to register your function as an instance of ToJson?

By registering your instance, common type class related functionality like toJson works for your type. If you are not familiar with type classes, see the chapter in TPIL.

-- register this as instance of `ToJson Foo`
instance instToJsonFoo : ToJson Foo where
  toJson := fooToJson

#eval toJson (Foo.mk 1) -- 1

How to automatically derive ToJson Bar?

Using deriving you can automatically create and derive an instance of ToJson for your type. Especially with JSON, this may or may not be how you want toJson to behave. If it is not, the best option is just to define and register your own instance of ToJson Bar manually as above.

In my example below I set set_option trace.Elab.definition true to get more insight into what is going on.

set_option trace.Elab.definition true

-- new definition using `deriving ToJson`
inductive Bar
| mk (n : Nat)
deriving ToJson

-- it automatically created instance of `ToJson Bar` 
#eval toJson (Bar.mk 0) -- 0

Using the trace given by set_option trace.Elab.definition true we can see more of what is going on including the generated code.

There is an instance instToJsonBar which can be printed:

#print instToJsonBar
-- def instToJsonBar : ToJson Bar := { toJson := toJsonBar✝ }

The contents of the private function toJsonBar✝ can't be printed, but they can be read from the trace of deriving ToJson.

/-
[Elab.definition] _private.0.toJsonBar._@._hyg.67 : Bar → Lean.Json :=
    fun x =>
      match x with
      | Bar.mk a => Lean.Json.mkObj [("mk", Lean.Json.mkObj [("n", Lean.toJson a)])] 
-/

Making your own derive handler

You could make your own just derive handler, say ToJsonBetter and then when that is working, fix Lean's ToJson derive handler and PR it back to Lean. This is pretty advanced, and you should probably ask about it on the Lean Zulip first. The current derive handler for ToJson seems to be located here: https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Deriving/FromToJson.lean

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.