Почему и класс типов, и механизм неявных аргументов?

Question

Таким образом, мы можем иметь явные аргументы, обозначенные (),
Мы также можем иметь неявные аргументы, обозначаемые как {},

Все идет нормально.

Однако зачем нам также [] обозначения для классов типов конкретно?

В чем разница между следующими двумя:

theorem foo  {x : Type} : ∀s : inhabited x, x := sorry
theorem foo' {x : Type} [s : inhabited x] : x := sorry

Answer 1

Неявные аргументы вставляются автоматически разработчиком Lean. {x : Type} который появляется в обоих ваших определениях, является одним из примеров неявного аргумента: если у вас есть s : inhabited natтогда можешь написать foo s, который будет разрабатывать с точки зрения типа nat, поскольку x аргумент может быть выведен из s,

Аргументы класса type - это еще один вид неявного аргумента. Вместо того, чтобы выводиться из более поздних аргументов, разработчик запускает процедуру, называемую разрешением класса типов, которая попытается сгенерировать термин указанного типа. (См. Главу 10 в https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf.) Итак, ваш foo' на самом деле не будет принимать никаких аргументов вообще. Если ожидаемый тип x может быть выведен из контекста, Лин будет искать экземпляр inhabited x и вставьте это:

def foo' {x : Type} [s : inhabited x] : x := default x
instance inh_nat : inhabited nat := ⟨3⟩
#eval (2 : ℕ) + foo' -- 5

Здесь Лин полагает, что x должно быть natи находит и вставляет экземпляр inhabited nat, чтобы foo' один разрабатывают до термина типа nat,