пример за зависими типове и типове като доказателства на агда

Even.agda

-- boilerplate - име на модула
module Even where

-- `X : Y`
-- означава "X е от тип Y"

-- типова декларация
-- казва че "има нещо което се казва One"
-- и то е тип (": Set" частта това означава, нека мислим че Set е същото като Тип)

-- казва и че то има един конструктор, unit
-- като следствие, единствената стойност от този тип е unit (затова и се казва One - една стойност)

-- ще мислим на този тип като на "тривиална истина", защото е много лесно да дадем стойност от него
-- и тя винаги е една и съща - `unit`

-- TODO(георги): може би record вместо data
data One : Set where
  unit : One

-- TODO(георги): пример за ползване, тоест пример за патърн мач

-- типова декларация за Zero
-- няма конструктори и съответно не можем да построим никакви стойности (затова и се казва Zero - нула стойности)
-- от този тип
-- по тази причина ще мислим на него като на "лъжа" - ако ми дадеш нещо от този тип
-- значи със сигурност ме лъжеш
data Zero : Set where

-- TODO(георги): пример за ползване, тоест как се елиминират невъзможни случаи с патърн мач

-- естествени числа
-- два конструктора
-- zero - нула
-- suc - наследник (+1)
-- сигнатурата на suc казва че той взима едно естествено число (Nat), и връща друго (-> Nat)
data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

-- рекурсивна дефиниця на събиране, за пример за дефиниция на функция

-- сигнатурата казва че функцията взима две числа и връща число

-- дефиницията правим с pattern matching - щом първият аргумент е естествено число (`Nat`)
-- значи със сигурност е конструирано или с `zero` или с `suc n'` за някое друго n'
-- това n' е именно "предшественикът" на n (тоест n' = n - 1)
plus : Nat -> Nat -> Nat
plus zero m = m
plus (suc n') m = suc (plus n' m)

-- пример за стъпки в които се оценява тази функция:
-- (под 3 ще имаме предвид `suc (suc (suc zero))` и под 2  `suc (suc zero)`
-- тоест, колко пъти сме събрали 1 към нулата
-- plus 3 2
-- suc (plus 2 2)
-- suc (suc (plus 1 2)
-- suc (suc (suc (plus 0 2)
-- suc (suc (suc 2))

-- функция която взима число и връща тип, зависимост от какво е числото

-- искаме да изразим свойството "четност"
Even : Nat -> Set
Even zero = One -- в случая че числото ни е нула, знаем тривиално че то е четно
                -- съответно за да докажеш че е четно, трябва да дадеш доказателство - стойност от типа `One`,
                -- което винаги можем да направим, защото знаем конструкторът му `unit`

Even (suc zero) = Zero -- когато пък е единица, знаем тривиално че е нечетно
                       -- съответно за да докажеш че единицата е четна, трябва "само"
                       -- да дадеш доказателство за нещо невъзможно - стойност от типа `Zero`, каквито няма

Even (suc (suc n')) = Even n' -- щом числото ни не е нито 0 нито 1, знаем със сигурност че то е от вида 2 + n'
                              -- за някое n', тогава оригиналното ни число е четно <=> n' е четно

-- примери за стъпки в които се оценява Even
-- Even 2 или с други думи Even (suc (suc zero))
-- Even zero
-- One
-- т.е. за да докажеш че 2 е четно, просто дай стойност от `One` - `unit`

-- Even 3 или с други думи Even (suc (suc (suc zero)))
-- Even (suc zero)
-- Zero
-- т.е. за да докажеш че 3 е четно, просто дай стойност от `Zero` (успех)

-- деление на 2 без остатък

-- за да делим на две без остатък, трябва със сигурност да знаем че числото което делим е четно,
-- тоест ако ще делим n на две без остатък, ни е достатъчно да искаме доказателство за Even n

-- синтаксисът `(n : Nat)` ни позволява да реферирам към аргумента n по-нататък в сигнатурата на функция
-- за да можем да кажем `Even n`
div2 : (n : Nat) -> Even n -> Nat
div2 zero unit = zero -- когато първият ни аргумент е 0, знаем че Even n == One
                      -- тоест можем да проверим че стойността му е unit

div2 (suc zero) () -- когато първият аргумент е 1, знаем че Even 1 == Zero
                   -- езикът ни позволява да кажем "стига лъга, това е невъзможно"
                   -- използвайки (), за да индикираме че *не е възможно* да има обитатели на `Zero` (което е `Even 1`)

div2 (suc (suc n')) evenn' = suc (div2 n' evenn') -- в случай че числото не е нито 0, нито 1, значи със сигурност е 2 + n' за някое n'
                                                  -- тогава Even (2 + n') == Even n', и можем спокойно да извикаме рекурсивно
                                                  -- `div2 n' evenn'`, защото знаем *точно* че е вярно, че evenn' е от тип Even n'

-- имплементацията не е винаги *коректна* - може да върнем просто 1 във всички случаи, например
-- но:
-- * сме гарантирали че входът ни е валиден за "деление на две без остатък"
-- * с още малко доизпипване може да направим тип, който не ни разрешава да напишем грешна имплементация