A little project of mine

Stream: general

[Joseph O]

hello, I want to share a little project I did in lean 4. Its nowhere near complete, nor do i plan on finishing it. It has some useful elements, that could be used in a project, like heterogeneous lists, range list syntax, accessing nth element of product; but in truth this was just a project to get some experience in lean 4, and I think it did just that. I also want to thank everyone who helped me on the zulip. This used to be lean4-Tuple, but now it is much more. Here is the repo: https://github.com/crabbo-rave/Soup

[Joseph O]

I wouldn't mind any feadback

[Arthur Paulino]

Nice! Good learning experience. I'm glad to see your questions and the problems you face motivating some improvements on Lean 4. The piece of feedback that I have, just from looking at the README, is that you ate up multiple syntax variations to do the same thing here:

#eval ⟪1,"2",3.0⟫.nth 1 -- "2"
#eval ⟪1,"2",3.0⟫#1
#eval ⟪1,"2",3.0⟫@1
#eval ⟪1,"2",3.0⟫[1]
#eval ⟪1,"2",3.0⟫::1
#eval ⟪1,"2",3.0⟫∧1

It's usually better to standardize an unique notation to avoid coding styles hell

[Joseph O]

Oh yeah, the readme is very old

[Joseph O]

The syntax has changed. It just uses brackets now.

[Joseph O]

I updated it

[Joseph O]

Arthur Paulino said:

Nice! Good learning experience. I'm glad to see your questions and the problems you face motivating some improvements on Lean 4. The piece of feedback that I have, just from looking at the README, is that you ate up multiple syntax variations to do the same thing here:

#eval ⟪1,"2",3.0⟫.nth 1 -- "2"
#eval ⟪1,"2",3.0⟫#1
#eval ⟪1,"2",3.0⟫@1
#eval ⟪1,"2",3.0⟫[1]
#eval ⟪1,"2",3.0⟫::1
#eval ⟪1,"2",3.0⟫∧1

It's usually better to standardize an unique notation to avoid coding styles hell

Now i only have 3

notation:90 p "#" i => nth p #i
notation:90 p "@" i => nth p #i
notation:90 p "[" i "]" => nth p #i

Just for different programmers

[Arthur Paulino]

Languages that allow the creation of your own syntax/macros are usually feared because "Just for different programmers" can turn into "Just for different programmers not to understand each other". Taking Lean 4 source code as an example, I like that #[...] is the way to represent arrays and that I don't need to know other syntax to recognize them

[Arthur Paulino]

I don't mean to sound blunt though :sweat_smile:
It's your creation afterall, your library. I'm just expressing a worry that would come to my mind if I were to use it as a dependency

[Joseph O]

I see. Which do you suggest I stick to?

[Arthur Paulino]

That's totally up to you :smiley:

[Joseph O]

@ is pretty neat

[Mario Carneiro]

I would suggest only l[i] if you want a notation like this, and you should use getOp which magically enables this notation

[Mario Carneiro]

the reason is that, like Arthur says, there is importance in consistency across the language to help people learn things

[Mario Carneiro]

and this syntax is already used for getting elements of an array

[Joseph O]

Mario Carneiro said:

I would suggest only l[i] if you want a notation like this, and you should use getOp which magically enables this notation

What is getOp?

[Arthur Paulino]

Example. Apparently defining/implementing a getOp function in the namespace of your type allows you to do [i] on the terms of your type automagically:

inductive MyType | hi

def MyType.getOp (self : MyType) (idx : Nat) : Nat := idx

#eval MyType.hi[2] -- 2
#eval MyType.hi[3] -- 3

[Joseph O]

Arthur Paulino said:

Example. Apparently defining/implementing a getOp function in the namespace of your type allows you to do [i] on the terms of your type automagically:

inductive MyType | hi

def MyType.getOp (self : MyType) (idx : Nat) : Nat := idx

#eval MyType.hi[2] -- 2
#eval MyType.hi[3] -- 3

That wont really work for me tbh

[Joseph O]

Since i take in Fin' rather than Nat

[Joseph O]

so they would have to do h[#i], but my notation abstracts that

notation:90 p "[" i "]" => nth p #i

[Mario Carneiro]

What if they have a Fin' that they want to pass in though? I'm not sure hiding the # is a good idea

[Tomas Skrivan]

The proof by decide inside of # might not work if you do a little bit more complicated operations on indices. As an experiment, try to implement bubble sort with two for loops(not with recursion), would you run into a problem or not?

This might not apply to heterogenous lists, but for homogenous ones it is really nice to have i in Fin n. I often write a sum of all elements in a list: sum fun i => a[i]. In you notation l, i would be Nat and sum would need range specified. As I said, the use case for heterogeneous lists might be completely different and this might not apply.

[Joseph O]

Mario Carneiro said:

What if they have a Fin' that they want to pass in though? I'm not sure hiding the # is a good idea

Hmm.

[Tomas Skrivan]

@Joseph O For quite some time I wanted some mechanism for n-fold currying and uncurrying. For example, turning f : Nat -> Int -> (Unit -> Nat) -> Nat to fun x => f x[0] x[1] x[2] of type HList [Nat,Int,Unit->Nat] -> Nat. I got inspired and motivated by your project, so I finally did it.

I has to do some tricky typeclasses but I have a function huncurry n that uncurries n arguments:

example : huncurry 3 (λ (i j k : Nat) => i + j)
          =
          λ xs => xs[#0] + xs[#1] :=
by rfl

example : huncurry 2 (λ (i j k : Nat) => i + j)
          =
          λ xs k => xs[#0] + xs[#1] :=
by  rfl

What I particularly like is that the above is solved by rfl, so writing huncurry 3 f is identical to λ xs => f xs[#0] xs[#1] xs[#2]

The full code(have skipped most of the proofs):

structure HArray (Ts : List Type) where
  data : Array (Sigma (λ T : Type => T))
  h_len : Ts.length = data.size
  typed : ∀ i : Fin Ts.length, (data.get (h_len ▸ i)).1 = Ts.get i

namespace HArray

  variable {n} {Ts : List Type}

  def get (u : HArray Ts) (i : Fin Ts.length) : Ts.get i
    := u.typed i ▸ (u.data.get (u.h_len ▸ i)).2

  def getOp (self : HArray Ts) (idx : Fin Ts.length) : Ts.get idx
    := self.typed idx ▸ (self.data.get (self.h_len ▸ idx)).2

  def set (u : HArray Ts) (i : Fin Ts.length) (x : Ts.get i) : HArray Ts
    := ⟨u.data.set (u.h_len ▸ i) (⟨_, x⟩), sorry, sorry⟩

end HArray

class HCurryType (n : Nat) (F : Type) where
  Xs : List Type
  Y  : Type

attribute [reducible] HCurryType.Xs HCurryType.Y

@[reducible]
instance : HCurryType 0 Y where
  Xs := []
  Y := Y

@[reducible]
instance {X Y : Type} [t : HCurryType n Y] : HCurryType (n + 1) (X → Y) where
  Xs := X::t.Xs
  Y := t.Y

class HCurry (i : Nat) (Xs' Xs : List Type) (Y : Type) where
  index_valid : Xs'.length + i = Xs.length
  types_valid : ∀ j, i + j < Xs.length → Xs'.get ⟨j, sorry⟩ = Xs.get ⟨i + j, sorry⟩
  F : Type
  uncurry : F → (HArray Xs → Y)

attribute [reducible] HCurry.F HCurry.uncurry

@[reducible]
instance (Xs : List Type) (Y : Type) : HCurry n [] Xs Y where
  index_valid := sorry
  types_valid := sorry
  F := Y
  uncurry := λ y xs => y

@[reducible]
instance [c : HCurry (i+1) (Xs') Xs Y] : HCurry (i) (X'::Xs') Xs Y where
  index_valid := sorry
  types_valid := sorry
  F := X' → c.F
  uncurry := λ f xs =>
    let h : (Xs.get ⟨i,sorry⟩ = X') := sorry
    let xi : X' := (h ▸ xs[⟨i,sorry⟩])
    c.uncurry (f xi) xs

def huncurry (n : Nat) {F : Type} [HCurryType n F]
  [ci : HCurry 0 (HCurryType.Xs n F) (HCurryType.Xs n F) (HCurryType.Y n F)]
  (f : F) :=
    let h : F = ci.F := sorry
    ci.uncurry (h ▸ f)

macro:max "#" noWs t:term : term => `(⟨$t, by decide⟩)

example : huncurry 3 (λ (i j k : Nat) => i + j)
          =
          λ xs => xs[#0] + xs[#1] :=
by  rfl

example : huncurry 2 (λ (i j k : Nat) => i + j)
          =
          λ xs k => xs[#0] + xs[#1] :=
by rfl

[Patrick Massot]

Do you know about docs#function.has_uncurry in Lean 3?

[Tomas Skrivan]

Patrick Massot said:

Do you know about docs#function.has_uncurry in Lean 3?

Now I do :) thanks. I guess I did it partially as an exercise, but I will look into mathlib's implementation to see how it is done there.

[Tomas Skrivan]

One of my motivation was that I wanted to end up with fun x => f x[0] x[1] x[2] instead of fun x => f x.1 x.2.1 x.2.2.

[Eric Wieser]

I find the docstring for has_uncurry very confusing, as it uses alpha/beta/gamma in a totally different way to the lean code it describes.

[Joseph O]

@Tomas Skrivan wow looks nice. Glad to hear you got inspired, though the code is perhaps a bit too complicated for me to understand yet. I hope to get there soon.

[Joseph O]

Mario Carneiro said:

What if they have a Fin' that they want to pass in though? I'm not sure hiding the # is a good idea

ok I implemented getOp instead now.
The current way to access the index is

#eval [1,"2",3.0][#1]