1
$\begingroup$

I'm using the Lean computer proof assistant and customizing some notation. Here's the example I'm working with:

def comp  (X Y Z : Type*) (g : [Y, Z]) (f : [X, Y]) (x : X) : Z := g (f x)
constant X : Type
constant Y : Type
constant Z : Type
constant f : X \rightarrow Y
constant g : Y \rightarrow Z
def h := comp(X)(Y)(Z)(g)(f)

One thing that would be really convenient is being able to omit characters. In the code above, it would be nice if Lean could infer the (X)(Y)(Z) in comp(X)(Y)(Z)(g)(f).

So I was hoping that somehow it would be possible for Lean to infer X and Y and Z from g and f. Is this possible?

More generally, I am interested in any notation feature in lean which could infer types of things so as to make the notation cleaner for myself.

For instance, how do I obtain the type of something for use in further computations. That is, suppose a : A, A : Type. I want to obtain A from a and construct from it the type A \rightarrow A in a closed form involving a.

$\endgroup$

2 Answers 2

4
$\begingroup$

You can use implicit arguments (https://leanprover.github.io/lean4/doc/implicit.html#implicit-arguments lean 4 but the notation is the same in 3) to omit arguments that are inferrable from the (type of) later arguments.

As for your second question if you use implicit arguments you could write an abstract function returning A -> A given a : A if you like, but it can be more convenient to just work in an abstract setting to begin with, so that your types won't involve intermediate definitions.

$\endgroup$
2
  • $\begingroup$ Thanks very much Alex. But what is a closed from for A involving a, when a : A? As in, I want some function like Type_of $\endgroup$ Sep 7, 2022 at 15:35
  • $\begingroup$ typeof can also implemented with implicits: def typeof {A : Type} (a : A) : Type := A. So typeof 0 = Nat. (It is already in Lean, but I forgot the name.) $\endgroup$
    – Jason Rute
    Sep 7, 2022 at 16:07
3
$\begingroup$

This is just a comment regarding the typeof mentioned by Jason Rute, but I do not have the sufficient reputation to do so. Although what Jason mentioned is absolutely right, I think there is an xy problem here.

Lean is a strongly typed language in the sense that one could not define a function that accepts merely an argument of arbitrary type. For Lean to achieve "type polymorphism", the function must be defined as one that accepts an arbitrary type, and then a term of that type. So, you will always know the type of the term you are getting.

Using typeof, you can definitely do

def foo {A : Type} (a : A) : Type := typeof a -> typeof a

But this is quite meaningless, as you already know that the type of a is A, and the line above is definitionally equal to

def foo {A : Type} (a : A) : Type := A -> A

which is what Alex mentioned in his answer.

You can also write A -> A in place of foo a. Hence the best answer is that you probably wouldn't need such a function/definition in the first place.

$\endgroup$
1
  • $\begingroup$ Yeah, I couldn’t tell if it was an XY problem or they were asking for just the simplest example of using implicits. $\endgroup$
    – Jason Rute
    Sep 7, 2022 at 18:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.