Refactoring help

Stream: new members

[Shubham Kumar 🦀 (he/him)]

so currently I have the following function

def pAppl
  {s a b : Type}
  : Parser s (b -> a) -> Parser s b -> Parser s a
  :=
  λ (Parser.P p₁)  (Parser.P p₂) => Parser.P (λ inp => p₁ inp
      |>.map (λ (v₁, ss₁) => (v₁, p₂ ss₁))
      |>.map (λ (v₁, lst) => lst.map (λ (v₂, ss₂) => (v₁ v₂, ss₂))) |>.head!)

and I want it to make it more readable, I don't know what changes I should make. I want to get better at writing readable lean code

[Bolton Bailey]

The first thing that jumps out at me is that instead of having something of the form A -> B -> C after the colon, put (a : A) (b : B) before the colon. Hard to demonstrate when it's not a #mwe, though.

[Eric Wieser]

I think the answer here is probably "make an docs#Applicative instance"

[Shubham Kumar 🦀 (he/him)]

Bolton Bailey said:

The first thing that jumps out at me is that instead of having something of the form A -> B -> C after the colon, put (a : A) (b : B) before the colon. Hard to demonstrate when it's not a #mwe, though.

is putting a signature not the right way do it?

[Shubham Kumar 🦀 (he/him)]

Eric Wieser said:

I think the answer here is probably "make an docs#Applicative instance"

I was implementing an Applicative so that makes sense

[Shubham Kumar 🦀 (he/him)]

Thanks for the help, probably implementing an Applicative instance would be the best thing to do

[Mark Fischer]

Shubham Kumar 🦀 (he/him) said:
is putting a signature not the right way do it?

Here's how I read this advice:

Consider these two examples:

variable (P : Prop)

def foo : P → P := λ(p : P) ↦ p
#check foo
#check (foo)

def bar (p : P) : P := p
#check bar
#check (bar)

You'll notice how the type of foo and bar are similar. If the first thing you're doing is just introducing a variable for the antecedent, it's often cleaner to make the value an actual parameter instead of an antecedent.

[Ruben Van de Velde]

Also, you can do bar (p := q), which you can't with foo

[Shubham Kumar 🦀 (he/him)]

So I can use named variables, I didn't know that. Tangential to the problem that is cool

[Shubham Kumar 🦀 (he/him)]

Ok so I do see the pro of using it. I like the usage of defining function signature before defining the function

[Shubham Kumar 🦀 (he/him)]

Maybe I'm used to it and in lean4 isn't the idiomatic. Good to know.

Thanks!

[Mark Fischer]

Shubham Kumar 🦀 (he/him) said:

I like the usage of defining function signature before defining the function

If this preference were idiomatic, then dependent arrow types would start to feel a bit boilerplatey sometimes.

This is a bit contrived, but if you look at foo and bar:

import Mathlib

def foo : (a : ℕ) → (a ≤ 10) → ℕ := λ(b: ℕ) (h₀ : b ≤ 10) ↦ b
def bar (a : ℕ) (h₀ : a ≤ 10) : ℕ := a

For foo, you can see how the implementation sort of mirrors the type decl? To me it often feels cleaner to use parameters. Of course, that's not always desirable.

[Shubham Kumar 🦀 (he/him)]

Makes sense in this case, I haven't used lean to comment whether I like this in any scenario or not. It's ok that's the point of asking the question.

I wanted to know what is idiomatic. I got the answer

[Mark Fischer]

An example where my intuition is to do both styles at the same time:

import Mathlib

def inc := (· + 1)
def dec := (· - 1)

def foo (c : ℕ) : ℕ → ℕ :=
  if c % 2 == 0 then inc else dec

[Shubham Kumar 🦀 (he/him)]

Yeah this is also something I have seen in lean and mathlib code. The definition of foldr for list uses this

[Shubham Kumar 🦀 (he/him)]

I think it's mostly to use init as a named value

[Shubham Kumar 🦀 (he/him)]

I am growing to like this hybrid approach

[Shubham Kumar 🦀 (he/him)]

Thanks for the suggestion :smiley: