Zulip Chat Archive

Stream: lean4

Topic: better way of union type?

Joseph O (May 02 2022 at 15:47):

Is there a better way of doing this

inductive ValT : Type where
  | int : Int → ValT
  | float : Float → ValT

inductive RPN : Type where
  | add : RPN → RPN → RPN
  | mul : RPN → RPN → RPN
  | val : ValT → RPN

to have val be a constructor that takes in an Int or Float without a second inductive?

Horatiu Cheval (May 02 2022 at 15:50):

Your ValT is essentially a sum type, so it's the same as

inductive RPN : Type where
  | add : RPN → RPN → RPN
  | mul : RPN → RPN → RPN
  | val : Int ⊕ Float → RPN

Joseph O (May 02 2022 at 15:53):

Thanks

Leonardo de Moura (May 02 2022 at 15:53):

Yes, @Horatiu Cheval is right.
Note that, Int ⊕ Float is a notation for Sum Int Float.
That being said, I often prefer the version using ValT, the constructor names and type names often make the code easier to maintain.

Joseph O (May 02 2022 at 15:53):

You are probably right

Joseph O (May 02 2022 at 15:54):

I also have a small metaprogramming error. I was following the Arith tutorial, and this is my code so far,

inductive ValT : Type where
  | int : Int → ValT
  | float : Float → ValT

inductive RPN : Type where
  | add : RPN → RPN → RPN
  | mul : RPN → RPN → RPN
  | val : ValT → RPN

declare_syntax_cat rpn
syntax num : rpn
syntax rpn rpn "+" : rpn
syntax rpn rpn "*" : rpn

syntax "`[rpn| " rpn "]" : term

macro_rules
  | `(`[rpn| $num:numLit ]) => `(RPN.val (ValT.int $num))

(im making my own variation)
but in the first tule of the macro_rules, im getting this error:

expected 'num', 'rpn' or numeral

Joseph O (May 02 2022 at 15:54):

Any ideas?

Henrik Böving (May 02 2022 at 15:54):

Leonardo de Moura said:

Yes, Horatiu Cheval is right.
Note that, Int ⊕ Float is a notation for Sum Int Float.
That being said, I often prefer the version using ValT, the constructor names and type names often make the code easier to maintain.

In what situations would you prefer Sum over custom inductives?

Henrik Böving (May 02 2022 at 15:55):

Joseph O said:

Any ideas?

the numLit parser is now also called num

Joseph O (May 02 2022 at 15:55):

oh

Joseph O (May 02 2022 at 15:55):

Then the tutorial needs to be updated

Joseph O (May 02 2022 at 15:56):

Using Sum, would this be valid?

inductive RPN : Type where
  | add : RPN → RPN → RPN
  | mul : RPN → RPN → RPN
  | val : Int ⊕ Float → RPN

declare_syntax_cat rpn
syntax num : rpn
syntax rpn rpn "+" : rpn
syntax rpn rpn "*" : rpn

syntax "`[rpn| " rpn "]" : term

macro_rules
  | `(`[rpn| $num:num ]) => `(RPN.val $num)

Leonardo de Moura (May 02 2022 at 16:07):

Henrik Böving said:

Leonardo de Moura said:

Yes, Horatiu Cheval is right.
Note that, Int ⊕ Float is a notation for Sum Int Float.
That being said, I often prefer the version using ValT, the constructor names and type names often make the code easier to maintain.

In what situations would you prefer Sum over custom inductives?

I rarely use Sum. I just checked the Lean 4 codebase, and we used it in very few places. One problem is that if we have more than two cases, the patterns are inconvenient to write and the code looks cryptic. Example. 

def f (s : Nat ⊕ Int ⊕ Bool) : String :=
  match s with
  | .inl _        => "nat"
  | .inr (.inl _) => "int"
  | .inr (.inr _) => "bool"

I think better notation could address this issue, and the decision would be similar to the Prod vs. custom structure. I often regret using Prod for bigger tuples instead of a structure when maintaining the code later :)
One place where we found Sum (actually PSum) very useful is for auto-generated code. If you print mutual definitions where we show termination using well-founded recursion, you will find the PSums we use in our encoding.

Joseph O (May 02 2022 at 16:10):

for some reason when i uncomment the commented line here

declare_syntax_cat rpn
syntax num : rpn
syntax rpn rpn "+" : rpn
syntax rpn rpn "*" : rpn
-- syntax rpn+ : rpn

it crashes the server

Joseph O (May 02 2022 at 16:12):

I want to handle things like %rpn( 1 2 3 4 )

Leonardo de Moura (May 02 2022 at 16:13):

Joseph O said:

for some reason when i uncomment the commented line here

declare_syntax_cat rpn
syntax num : rpn
syntax rpn rpn "+" : rpn
syntax rpn rpn "*" : rpn
-- syntax rpn+ : rpn

it crashes the server

Could you please try with the latest nightly build? I didn't manage to reproduce the crash.

Joseph O (May 02 2022 at 16:15):

I am using leanprover/lean4:nightly-2022-04-28

Joseph O (May 02 2022 at 16:15):

image.png

Leonardo de Moura (May 02 2022 at 16:16):

Ok, your #mwe is not just

declare_syntax_cat rpn
syntax num : rpn
syntax rpn rpn "+" : rpn
syntax rpn rpn "*" : rpn
syntax rpn+ : rpn

Joseph O (May 02 2022 at 16:16):

Ok here is a MWE:

inductive RPN : Type where
  | add : RPN → RPN → RPN
  | mul : RPN → RPN → RPN
  | val : Int → RPN
  deriving Repr

declare_syntax_cat rpn
syntax num : rpn
syntax rpn rpn "+" : rpn
syntax rpn rpn "*" : rpn
syntax rpn+ : rpn

syntax "%rpn( " rpn ")" : term

macro_rules
  | `(%rpn( $num:num )) => `(RPN.val $num)
  | `(%rpn( $x:rpn $y:rpn +)) => `(RPN.add %rpn( $x ) %rpn( $y ))
  | `(%rpn( $x:rpn $y:rpn *)) => `(RPN.mul %rpn( $x ) %rpn( $y ))
  | `(%rpn( $x:rpn )) => `(%rpn( $x ))

#check %rpn(1 2 3 4 5)

Leonardo de Moura (May 02 2022 at 16:29):

It is a stack overflow when parsing #check %rpn(1 2 3 4 5). The problem is the command syntax rpn+ : rpn. We should produce an error message in this case since this kind of parser will always produce a stack overflow.

Arthur Paulino (May 02 2022 at 16:59):

@Joseph O I faced this same issue and Mario helped me with this solution

The idea is to create a syntax category specifically for sequences of syntax items of the same structure

Leonardo de Moura (May 02 2022 at 17:01):

There are many ways to encode this kind of example in Lean. Here is an example:

inductive Atom where
  | val (v : Int)
  | add
  | mul
  deriving Repr

def RPN := List Atom

def eval : RPN → (vs : List Int := []) → Except String (List Int)
  | [],          vs             => .ok vs
  | .val         v :: rpn, vs   => eval rpn (v :: vs)
  | .add :: rpn, v₁ :: v₂ :: vs => eval rpn ((v₁+v₂)::vs)
  | .mul :: rpn, v₁ :: v₂ :: vs => eval rpn ((v₁*v₂)::vs)
  | _,           _              => .error "insufficient args"

declare_syntax_cat rpn
syntax num : rpn
syntax rpn num "+" : rpn
syntax rpn num "*" : rpn
syntax rpn num : rpn

syntax "%rpn( " rpn ")" : term

macro_rules
  | `(%rpn( $num:num ))       => `([Atom.val $num])
  | `(%rpn( $x:rpn $y:num +)) => `(%rpn( $x:rpn ) ++ [Atom.val $y:num, Atom.add])
  | `(%rpn( $x:rpn $y:num *)) => `(%rpn( $x:rpn ) ++ [Atom.val $y:num, Atom.mul])
  | `(%rpn( $x:rpn $y:num))   => `(%rpn($x:rpn) ++ [Atom.val $y:num])

#eval eval %rpn(1 2 3 4 5)

#eval eval %rpn(1 1 + 3 * 5 +)

Joseph O (May 02 2022 at 17:03):

Wow thanks

Kevin Buzzard (May 03 2022 at 14:00):

Joseph O said:

Then the tutorial needs to be updated

@Joseph O Go ahead and make a brief pull request!

Joseph O (May 03 2022 at 16:18):

Kevin Buzzard said:

Joseph O said:

Then the tutorial needs to be updated

Joseph O Go ahead and make a brief pull request!

Done :)

Joseph O (May 03 2022 at 16:22):

By the way, @Leonardo de Moura I added a small thing to the syntax to embed terms, 

declare_syntax_cat rpn
syntax num : rpn
syntax rpn num "+" : rpn
syntax rpn num "*" : rpn
syntax rpn num : rpn
syntax "[" term "]" : rpn

syntax "%rpn( " rpn ")" : term

macro_rules
  | `(%rpn( $num:num ))       => `([Atom.val $num])
  | `(%rpn( [ $e:term ] ))    => `([e])
  | `(%rpn( $x:rpn $y:num +)) => `(%rpn( $x:rpn ) ++ [Atom.val $y:num, Atom.add])
  | `(%rpn( $x:rpn $y:num *)) => `(%rpn( $x:rpn ) ++ [Atom.val $y:num, Atom.mul])
  | `(%rpn( $x:rpn $y:num))   => `(%rpn($x:rpn) ++ [Atom.val $y:num])

yet 

def a := 1
#eval eval %rpn([a] 2 3 4 5)

gives the error

unknown identifier 'e✝'

cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors

Why is this happening?

Sebastian Ullrich (May 03 2022 at 16:32):

It looks like you forgot a $ in front of e in `([e])

Joseph O (May 03 2022 at 16:35):

Sebastian Ullrich said:

It looks like you forgot a $ in front of e in `([e])

Oh my bad. Then I assume the guide forgot one too

Joseph O (May 03 2022 at 16:36):

Nevermind

Joseph O (May 03 2022 at 16:37):

Thanks

Notification Bot (May 03 2022 at 16:37):

Joseph O has marked this topic as resolved.

Notification Bot (May 03 2022 at 17:06):

Joseph O has marked this topic as unresolved.

Joseph O (May 03 2022 at 17:07):

Just one small thing, using the exact same code from above, it doesn't let me have an embedded term in the middle:

def a := 1
def b := 2
#eval eval %rpn([a] [b] 3 4 5)

error:

expected ')'

any ideas?

Sebastian Ullrich (May 03 2022 at 17:18):

How does the notation accept multiple numbers? If that part is clear to you, you should be able to solve this issue by yourself.

Joseph O (May 03 2022 at 17:19):

I dont know. The syntaxes for both look almost identical:

syntax num : rpn
syntax "[" term "]" : rpn

Joseph O (May 03 2022 at 17:19):

even in the macro_rules

macro_rules
  | `(%rpn( $num:num ))       => `([Atom.val $num])
  | `(%rpn( [ $e:term ] ))    => `([Atom.val $e])

Joseph O (May 03 2022 at 17:19):

Oh wait

Joseph O (May 03 2022 at 17:19):

Nevermind, I see it now

Joseph O (May 03 2022 at 17:21):

actually implementing the rule produces the same error

| `(%rpn( $x:rpn [ $e:term ])) => `(%rpn($x:rpn) ++ [Atom.val $e:term])

Joseph O (May 03 2022 at 17:22):

expected ')'

Sebastian Ullrich (May 03 2022 at 17:24):

Yes, the rule is one part, but it doesn't by itself change what syntax the parser accepts. There is another requisite part.

Joseph O (May 03 2022 at 17:24):

I found it

Joseph O (May 03 2022 at 17:25):

Yup I fixed it, Thanks

Joseph O (May 03 2022 at 17:26):

Do we have a function in lean 4 that take a list of strings and converts and joins it with a seperator?

Sébastien Michelland (May 03 2022 at 17:27):

What about String.intercalate?

Arthur Paulino (May 03 2022 at 17:37):

@Joseph O feel free to copy it:
Link

Arthur Paulino (May 03 2022 at 17:39):

Oh, that seems to be String.intercalate!

Henrik Böving (May 03 2022 at 17:40):

And the one in stdlib is even tail recursive \o/

Joseph O (May 03 2022 at 17:46):

yet intercalate doesnt work for #eval List.intercalate " " ["h", "i"]

Henrik Böving (May 03 2022 at 17:50):

Of course not, after all you want the string and not the list variant.

Joseph O (May 03 2022 at 17:50):

Oh right

Joseph O (May 03 2022 at 17:50):

:face_palm:

Joseph O (May 03 2022 at 17:50):

There we go

Joseph O (May 03 2022 at 17:54):

Wait no way List.get uses Fin now

Joseph O (May 03 2022 at 17:54):

I wonder if the change was because of my Soup project...

Joseph O (May 03 2022 at 17:58):

Suggestion on how to make this less repetitive?

declare_syntax_cat rpn
syntax "[" term "]" : rpn
syntax num : rpn
syntax rpn num "+" : rpn
syntax rpn num "*" : rpn
syntax rpn "[" term "]" "+" : rpn
syntax rpn "[" term "]" "*" : rpn
syntax rpn num : rpn
syntax rpn "[" term "]" : rpn

syntax "%rpn( " rpn ")" : term

macro_rules
  | `(%rpn( $num:num ))       => `([Atom.val $num])
  | `(%rpn( [ $e:term ] ))    => `([Atom.val $e])
  | `(%rpn( $x:rpn $y:num +)) => `(%rpn( $x:rpn ) ++ [Atom.val $y:num, Atom.add])
  | `(%rpn( $x:rpn $y:num *)) => `(%rpn( $x:rpn ) ++ [Atom.val $y:num, Atom.mul])
  | `(%rpn( $x:rpn [ $e:term ] +)) => `(%rpn( $x:rpn ) ++ [Atom.val $e:term, Atom.add])
  | `(%rpn( $x:rpn [ $e:term ] *)) => `(%rpn( $x:rpn ) ++ [Atom.val $e:term, Atom.mul])
  | `(%rpn( $x:rpn $y:num))   => `(%rpn($x:rpn) ++ [Atom.val $y:num])
  | `(%rpn( $x:rpn [ $e:term ])) => `(%rpn($x:rpn) ++ [Atom.val $e:term])

Joseph O (May 03 2022 at 19:51):

Anyone?

Joseph O (May 03 2022 at 19:51):

Then I guess there is no way (though I doubt that)

Arthur Paulino (May 03 2022 at 19:53):

It's possible but you need to rethink your syntax structure to be more general

Joseph O (May 03 2022 at 19:57):

Arthur Paulino said:

It's possible but you need to rethink your syntax structure to be more general

Im pretty new to macros, so I don't know what structure to use. Do you have one in mind?

Arthur Paulino (May 03 2022 at 19:58):

this file contains some examples with more flexible syntaxes. Check the ones with interrogation marks

Arthur Paulino (May 03 2022 at 20:07):

For example, "+" and "*" can be grouped in a syntax category "operator". And it is optional in your term

Arthur Paulino (May 03 2022 at 20:10):

But I wouldn't bother too much about learning these details at the moment. I heard Sebastian is working on something that might cause some shake up on Lean 4 syntax

Sebastian Ullrich (May 03 2022 at 20:11):

There is no planned change to syntax itself

Arthur Paulino (May 03 2022 at 20:12):

@Sebastian Ullrich can you explain what will be changed? :pray:🏼

Sebastian Ullrich (May 03 2022 at 20:49):

It's about making macro programming more type-safe by annotating a Syntax wrapper with the carried syntax kind

Arthur Paulino (May 03 2022 at 20:52):

Ah, then we shouldn't notice too much difference except for those errors that happened when we didn't explicitly say the syntax kind?

@Joseph O can you show the definition of Atom and ++ as well?

Arthur Paulino (May 03 2022 at 21:55):

Here's a disastrously longer code that might serve the purpose of teaching about elaboration:

import Lean

inductive Atom where
  | val (v : Int)
  | add
  | mul
  deriving Repr

declare_syntax_cat    rpn_item
syntax "[" term "]" : rpn_item
syntax num          : rpn_item

declare_syntax_cat rpn_op
syntax " + "     : rpn_op
syntax " * "     : rpn_op

declare_syntax_cat              rpn
syntax rpn_item               : rpn
syntax rpn rpn_item (rpn_op)? : rpn

open Lean Elab Meta

def elabItem : Syntax → TermElabM Expr
  | `(rpn_item| $num:num) =>
    return mkApp (mkConst ``Atom.val) $
      mkApp (mkConst ``Int.ofNat) (mkNatLit num.toNat)
  | `(rpn_item| [ $e:term ]) =>
    return mkApp (mkConst ``Atom.val) (← Term.elabTerm e none)
  | _ => throwUnsupportedSyntax

def elabOp : Syntax → TermElabM Expr
  | `(rpn_op| +) => return mkConst ``Atom.add
  | `(rpn_op| *) => return mkConst ``Atom.mul
  | _ => throwUnsupportedSyntax

partial def elabRPN : Syntax → TermElabM Expr
  | `(rpn| $i:rpn_item) => do mkListLit (mkConst ``Atom) [← elabItem i]
  | `(rpn| $r:rpn $i:rpn_item $[$o:rpn_op]?) => do
    match o with
    | some o =>
      let l ← mkListLit (mkConst ``Atom) [← elabItem i, ← elabOp o]
      mkAppM ``List.append #[(← elabRPN r), l]
    | none =>
      let l ← mkListLit (mkConst ``Atom) [← elabItem i]
      mkAppM ``List.append #[(← elabRPN r), l]
  | _ => throwUnsupportedSyntax

elab "%rpn(" rpn:rpn ")" : term => elabRPN rpn

def a : Int := 8
#eval %rpn([a] 1 2 *) -- [Atom.val 8, Atom.val 1, Atom.val 2, Atom.mul]

Joseph O (May 03 2022 at 22:42):

I think I might stick with mine...

Joseph O (May 03 2022 at 22:43):

Like these I dont understand:

open Lean Elab Meta

def elabItem : Syntax → TermElabM Expr
  | `(rpn_item| $num:num) =>
    return mkApp (mkConst ``Atom.val) $
      mkApp (mkConst ``Int.ofNat) (mkNatLit num.toNat)
  | `(rpn_item| [ $e:term ]) =>
    return mkApp (mkConst ``Atom.val) (← Term.elabTerm e none)
  | _ => throwUnsupportedSyntax

def elabOp : Syntax → TermElabM Expr
  | `(rpn_op| +) => return mkConst ``Atom.add
  | `(rpn_op| *) => return mkConst ``Atom.mul
  | _ => throwUnsupportedSyntax

partial def elabRPN : Syntax → TermElabM Expr
  | `(rpn| $i:rpn_item) => do mkListLit (mkConst ``Atom) [← elabItem i]
  | `(rpn| $r:rpn $i:rpn_item $[$o:rpn_op]?) => do
    match o with
    | some o =>
      let l ← mkListLit (mkConst ``Atom) [← elabItem i, ← elabOp o]
      mkAppM ``List.append #[(← elabRPN r), l]
    | none =>
      let l ← mkListLit (mkConst ``Atom) [← elabItem i]
      mkAppM ``List.append #[(← elabRPN r), l]
  | _ => throwUnsupportedSyntax
```

Joseph O (May 03 2022 at 22:51):

also, @Arthur Paulino your version fails at #eval %rpn([1+2] 3 +)

Arthur Paulino (May 03 2022 at 22:55):

Alright, not worth debugging at the moment

Last updated: Dec 20 2023 at 11:08 UTC