Arguments vs parameters

Stream: lean4

[Joachim Breitner]

Patrick Massot schrieb:

I’m not sure what is the difference between arguments and parameters.

A convention thats sometimes helpful (by being pedantic) is that arguments are what you find in a function application, while parameters (sometimes called “formal arguments”) are the things in function declarations (or binders in general). Arguments can be complex expressions, parameters are always variables (or _, I guess).

[Simon Dima]

There's also a slight collision with the terminology for inductive type formers, where we distinguish between parameters and indices, which leads to amusing formulations like "If the constructor's parameter is a parameter" (source).

[Joachim Breitner]

Yes, indeed. All parameters are equal, but some parameters are more equal than others. The others are called indices.

[Simon Dima]

Joachim Breitner said:

The others are called indices.

And with constructors we even have a three-class society with parameters, indices and "others"!

inductive Vec (α : Type) : Nat -> Type where
  | nil : Vec α 0
  | cons n (a: α) (as: Vec α n): Vec α (n+1)

#check Vec.cons
-- Vec.cons {α : Type} (n : Nat) (a : α) (as : Vec α n) : Vec α (n + 1)

Here I'm not sure what the correct name for the "others" a and as are. In a sense they're the "real" arguments to the constructor, beyond the arguments to the inductive type former which every constructor must take. In the documentation comments for ConstructorVal, the word "fields" is used to refer to both indices and "others", which sort of makes sense since those are the constructor arguments which a match provides and which potentially need to be represented in compiled code (unless they're irrelevant), but it'd be nice to have a word which just means "others" in this context without having to say "arguments of a constructor which are neither parameters nor indices".

[Joachim Breitner]

I fear “parameters of a constructor which are neither parameters nor indices of the inductive type” is just what it is.

If we have mutual inductive, then the parameters of all inducitves have to be the same, and they are also parameters of the constructors. One could thus call them the “common prefix”. Not that that helps a lot.

[Mario Carneiro]

the third class is called "arguments", and they are also separated into recursive and nonrecursive arguments depending on whether their type contains the inductive type being defined

[Mario Carneiro]

arguments are not parameters, the parameters of a constructor are the same as the parameters of the inductive type

[Mario Carneiro]

indices are not arguments to the constructor (expressions in the arguments appear in the resulting type of the constructor as indices for the inductive type), so there are only two kinds of variables going into a constructor

[Joachim Breitner]

Fair, but that’s then a different (and conflicting) parameter/argument distinction convention than the one I describe, isn't it?

[Simon Dima]

Mario Carneiro said:

indices are not arguments to the constructor (expressions in the arguments appear in the resulting type of the constructor as indices for the inductive type), so there are only two kinds of variables going into a constructor

I'm not fully sure I understand what you mean here, let me try to reformulate what I think you're saying:

• type formers have parameters and indices, constructors have parameters and arguments, and each of these is a partition of everything a type former or constructor can be applied to
• in the expression @Vec.cons Bool n .true v, the constructor Vec.consis applied with the parameter Bool and the arguments n, .true and v (v being a recursive argument, the others nonrecursive)
• in the expression @Vec Bool (n+1) which is the type of the previous expression, the type former Vec is applied with parameter Bool and with index n+1
  Is that right?

[Notification Bot]

10 messages were moved here from #lean4 > A version of check displaying only explicit arguments. by Patrick Massot.

[Mario Carneiro]

:+1: