2_typesystems.lean

-- System F

def id_nat : ℕ → ℕ := λ x : ℕ, x    -- функция id для натуральных чисел, для введения полифорфизма функция
                                    -- также должна получать тип, это можно реализовать, например, введя переменную типа

universe u
variable α : Type u

def id_my : α → α := λ x : α, x     -- полученная функция принимает некоторый x типа α и возвращает его же
                                    -- рассмотрим тип этой функции

#check id_my -- Π α : Type u, α → α -- выведенный тип является Π-типом (\Pi), добавляющий возможность сконструировать
                                    -- новый тип (α → α) для любого α из вселенной Type u;
                                    -- выражение Π x : α, β (\Pi для Π) означает, что в типе β может
                                    -- использоваться некоторое значение типа α, то есть тип β
                                    -- зависит от x : α; в случае, если β не зависит от x : α, мы пользуемся
                                    -- синтаксическим ахаром α → β

def id_my' : Π α : Type u, α → α := -- функцию можно записать самостоятельно в полном виде
  λ (α : Type u) (x : α), x         -- в этом случае в λ-абстракцию нужно явно передать тип α

#check id_my ℕ     -- ℕ → ℕ         -- для работы с конкретным типом требуется подставить вместо переменной α этот тип
#reduce id_my ℕ 42 -- 42            -- при передачи всех аргументов функция может быть вычислена

#check id_my' ℕ                     -- явная версия функции ведет себя ровно так же
#reduce id_my' ℕ 42

-- System Fω (по традиции просто λω опускается за ненужностью)

namespace mylist                    -- тот же механизм можно использовать для построения типов, зависящих от типов (λω)

  constant list : Type u → Type u   -- list принимает в качестве аргумента тип в некоторой u и возвращает новый тип из той же вселенной

  constant cons   : Π α : Type u, α → list α → list α 
  constant nil    : Π α : Type u, list α
  constant head   : Π α : Type u, list α → α
  constant tail   : Π α : Type u, list α → list α
  constant append : Π α : Type u, list α → list α → list α

end mylist

constant γ : Type u                 -- введем несколько вспомогательных констант для проверки наших конструкций
constant x : γ
constants l1 l2 : mylist.list γ

#check mylist.cons γ x              -- аппликация терма к типу и типа к типу позволяют строить конструкции типа list γ
                     (mylist.nil γ)
#check mylist.append γ l1 l2

-- λPω

constant vec : Type u → ℕ → Type u  -- вектор фиксированный длины зависит от типа элементов и размера
                                    -- тип лежит в u, тогда как (x : ℕ) лежит в ℕ, который уже лежит в u;
                                    -- таким образом, мы спускаемся на вселенную ниже и получаем зависимые типы (зависящие от "значений")

namespace vec

  constant empty  : Π α : Type u, vec α 0
  constant cons   : Π (α : Type u) (n : ℕ),     -- синтаксический сахар для вложенных Π-типов аналогичен вложенным лямбдам
                      α → vec α n → vec α (n + 1)
  constant append : Π (α : Type u) (n m : ℕ), -- склейка одинаковых по типу элеменов может проходить так же
                      vec α n → vec α m → vec α (n + m)

end vec

variables n m : ℕ
variables (v1 : vec α n) (v2 : vec α m)

#check vec.append α n m v1 v2                 -- использование функции требует указания всех типов и размеров,
                                              -- что может утомлять, тем более они могут быть выведены автоматом

-- Сигма-типы

variable θ : ℕ → Type                         -- допустим, у нас есть тип, зависящий от значения другого типа
variable k : ℕ
variable o : θ k

#check sigma.mk k o -- Σ (k : ℕ), θ k         -- sigma.mk конструирует зависимую Σ-пару (\Sigma), в которой второй элемент
                                              -- пары зависит от первого, такие типы также называют зависимыми декартовыми произведениями

#check (sigma.mk k o).1 -- ℕ                  -- к элементам этой пары можно обращаться через .1 и .2
#check (sigma.mk k o).2 -- (λ (k : ℕ), θ k) ⟨k,o⟩

-- Неявные аргументы

#check id_my ℕ 42                             -- рассмотрим уже исследованные выше функции
#check mylist.cons γ x (mylist.nil γ)         -- в каждой из них указываются типы или значения, которые могут быть выведены
#check vec.append α n m v1 v2

#check id_my _ 42                             -- во всех случаях получим то же самое
#check mylist.cons _ x (mylist.nil _)         -- получается, что все эти вещи можно и не писать
#check vec.append _ _ _ v1 v2                 -- для этого придуман синтаксический сахар неявных аргументов

def id_my_h : Π {α : Type u}, α → α :=        -- неявные аргументы пишутся так же, как и обычные, но берутся в фигурные скобки
  λ {α : Type u} (x : α), x                   -- внутри λ-абстракции также нужны {}

namespace vec_h                               -- чтоб не писать лишние подчеркивания в векторе также можно 
                                              -- воспользоваться неявными аргументами
  constant empty  : Π {α : Type u}, vec α 0
  constant cons   : Π {α : Type u} {n : ℕ},
                      α → vec α n → vec α (n + 1)
  constant append : Π {α : Type u} {n m : ℕ},
                      vec α n → vec α m → vec α (n + m)

end vec_h

#check vec_h.append v1 v2                      -- никаких лишних типов или размеров не указывается

#check @id_my_h   -- Π {α : Type u}, α → α     -- через символ @ можно смотреть полный тип, включая неявные аргументы
#check list.head  -- list α → α                -- в стандартной библиотеке активно используются неявные аргументы
#check @list.head -- Π {α : Type u}, list α → α

#check (5 : ℕ)      -- ℕ
#check (5 : ℤ)      -- ℤ
#check (id : ℕ → ℕ) -- ℕ → ℕ                   -- типы можно явно указывать для арзрешения полиморфизма

#check @vec_h.cons γ 5 -- γ → vec γ 5 → vec γ (5 + 1)
#check @id ℕ           -- ℕ → ℕ                -- другой способ указывать типы, вызывать функцию с явными аргументами через @