parameter

Stream: lean4

[Horatiu Cheval]

As far as I can tell (please correct me if I'm mistaken) parameter from Lean 3 no longer exists in Lean 4.
If that's the case, I'm curious as to why this is the case. Was it a conscious decision that parameter did more harm than good? I remember it being quite recommeded against and rarely used in Lean 3, and I myself filled a project with parameters at one point and regretted it afterwards. Or was it simply deemed not high priority or not worth the effort?

[Henrik Böving]

What is parameter I've never heard of it before.

[Simon Hudon]

I think parameter was broken in Lean 3. Lean 4 is making many language features into library features. parameter is an example where you can define your own in a module.

[Simon Hudon]

parameter is like variable but in your definitions, inside the same section, you don't have to / don't get to specify an argument for that variable.

Example:

section
variable (x : Nat)
parameter (y : Nat)

def foo := x + y

def bar := foo x -- y is implicitly fixed
def bar' := foo (x + 1) -- we can't pass in `y+1`

end

[Simon Hudon]

To someone used to object oriented programming, this can look a bit like class variables where you don't have to write this->myVar, you can simply refer to it as myVar.

[Joachim Breitner]

I tried to use it in mathlib, but it doesn’t affect what you write in tactics, which made it less useful than I hoped for

[Simon Hudon]

Yes, that's the big issue with it

[Horatiu Cheval]

Simon Hudon said:

To someone used to object oriented programming, this can look a bit like class variables where you don't have to write this->myVar, you can simply refer to it as myVar.

Interesting, I didn't think of this way of seeing it, but yeah. I mostly saw it is a counterpart for the pen and paper mathematical custom of saying "throughout this section, let x be something". And then it is never specified as an argument of functions, but it still is in reality

[Mario Carneiro]

Simon Hudon said:

I think parameter was broken in Lean 3. Lean 4 is making many language features into library features. parameter is an example where you can define your own in a module.

That seems not at all obvious to me. Part of the reason why parameter did not work as seamlessly as it should in lean 3 is because it was not integrated into all parts of the system, it was basically just a notation that was stored in a weird place in the environment that was not always queried. Which means that the solution would be to make sure that it is properly part of the system, and librarification doesn't seem likely to help here.

[Simon Hudon]

I did not try to implement it myself but I remember @Sebastian Ullrich early on (2019?) expressing the hope it could be implemented by users.

Trying to implement a different section-based notation, it doesn't look obvious to implement for me either. It might involve highjacking the elaborator of every command in a given section.

[Kevin Buzzard]

Are there cases when we wished we could use it in mathlib? I was quite happy operating without it

[Mario Carneiro]

You can certainly get used to working without it, but you can get used to not having a lot of things. There are plenty of places where it is useful to fix some variables for a section (or longer) and not have to pass them into everything

[Mario Carneiro]

I'm not referring to lean 3 parameter exactly, but rather something that operates roughly like it. Lean 3 parameter has a lot of issues that make it not live up to its goals, but I think that's an implementation issue rather than a design issue

[Mario Carneiro]

Not being able to reopen parameters is another issue that limits their applicability

[Patrick Massot]

Kevin, I remember I wished parameters when working on LTE. On paper you really think: I'm fixing some Breen-Deligne data and I don't want to mention it again in this section.

[Kevin Buzzard]

That is true. Perhaps I'm falling into the trap Mario suggests -- if you don't have something and know how to work around it you don't miss it

[Sebastian Ullrich]

Mario Carneiro said:

Not being able to reopen parameters is another issue that limits their applicability

I think this point is the crux of the problem - Lean 3's parameters even if worked perfectly, was really just a poor man's module system. But I still think that with only a little syntax sugar, we can get pretty close to actual module systems.

-- define basic parameterized module
-- adapted from https://agda.readthedocs.io/en/v2.6.0.1/language/module-system.html
-- but you should really just use `variable {α : Type} [LE α] [DecidableRel (α := α) (· ≤ ·)]`
-- in actual Lean code
module Sorting (α : Type) (le : α → α → Bool)
  -- takes syntax like no problem
  scoped infix:50 " ≤ " => le

  def insert (x : α) : List α → List α
    | []      => [x]
    | y :: ys => if x ≤ y then x :: y :: ys else y :: insert x ys

  def sort : List α → List α
    | []      => []
    | x :: xs => insert x (sort xs)
end Sorting

#check @Sorting.sort  -- [self : Sorting] → List Sorting.α → List Sorting.α
-- hmm, slightly suspicious output

-- module application
module SortingNat := Sorting Nat (· ≤ ·)

#check SortingNat.sort  -- List Sorting.α → List Sorting.α
-- still a bit suspicious... but perfectly usable after a little reduction
#check (SortingNat.sort : List Nat → List Nat)

-- re-open module
-- I don't think Agda or Coq let you do this?
module Sorting
  #check le  -- α → α → Bool

  def revSort (xs : List α) : List α := sort xs |>.reverse
end Sorting

#check SortingNat.revSort  -- List Sorting.α → List Sorting.α

open module SortingInt := Sorting Int (· ≤ ·)

#check (sort : List Int → List Int)

Implementation

import Lean
open Lean.Parser.Command

macro "module" n:ident params:structFields : command =>
  -- may want better error message when using the wrong case
  if params[0].getArgs.isEmpty then
    `(namespace $n
      variable [self : $n])
  else
    `(class $n:ident where $params:structFields
      namespace $n
      variable [self : $n])

macro "module" n:ident " := " mod:ident args:term:arg+ : command =>
  `(def $n : $mod := ⟨$args.getArgs,*⟩)

macro "open" "module" n:ident " := " mod:ident args:term:arg+ : command =>
  `(def $n : $mod := ⟨$args.getArgs,*⟩
    local instance : $mod := $n
    open $mod:ident)

[Simon Hudon]

Nice! It looks like the first time you write module Foo, you have to list all the parameters already. If you wanted to use parameter as one would variable, you'd need to customize the elaborator of end, right? Could you use an extension to accumulate all the parameters declared in that section? The alternative I can see is to declare the syntax as "module " ident (!"end " (command <|> parameter))* "end " ident. Which would allow us to manipulate the environment before and after the elaboration of each command. Something tells me that might be overly complex and that there might be a simpler way of getting the default elaborators to understand parameter correctly.

[Mac]

Simon Hudon said:

parameter is like variable but in your definitions, inside the same section, you don't have to / don't get to specify an argument for that variable

I am resurrecting this thread because it was just mentioned in this recent topic and I have a question about this discussion. From the description here, was Lean 3's parameter just syntactic sugar for what is essentially a reader monad?

[Mac]

To demonstrate what I mean by adapting the example:

section
variable (x : Nat)

-- parameter (y : Nat)
abbrev yM := ReaderT Nat Id
def y : yM Nat := read

def foo : yM Nat := return x + (← y)

def bar := foo x -- y is implicitly fixed
def bar' := foo (x + 1) -- we can't pass in `y+1` (?)
def bar'' := withReader (· + 1) <| foo (x + 1) -- but we actually can
def bar''' := return foo (x + 1) ((← y) + 1) -- in two ways
end

[Simon Hudon]

You can use both for similar purposes but parameter (if it's implemented correctly) has no way of supporting the reader's local : (r -> r) -> m a -> m a function.