To nejlepší na tom je, že funkční typ odpovídá implikaci, třeba v případě toho Even n → Even (S (S n)) se vlastně říká, že když je n sudé, tak je sudé i n+2. Závislostní typy pak jen implementují kvantifikátory, jinak bychom byli ve výrokové logice.
OK, Even n → Even (S (S n)) jsem asi pochopil. Přičemž tedy, pokud není uveden další, hmm, omezení, tak to neplatí jen pro sudé, ale i pro liché. Že každé n, je-li liché, tak další n je taky liché. (Takže ta definice je nepřesná, ale už nebudu zabředávat.)
Ta definice je přesná, ta implikace platí i pro lichá čísla, jenže pro ně je antecedent vždy nepravda, a z nepravdy plyne cokoliv. Trik je v tom, že nula je sudá, kdežto jednička ne.
Aha. A jak by vypadala definice pro liché čísla?
Stejně, ale dno redukce pak je OddSZ : Odd (S Z).
Trochu jsem se v tom ztratil. Co platí:
Even n → Even (S (S n))
nebo
EvenZ : Even Z a
EvenSS : Even n -> Even (S (S n))
(Děkuji za trpělivost.)
Pak bych měl ještě jednu otázku:
Já jsem (narozdíl od tebe) vytvářel typ pro sudá čísla tak nějak "jako":
type Even = 2, 4, 6, ...
Každopádně to je typ. A pak jde o jeho použití. Zatímco já jsem si "vystačil" s funkcí:
inc :: Even -> Number
inc a = a + 1
ty tam máš spoustu bordelu kolem:
div2 (S (S n)) {prf=EvenSS prf} = S (div2 n {prf})
Každopádně by mě zajímalo, když zavolám:
calculate b = (inc b) + (div2 b)
calculate 3
Tak to v obou způsobech selže a v obou případech mě to přinutí vytvářet omáčku kolem na ošetření zda tam leze sudé číslo - což je cíl. Každopádně závislostní typy mi v tom žádnou zvláštní magii navíc nepřidají, že?