Debugging within a do block

Stream: new members

[Malcolm Langfield]

This is probably a pretty basic question. I've run into the same situation multiple times: I'm trying to inspect a value of some type that doesn't implement ToString, and do it within a do block. My bad solution so far has just been to replicate the whole function up to that point in a different file, and then change the return type to be the type of the object I want to inspect. Then I can at least #eval it. Is there an idiomatic way to do this sort of debugging?

[Arthur Paulino]

(deleted)

[Mario Carneiro]

depending on the monad, you can use dbg_trace to show the value. If that doesn't work lots of things have a repr that you can trace instead

[Mario Carneiro]

and I think you can automatically derive Repr so that's a least common denominator solution in most cases

[Malcolm Langfield]

Mario Carneiro said:

and I think you can automatically derive Repr so that's a least common denominator solution in most cases

Sorry for my ignorance, but what's the syntax for doing this?

[Malcolm Langfield]

Or a reference to where it's described

[Mario Carneiro]

deriving Repr at the end of the inductive/structure type declaration, or deriving instance Repr for Foo after the fact

[Mario Carneiro]

@Arthur Paulino Is this in the book?

[Arthur Paulino]

The book uses dbg_trace but I think it's worth explicitly talking about these details

[Mario Carneiro]

I meant about deriving handlers in general and maybe which ones are implemented by default

[Mario Carneiro]

I suppose it's not metaprogramming per se, although I do get the sense that you interact a lot more with deriving handlers when (meta)programming in lean as compared to proving

[Arthur Paulino]

Ah, no. Henrik mentioned it to me via DM and we agreed that it could be covered. I'm just not sure which approach would be better. Maybe we can teach how to create them?

[Mario Carneiro]

Knowing about deriving Repr, Quote, ToExpr should be a fairly early topic, you will want to know about it when doing basic metaprogramming. Writing a deriving handler on the other hand is a pretty advanced topic, and I would just cover the core functions for doing so in the section that deals with that part of lean

[Malcolm Langfield]

Maybe looking at a specific example would be helpful. So I'm playing around with the Http.lean package:

  import Http
  open Http Http.URI

  constant spreadsheetId : String := "<id>"

  deriving instance Repr for Headers     ■ default handlers have not been implemented yet, class: 'Repr' types: [Http.Headers]
  deriving instance Repr for Request     ■■■■ failed to synthesize instance    Repr Headers

  def main : IO UInt32 := do
    let input ← pure s!"https://sheets.googleapis.com/v4/spreadsheets/{spreadsheetId}"
    try
      let url ← IO.ofExcept <| URI.parse input
      println! "URL: {url}"
      let headers := Headers.fromList [("Host", url.host)]
      let request := Request.init url Method.GET headers none
      -- println! "Candidate request: {request}"
      println! "Headers: {headers}"
      pure 0
    catch e =>
      IO.eprintln s!"error: {e}"
      pure 1

I'm not even sure if having those deriving commands floating there at the top-level of the file is correct syntax. But you can see the definitions of the Request and Headers types here: https://github.com/yatima-inc/Http.lean/blob/3f1e77d98b14a0d8d2e6dd7d93730c4c15d57c7b/src/Http/Types.lean#L114

Headers is just a hashmap:

def Headers := Std.HashMap CaseInsString String

It's very surprising to me that you can't print a term of this type, since it's from Std and CaseInsString implements ToString. But maybe I'm seriously misunderstanding something.

[Arthur Paulino]

Hm, throughout the book we didn't come across the need to use those handlers. We usually print strings and other objects that can already be printed

[Mario Carneiro]

Malcolm Langfield said:

It's very surprising to me that you can't print a term of this type, since it's from Std and CaseInsString implements ToString. But maybe I'm seriously misunderstanding something.

That's the delta deriving handler, which is not yet implemented in lean 4 / mathlib4. It's not too hard to implement it yourself:

instance : Repr Headers := inferInstanceAs $ Repr (Std.HashMap ..)

[Mario Carneiro]

The thing which makes this hard is that it works for any typeclass, it's not just for Repr, while deriving handlers are normally indexed by class

[Malcolm Langfield]

Mario Carneiro said:

Malcolm Langfield said:

It's very surprising to me that you can't print a term of this type, since it's from Std and CaseInsString implements ToString. But maybe I'm seriously misunderstanding something.

That's the delta deriving handler, which is not yet implemented in lean 4 / mathlib4. It's not too hard to implement it yourself:

instance : Repr Headers := inferInstanceAs $ Repr (Std.HashMap ..)

This does not seem to work:

instance : Repr Headers := inferInstanceAs $ Repr (Std.HashMap ..)     ■ failed to synthesize instance    Repr (Std.HashMap CaseInsString String)

The concept of a deriving handler is new to me. Is there any discussion of this in any of the various docs/books? I expected to find it in TPIL4, maybe in the section on type classes or inductive types, but there is only the most basic discussion of using the deriving keyword while defining inductive types.

[Mario Carneiro]

If that fails, then that means that even after unfolding there is something that requires a repr instance, probably CaseInsString?

[Mario Carneiro]

Deriving handlers are the functions that get called whenever you write deriving Foo on an inductive/structure type. Not all typeclasses have deriving handlers, Repr is one of the few that does, but it doesn't support def deriving so you have to use the trick above to do what it would otherwise need to do

[Malcolm Langfield]

  deriving instance Repr for CaseInsString
  instance : Repr CaseInsString := inferInstanceAs $ Repr CaseInsString
E instance : Repr Headers := inferInstanceAs $ Repr (Std.HashMap ..)     ■ failed to synthesize instance    Repr (Std.HashMap CaseInsString String)

Thanks very much for the help so far! It looks as though CaseInsString has one, and String does as well. Is there any way to get Lean to give me more information about what is causing the failure to synthesize instance? Surely someone cannot be expected to know all of this in order to print-debug something?