dumb questions

Stream: lean4

[Chris Lovett]

Can someone help me get a Tree walk function working? I'm trying to copy how the Json render function works but I'm getting a strange error:

inductive Tree (β : Type v) where
 | leaf
 | node (left : Tree β) (key : Nat) (value : β) (right : Tree β)
deriving Repr

def walk  : Tree β → String
  | leaf => "leaf"
  | node l k v r => "node: " ++ (toString k) ++ (v) ++ "\n" ++ (walk l) ++ "\n" ++ (walk r)

error: invalid pattern, constructor or constant marked with '[matchPattern]' expected?

[Mario Carneiro]

leaf and node aren't in scope

[Mario Carneiro]

You can fix this with either open Tree or def Tree.walk or use .leaf and .node in the patterns

[Chris Lovett]

Doh! thanks, not the best error message... :-)

[Henrik Böving]

The reason its giving you this error message is that it is interpreting node as a named wildcard pattern (which is in principle correct) but now you're also giving the thing arguments as if it was a function (l k v r) which doesnt make sense since the wildcard pattern can of course not receive arguments.

It also did the same with leaf but since leaf doesn't have arguments it goes through as a normal named wildcard.

You can also recognize the difference between a match pattern being interpreted as a wildcard and as a real constructor based on it's highlighting:

As wildcard:
image.png

As constructor:
image.png

[Malcolm Langfield]

I've just tried to run this for kicks, and I've gotten an error message I don't understand (scroll to the right if you can't see it):

  inductive Tree (β : Type v) where
   | leaf
   | node (left : Tree β) (key : Nat) (value : β) (right : Tree β)
  deriving Repr

  def walk  : Tree β → String
    | .leaf => "leaf"
    | .node l k v r => "node: " ++ (toString k) ++ (v) ++ "\n" ++ (walk l) ++ "\n" ++ (walk r)     ■ failed to synthesize instance    HAppend String β ?m.5860

I see in the Lean 4 source that HAppend is responsible for the ++notation, and is a typeclass taking three arguments, and the first two look all right:

class HAppend (α : Type u) (β : Type v) (γ : outParam (Type w)) where
   hAppend : α → β → γ     ■ (kernel) unknown constant 'Eq.ndrec'

So I assume it's unhappy about whatever it's getting for γ. But I don't really understand how this class is being instantiated when you use this notation.

[Sebastian Ullrich]

What the error message is trying to say is that Lean doesn't know how to append a String ("node: " ++ (toString k)) and a β ((v))

[Henrik Böving]

First things first there is not actually a reason to use the append notation here, we might as well use s! notation like this:

 def walk  : Tree β → String
   | .leaf => "leaf"
   | .node l k v r => s!"node: {k} {v}\n{walk l}\n{walk r}"

this does however still throw an error (and as we will see this is also the reason why the append notation fails)

failed to synthesize instance
  ToString β

so let's add that instance to our arguments:

 def walk [ToString β] : Tree β → String
   | .leaf => "leaf"
   | .node l k v r => s!"node: {k} {v}\n{walk l}\n{walk r}"

Now everything works.

So what's happening above is that everything comes down to:

 def walk  : Tree β → String
   | .leaf => "leaf"
   | .node l k v r => (toString k) ++ (v)

this not working out properly, it produces the same error message:

failed to synthesize instance
  HAppend String β ?m.1520

If we were to use toString on vand add the corresponding instance parameter everything would work just fine.

[Henrik Böving]

And i spent 5 min writing this essay /o\

[Sebastian Ullrich]

The essay is definitely more helpful :)

[Malcolm Langfield]

@Sebastian Ullrich @Henrik Böving Thanks for the quick explanations! I definitely like how the error message is a bit more clear (imo) when you use the string interpolation. So is it correct to read the square bracket/typeclass resolution notation as "β must implement ToString"? And for fixed β, we would achieve this by writing something of the form instance ToString β where ...?

[Henrik Böving]

You are missing a colon: instance optionalName : ToString β where but yes in principle you are right.

[Chris Lovett]

Another dumb question, I'm trying to parse XML and it took me forever to figure out that the import statement and the open statement have to be different and I'm wondering if there are any debug things that tell me what symbols are in scope when I use the open statement so I can debug this sort of thing:

import Lean.Data.Xml
open Lean.Xml
#eval parse "<root/>"

I also missed this magic combination a couple times until I realized that the Lean LSP was just being slow, seems when you import something it takes a few seconds to catch up? It might be handy to change the InfoView (or popup tips) to "busy" in this case so I know it's not done yet...

[Henrik Böving]

Regarding the first: I usually do #check Lean.Xml. and check out the auto completion at that point

Regarding the second thing, if I import something heavy and it takes a while I can see my emacs indicating that in the left side bar by colouring it orange
image.png
as the compiler progresses during the file it begins removing the orange bar from the lines that it already checked

[Chris Lovett]

Thanks, I have another one, what does the $ operator do?

partial def manyCore (p : Parsec α) (acc : Array α) : Parsec $ Array α :=
  (do manyCore p (acc.push $ ←p))
  <|> pure acc

I think it's implemented here, but I couldn't figure it out from there...

def macroArg       := termParser maxPrec
def macroDollarArg := leading_parser "$" >> termParser 10
def macroLastArg   := macroDollarArg <|> macroArg

As the only place this is referenced is in BuildinNotation under elabStateRefT...?

[Hanting Zhang]

Parsec $ Array α is equivalent to Parsec (Array α). It doesn't do anything, but it binds with very low precedence so that you can avoid stacking parentheses

[Hanting Zhang]

So something like f (g (h x y)) can be written as f $ g $ h x y

[Chris Lovett]

Awesome thanks, totally wouldn't have figured that out from the code. A comment to that effect in the code would have been nice. Better yet, a comment that would then also popup when I hover my mouse over the $ symbol...

[Malcolm Langfield]

There is some documentation here: https://leanprover.github.io/lean4/doc/functions.html

For users familiar with the Haskell programming language, Lean also supports the notation f $ a for the backward pipeline f <| a.

The forward pipeline |> operator takes a function and an argument and return a value. In contrast, the backward pipeline <| operator takes an argument and a function and returns a value. These operators are useful for minimizing the number of parentheses.

Example from the manual:

def add1 x := x + 1
def times2 x := x * 2

#eval times2 (add1 100)
#eval 100 |> add1 |> times2
#eval times2 <| add1 <| 100

[Malcolm Langfield]

Admittedly it's not exactly easy to find if you're specifically looking for a definition of the $ operator, and don't already know your way around the manual.

[Remi]

How can I write this function?

def TType.eq : TType → TType → Option (t₁ = t₂)
  | t₁, t₂ =>
    if t₁ == t₂ then some sorry
    else none

[Edward Ayers]

Sounds like you want to derive DecidableEq TType

[Remi]

@Edward Ayers Thanks, that exactly what I want!

[Edward Ayers]

You can do something like this:

variable {TType : Type u} [DecidableEq TType]
def TType.eq (t₁ t₂ : TType) : Option (t₁ = t₂) :=
  if h : t₁ = t₂ then some h else none

Unfortunately that doesn't quite work because Option only accepts types and not props. But once you have the if h : P then A else B pattern where Decidable P you can do a lot.

Also have a look at this section of TPIL: https://leanprover.github.io/theorem_proving_in_lean4/type_classes.html?highlight=Decidable#decidable-propositions

[Chris Lovett]

Why doesn't this work:

#eval (List String).nil

I realize I can use literal syntax and do this ([]: List String) but I'm just wondering what the deep compiler reason is to disallow the syntax I've written here. I'm confused why I can't declare the type, put it in parens and call the nil constructor to get back a typed empty list.

Seems type classes have the same limitation:

#eval (Add Nat).add 1 2

and this doesn't work either:

def Foo := List String
#eval Foo.cons "hello" ["a", "b", "c"]

But I can write this:

#eval ["a", "b", "c"].cons "d"

and this:

def emptyListOfStrings : List String := List.nil
#check emptyListOfStrings   -- List String

So it works when the type is implicit or can be inferred, and so I guess I'd understand better if the type argument to list was declared implicitly instead of explicitly ...

[Reid Barton]

The useless reason is that there's no reason to think that your non-working examples should work.

[Reid Barton]

Note in your working examples you have, before the ., either a value (["a", "b", "c"]) or a namespace (List).

[Reid Barton]

In the former case, because ["a", "b", "c"] : List String, ["a", "b", "c"].cons means List.cons.

[Jireh Loreaux]

so #eval (List.nil : List String) would work, right? (I'm not in Lean 4 at the moment.)

[Chris Lovett]

Yeah, I know all the variations that work, I'm just trying to figure out what is wrong with my understanding of inductive types that makes me think I should be able to #eval (List String).nil. Note that I cannot call nil on a list value (like I can with x.cons) since the nil constructor takes no arguments.

[Reid Barton]

(List String).nil should refer to Type.nil, I guess

[Mario Carneiro]

Keep in mind that List.nil and (List).nil are two completely different things. The first one is a single token, a namespaced name, and the second one is the |>.nil operation applied to the expression List

[Mario Carneiro]

This is somewhat confused by the fact that x.nil (where x is a local variable) is ambiguous between both of them, and there is some complexity in name resolution due to this

[Chris Lovett]

Thanks, the fact that (List).nil gives the same error is helpful. Perhaps the type argument on List is not really a type argument, it is some sort of type "context" that can only be inferred. At least lean is very consistent about this, I can't do this either:

structure Point (α : Type u) :=
  x : α
  y : α
  deriving Repr

#eval (Point Float).mk 5 7              -- same error

#eval (Point.mk 5 7 : Point Float) -- { x := 5.000000, y := 7.000000 }

[Reid Barton]

So for example Nat.zero is a namespaced name (zero in namespace Nat) that has nothing to do with the type Nat--except that the same inductive command defined both of them

[Reid Barton]

Chris Lovett said:

Perhaps the type argument on List is not really a type argument, it is some sort of type "context" that can only be inferred.

The type argument in List String really is a type argument. But List in List.nil is not a type at all

[Chris Lovett]

And for consistency you can't write (Nat).zero either.

[Chris Lovett]

Well the members of an inductive type are called "constructors" in TPIL. So List.nil should be constructing a List but it can't resolve the required type parameter, so you get the unresolved type List.nil : List ?m.10448.

[Chris Lovett]

And I was thinking why can't I help the compiler resolve the missing type by providing it with (List String).nil but alas, parens are special and dot notation doesn't like them.

[Reid Barton]

No, it has nothing to do with parentheses

[Reid Barton]

You are inventing some interpretation of List.nil that does not exist in Lean.

[Chris Lovett]

That's a good way to put it. All inductive type constructors must then be only "Name.ctor" where Name is the inductive type name and ctor is the constructor name, like Weekday.Monday in TPIL. But if the inductive type has one or more type parameters, those types must be inferred as they cannot be passed directly in the inductive type constructor call.

[Chris Lovett]

Oh, wait, yes it can with this #check List.nil (α := Float) -- : List Float interesting...

[Reid Barton]

Maybe it's not clear what inductive actually does: the inductive definition for List creates three new identifiers List, List.nil, List.cons (and a bunch of other stuff). List.nil has List as part of its name (more precisely, it is in the List namespace).

[Reid Barton]

List.nil doesn't mean "give me something called nil of type List", it is simply the identifier List.nil.

[Chris Lovett]

Well TPIL calls it an inductive type "constructor" so I don't want to stray too far from that definition.

[Chris Lovett]

So I read List.nil as construct a List using the nil constructor.

[Reid Barton]

Well, that's not how it works :upside_down:

[Chris Lovett]

Oh?

[Reid Barton]

It just means: the identifier List.nil.

[Reid Barton]

You could imagine a version of inductive that instead creates constructors called List_nil and List_cons, and then the way you would construct an empty list is using List_nil--but it would work exactly the same way.

[Mario Carneiro]

The C++ analogue would be something like List::nil()

[Mario Carneiro]

this is not the same as List.nil() which is a method applied to an object called List

[Mario Carneiro]

The List in List::nil is just a namespace, not an object. it's a way to construct fancy segmented names but not otherwise a thing in its own right

[Mario Carneiro]

In lean the first one is spelled List.nil and the second is (List).nil or List |>.nil (and this latter thing doesn't work because there isn't a method Type.nil that would apply to List itself)

[Chris Lovett]

I'm sure that all the object oriented programming I've done is where my problems are coming from so switching to C++ doesn't help because there I can call the constructor on the fully qualified type to create an empty list with auto x = list<float>();

[Mario Carneiro]

The analogue of calling the constructor on the fully qualified type is @List.nil Float

[Chris Lovett]

But I cannot call the constructors on a fully qualified inductive type like (List String)

[Mario Carneiro]

or (.nil : List String)

[Chris Lovett]

thanks and I also found List.nil (α := Float) earlier.

[Chris Lovett]

This one (.nil : List String) doesn't count in my mind because it is depending on type inference. I was looking for a syntax that did not depend on type inference. The @ one is interesting, but probably not for beginners? I think the closest so far is List.nil (α := Float)

[Mario Carneiro]

The @ syntax is the most straightforward, even for beginners, although you might want to prefer the other methods for style reasons

[Mario Carneiro]

If there are typeclass arguments you will need a lot of _ when using @

[Reid Barton]

What makes this confusing is:

• The dot is used in two different syntactic constructs, building namespaced names (List.nil) and also "dot notation" (["a", "b", "c"].cons "d").
• In Lean, types are also expressions, so the type List is something that it would make sense to use dot notation on (at least in principle). However, that's not what's going on in List.nil, which is a namespaced name.
• The inductive command puts the constructors in a namespace named after the type being created. (Likewise, hand-written definitions relating to the List type are by convention put in the List namespace.) That opens the possibility of misinterpreting List.nil as involving the type List somehow.

[Mario Carneiro]

It's the most direct analogue of your list<string>() example

[Jireh Loreaux]

It wouldn't make much sense to call a constructor on List String. Think about this: modulo differences that don't matter List (α : Type) → Type, so List eats a type and spits out another type. Thus List String : Type. If you were going to have a function that takes List String as an argument and returns something (like the List.nil) of that type, such a function would have to have type Type → List String. How would such a function behaves on types other than List String?

[Mario Carneiro]

This also explains why if you want to have List String involved in the syntax you need to use type inference, because the constructor isn't taking List String as the argument, the argument is String and the resulting type is List String

[Leonardo de Moura]

BTW, our LSP server makes it clear which interpretation was used for the .s. You have to use a color theme that distinguishes the relevant syntactic categories or customize one.
image.png

• List.nil is white because it is a constant.
• val and values are yellow because they are parameters (or local variables).
• cons is purple because it is part of the dot-notation. values.cons val is syntax sugar List.cons val values. If we hover over the elements, you will also get similar information.

[Patrick Massot]

Do we have a guide of relevant syntactic categories? I start all my Lean4 files with set_option autoImplicit false because my color theme isn't good enough at telling me when a typo triggers autoImplicit while I meant to name some existing thing.

[Leonardo de Moura]

@Patrick Massot The key syntactic categories for Lean are variable (for highlighting local variables and parameters) and property (for highlighting the dot notation). Very few color themes handle them out of the box :(

[Leonardo de Moura]

You can configure an existing theme by editing your settings.json.

[Patrick Massot]

I found the previous discussion in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.E2.9C.94.20VS.20Code.20color.20scheme. I'll try to write a useful summary

[Leonardo de Moura]

Here is my config

    "editor.semanticHighlighting.enabled": true,
    "workbench.colorCustomizations": {
      "[Solarized Light]": {"editor.selectionHighlightBackground": "#e9dcc5"}
    },
    "editor.semanticTokenColorCustomizations": {
        "[Solarized Light]": {"rules": {"function": "#c1892f", "property": "#69878c"}},
        "[Ayu Dark]": {"rules": {"property": "#948fd0", "variable": "#cbc248"}}
    },

[Leonardo de Moura]

Patrick Massot said:

I found the previous discussion in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.E2.9C.94.20VS.20Code.20color.20scheme. I'll try to write a useful summary

Thanks! We will add it to the manual.

[Chris Lovett]

Leo made an interesting point that is helpful: values.cons val is actually List.cons val values. I was thinking of List as a sort of generic type (in the C++ sense) that can't reallybe constructed until you provide the type parameters, and List String then as a specialization of that same type and therefore it inherits all the methods that List has, including the constructors and this is simply not the case. So, the fact that you can write #eval ["a", "b"].cons "c" -- ["c", "a", "b"] is a little misleading because it makes it appear that List String has a cons constructor, but it doesn't.

[Chris Lovett]

Building on all the interesting talk about namespaces above, I can extend the List.String namespace and add this:

namespace List.String
def nil : List String := []
end List.String

#eval List.String.nil  -- []
#check List.String.nil  --List String

but obviously I don't want to do that for every possible type of list...

[Reid Barton]

Likewise, you could also do

namespace Nat
def nil : List String := []
end Nat

#eval Nat.nil  -- []
#check Nat.nil  --List String

[Mauricio Collares]

The List.String namespace was empty before this, right?

[Mauricio Collares]

If not, that gives me a strong vector<bool> vibe

[Jireh Loreaux]

Again, the above List.String.nil is just an identifier; it's not doing anything fancy.

[Mauricio Collares]

Right, I should have said "there are no other List.String-prefixed identifiers, right?". Thanks for the correction.

[Jireh Loreaux]

Sorry Mauricio, my comment was intended for aiding Chris's understanding.

[Chris Lovett]

I hear what you are saying about "List.nil" is just an identifier and "List.String.nil" is just an identifier and so on, but it is not satisfying given that in every other language "." is special. If I followed your statement to its logical conclusion, I would think it is perfectly fine to write this function:

def Frump...alump (x : Nat) := x * x            -- unknown identifier 'Frump'

But alas I cannot. So "." in an Identifier is special. It is a namespace separator.

[Reid Barton]

Yes exactly. But the List namespace has no relation to the List type, except by convention (and how the inductive command works).

[Mario Carneiro]

. in identifiers is special, but only to give a hierarchical structure to identifiers. . is not an "identifier character" so you can't directly write a..b as an ident

[Mario Carneiro]

Without such structure it's hard to have commands like open that allow you to omit namespaces in an identifier

[Chris Lovett]

I love using "." in namespace qualified names. I'm glad Lean can do the same. Note that TPIL does indeed call the List inductive type a namespace, with this:

The constructors all live in the Weekday namespace.

[Jireh Loreaux]

No, List the namespace and List the inductive type are different, they just happen to share the same four English letters. Nevertheless, the constructors for List the inductive type do live in the List namespace.

[Chris Lovett]

Perhaps you are talking implementation details, or are you saying the book TPIL is wrong when it says "The constructors all live in the Weekday namespace" ?

[Reid Barton]

The book is correct, the constructs do live in the Weekday namespace.

[Reid Barton]

The Weekday type and the Weekday namespace are not the same thing.

[Chris Lovett]

Well it's tricky because in the book the Weekday inductive type and all its constructors are defined BEFORE any explicit creation of namespace Weekday and in fact even before defining namespace Weekday the code was then able to open Weekday and open is defined to only work on namespaces, therefore the inductive type Weekday created a namespace of the same name, but we are quibbling now, so diminishing returns, but thanks for all the excellent thoughts and clarifications.

[Leonardo de Moura]

@Chris Lovett The book says: "The inductive command creates a new type, Weekday. The constructors all live in the Weekday namespace." It looks clear to me that a namespace called "Weekday" was also created. Otherwise, how would we add the constructors to the namespace "Weekday"?
Any suggestions on how to make it clear that a namespace "Weekday" is also being created? Or is it not clear at this point in the book that namespaces and types are different things?

[Reid Barton]

I think a namespace is "created" (in the sense that you can open it) as soon as any identifier is defined in that namespace; in any case, the inductive Weekday [...] command certainly creates the Weekday namespace, as well as the Weekday type (and various other things).

[Chris Lovett]

I think it would be nice to explicitly state somewhere that defining and inductive type creates both a type and a namespace of that same name. This avoids confusion with other languages where a type name is a namespace which then avoids my original confusion thinking (List String) is a namespace that I could .cons or .nil into. Question, does a type class also create a namespace of the same name? What about a structure?

[Leonardo de Moura]

From TPIL: "The structure command is essentially a "front end" for defining inductive data types. Every structure declaration introduces a namespace with the same name. The general form is as follows:"

[Leonardo de Moura]

https://leanprover.github.io/theorem_proving_in_lean4/structures_and_records.html#declaring-structures

[Chris Lovett]

that language is perfect, and I assume the same language could be used in the chapter on inductive types, and type classes?

[Chris Lovett]

How come Repr doesn't provide ToString?

structure Config where
  help : Bool := false
  verbose : Bool := false
  input : String := ""
  output : String := ""
  deriving Repr

#eval ({} : Config)
-- { help := false, verbose := false, input := "", output := "" }

But I can't seem to do IO.println config nor can I IO.println s!"{config}" ? Do I have to also create a ToString instance on this? I see stuff like this in the Lean code base:

def Stats.toString (s : Stats) : String :=
  s!"\{nodes := {s.numNodes}, depth := {s.depth}, tail size := {s.tailSize}}"

instance : ToString Stats := ⟨Stats.toString⟩

But what's the point of Repr if we have to do this also?

[Mario Carneiro]

ToString and Repr have slightly different purposes, roughly comparable to Rust's Display vs Debug. ToString is for a human-readable display of the string, while Repr is supposed to be (mostly) suitable for copy-pasting as lean code

[Chris Lovett]

Ok, and there's no helpers for ToString on a structure? I have to do it by hand?

[Mario Carneiro]

for instance, the ToString instance for strings just spits the string back out, while the Repr instance puts quotes and backslashes in

[Mario Carneiro]

And also like Rust, the derive handler only exists for Repr, with the ToString instance intended for manual implementation

[Mario Carneiro]

If you would like to use the same ToString as Repr, you can derive Repr and then instance : ToString Foo := \<repr\>

[Chris Lovett]

structure Config where
  help : Bool := false
  verbose : Bool := false
  input : String := ""
  deriving Repr

instance : ToString Config :=  ⟨repr⟩

gives an error

type mismatch
  ?m.2361 → Std.Format
has type
  Sort (max 1 ?u.2357) : Type (max 1 ?u.2357)
but is expected to have type
  ToString Config : Type

I searched the lean code for ⟨repr⟩ but found nothing like that...

[Sebastian Ullrich]

That's a terrifying error message, but I can't reproduce it

application type mismatch
  { toString := repr }
argument
  repr
has type
  ?m.1683 → Lean.Format : Type ?u.1682
but is expected to have type
  Config → String : Type