Suppressing notation in Lean

Question

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.

Answer 1

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.

Answer 2

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.