Начнем с постулата. Синтаксис прост:
postulate name : type
Это утверждает, что существует некоторое значение типа type, называемое name. Думайте об этом как об аксиомах логики - о вещах, которые определены как истинные и не подвергаются сомнению (в данном случае со стороны Агды).
Далее идет определение данных. В объявлении mixfix есть небольшая недоработка, поэтому я исправлю его и объясню, что он делает. Первая строка:
data _∨_ (A B : Set) : Set where
Представляет новый тип (конструктор) под названием _∨_. _∨_ принимает два аргумента типа Set и затем возвращает Set.
Я сравню с Haskell. A и B более или менее эквивалентны a и b в следующем примере:
data Or a b = Inl a | Inr b
Это означает, что определение данных определяет полиморфный тип (шаблон или универсальный, если хотите). Set - это Agda-эквивалент * в Haskell.
Что случилось с подчеркиванием? Agda позволяет вам определять произвольные операторы (префикс, постфикс, инфикс ... обычно просто вызываются одним именем - mixfix). Подчеркивание просто указывает Agda на аргументы. Лучше всего это видно с операторами префикса / постфикса:
-_ : Integer → Integer -- unary minus
- n = 0 - n
_++ : Integer → Integer -- postfix increment
x ++ = x + 1
Вы даже можете создавать сумасшедшие операторы, такие как:
if_then_else_ : ...
Следующая часть - определение самих конструкторов данных. Если вы видели GADT от Haskell, это более или менее то же самое. Если у вас нет:
Когда вы определяете конструктор в Haskell, скажем Inr выше, вы просто указываете тип аргументов, а Haskell определяет тип всего объекта, то есть Inr :: b -> Or a b. Когда вы пишете GADT или определяете типы данных в Agda, вам нужно указать весь тип (и для этого есть веские причины, но я не буду сейчас вдаваться в подробности).
Итак, в определении данных указаны два конструктора: inl типа A → A ∨ B и inr типа B → A ∨ B.
Теперь самое интересное: первая строка classical-2 - это простое объявление типа. Что случилось с Set? Когда вы пишете полиморфные функции в Haskell, вы просто используете строчные буквы для представления переменных типа, например:
id :: a -> a
На самом деле вы имеете в виду:
id :: forall a. a -> a
И что вы на самом деле имеете в виду:
id :: forall (a :: *). a -> a
Т.е. это не просто какой-то a, но этот a тип. Agda заставляет вас сделать этот дополнительный шаг и явно объявить эту количественную оценку (это потому, что вы можете количественно оценить больше вещей, чем просто типы).
А фигурные скобки? Позвольте мне снова использовать приведенный выше пример Haskell. Когда вы где-то используете функцию id, скажем id 5, вам не нужно указывать это a = Integer.
Если бы вы использовали обычные партезы, вам нужно было бы указывать фактический тип A каждый раз, когда вы вызываете classical-2. Однако в большинстве случаев тип может быть определен из контекста (как и в примере id 5 выше), поэтому в таких случаях вы можете «скрыть» аргумент. Затем Agda пытается заполнить это автоматически - и, если не может, жалуется.
И последняя строка: λ x → y - это способ выражения Agda \x -> y. Это должно объяснить большую часть линии, единственное, что осталось, - это фигурные скобки. Я почти уверен, что вы можете опустить их здесь, но в любом случае: скрытые аргументы делают то, что говорят - они скрывают. Поэтому, когда вы определяете функцию от {A} до B, вы просто предоставляете что-то типа B (потому что {A} скрыт). В некоторых случаях вам нужно знать значение скрытого аргумента, и именно это делает этот особый вид лямбда: λ {A} → позволяет вам получить доступ к скрытому A!
person
Vitus
schedule
23.01.2015
