Hlavní navigace

Jemný úvod do jazyka Idris (2) - Některé výrazy jsou si rovnější

11. 10. 2018 14:48 (aktualizováno) Calculon

V minulém díle jsme si řekli, že v Idrisu jsou kromě „běžných“ typů také typy rovnostní, jejichž (generickou) definici si můžeme představit zhruba takto:

data (=) : a -> b -> Type where
  Refl : x = x

Konstruktor je nanejvýš jeden, a to pouze v případě, že se oba argumenty shodují. To dává smysl, připomeňte si, že typy odpovídají logickým výrokům, takže existence konstruktoru znamená, že výrok platí.

Nadefinujme si typ Planet:

data Planet = Mercury | Venus | Earth | Mars | Jupiter | Saturn | Uranus | Neptune

a funkci pro následníka planety:

total next_planet : Planet -> Maybe Planet
next_planet Mercury = Just Venus
next_planet Venus = Just Earth
next_planet Earth = Just Mars
next_planet Mars = Just Jupiter
next_planet Jupiter = Just Saturn
next_planet Saturn = Just Uranus
next_planet Uranus = Just Neptune
next_planet Neptune = Nothing

Všimněte si, že funkci deklarujeme jako totální. Návratová hodnota je monadická, protože ne každá planeta má následovníka (logicky ta poslední ne, tedy v naší soustavě Neptun).

Teď se budeme chvíli věnovat formální logice a důkazům. Jedním z nejjednodušších důkazů v kontextu našeho příkladu je konstruktivně dokázat, že po Merkuru následuje Venuše:

proof1 : next_planet Mercury = Just Venus
proof1 = Refl

V tomto triviálním případě je důkaz velice jednoduchý, hledaným konstruktorem je přímo Refl, protože Mercury se bezprostředně přepíše na Just Venus.

Pro příklad mírně složitějšího důkazu si nadefinujme funkci on_mercury, která dostane planetu a řekne nám, jsme-li na Merkuru:

on_mercury : Planet -> Bool
on_mercury Mercury = True
on_mercury _ = False

Nyní formálně dokážeme, že (∀p:Planet)p=Mercury⊃onMer­cury(p). Nejprve výrok přepíšeme jako typ:

proof2 : (planet:Planet) -> planet = Mercury -> on_mercury planet = True

Jako důkaz teď Refl neposlouží, protože on_mercury planet není hodnota (kontrolní otázka: proč?) a tento výraz nelze mimo kontext vyhodnotit. Můžeme ale použít daný předpoklad planet = Mercury. K tomu slouží operátor rewrite:

proof2 planet eq = rewrite eq in Refl

Protože proof2 dostane jako argumenty planetu a důkaz, že jde o Merkur, můžeme rovnost eq použít k nahrazení vše výskytů planet v důkazu on_mercury planet = True, což je přesně to, co rewrite eq in Refl dělá.

Jak se ale dokáže, že něco neplatí? V použité logice nemáme operátor negace, ale je snadné nahlédnout, že pokud p neplatí, tak musí platít p⊃⊥. Například onMercury(Venus)=True⊃⊥, což je následující typ:

proof3 : on_mercury Venus = True -> Void

Pro důkaz se použije klíčové slovo impossible, kterým vyjádříme, že proof3 nelze s konstruktorem Refl použít:

proof3 Refl impossible

Sdílet