Naivní závislostní typ (úvaha)

[Mirek Prýmek]

Hele, mám pocit, že tady někdo něco přeskočil. Právě na tomhle scénáři jsem to přeci vysvětloval.

Zkusil jsem uvést příklad, popsal jsem skoro komplet kód, popsal jsem to na několik způsobů. Víc po mě už chtít nemůžeš. Asi bych pasáž, compiletime, versu runtime vypustil. A budu se těšit, jestli mi Idris řekne něco k těm sudejm číslům.

Fair enough

[Reklama]

[Idris]

A v druhé řadě, nesouhlasil jsem s tím, že by mi to typovej systém neohlídal compile time. Proč by nemohl. Všechny informace má.

No, Idris ti to už napsal: máš pole Intů, nic víc nevíš. Třeba jsi ho načetl serializované z disku nebo ze sítě. V compile time víš jenom, že to je pole intů. Teprve až to načteš z toho disku, můžeš zjistit, že třetí, pátý a sedmdesátý osmý je Age

Hele, mám pocit, že tady někdo něco přeskočil. Právě na tomhle scénáři jsem to přeci vysvětloval.

Já tady taky moc nechápu, jak to myslíš. Ale to je fuk, dědičnost nechme stranou

[BoneFlute]

To fakt není nejjednodušší příklad na naučení. Lepší je možná začít třeba s typem pro sudá přirozená čísla nebo tak něco.

Jsem pro.

Kód: [Vybrat]

type Even = 2, 4, 6, ...

inc :: Even -> Number
inc b = a + 1

calculate :: Number -> Number -> Number

-- nepřeloží se
calculate a b = (inc b) + a

-- přeloží se
calculate a b = (inc (toEvenOr b 2)) + a
  where
    toEvenOr a default = ...
Jak by se to dělalo pomocí dep. types, prosím?

Mohl bych se @Idris připomenout? Samozřejmě chápu, že máš dost svých starostí, ale třeba budu mít štěstí.

[Idris]

To fakt není nejjednodušší příklad na naučení. Lepší je možná začít třeba s typem pro sudá přirozená čísla nebo tak něco.

Jsem pro.

Kód: [Vybrat]

type Even = 2, 4, 6, ...

inc :: Even -> Number
inc b = a + 1

calculate :: Number -> Number -> Number

-- nepřeloží se
calculate a b = (inc b) + a

-- přeloží se
calculate a b = (inc (toEvenOr b 2)) + a
  where
    toEvenOr a default = ...
Jak by se to dělalo pomocí dep. types, prosím?

Mohl bych se @Idris připomenout? Samozřejmě chápu, že máš dost svých starostí, ale třeba budu mít štěstí.

Sorry, teď teprve se k tomu vracím. Stay tuned

[Idris]

Mohl bych se @Idris připomenout? Samozřejmě chápu, že máš dost svých starostí, ale třeba budu mít štěstí.

I'm back
No, vezmu to zkrátka, jako jednoduchý příklad budeme mít unární predikát Even : Nat -> Type. Konstruktory budou dva, a sice
EvenZ : Even Z a
EvenSS : Even n -> Even (S (S n))
(tady je krásně vidět, jak typový konstruktor pro funkce je vlastně implikace, včetně stejného zápisu).
Jako příklad použití mějme funkci pro dělení dvěma, která akceptuje pouze sudá čísla:
div2 : (n:Nat) -> {auto prf:Even n} -> Nat
Pro nulu máme
div2 Z {prf=EvenZ} = 0
a jinak
div2 (S (S n)) {prf=EvenSS prf} = S (div2 n {prf})
Takže teď můžu jednoduše volat div2 n, přičemž ten druhý argument (důkaz sudosti) mi překladač odvodí sám.

[Reklama]

[BoneFlute]

div2 (S (S n)) {prf=EvenSS prf} = S (div2 n {prf})

Co prosím tě znamená to S?

[Idris]

div2 (S (S n)) {prf=EvenSS prf} = S (div2 n {prf})

Co prosím tě znamená to S?

“Z” je nula a “S” je successor.

[BoneFlute]

div2 (S (S n)) {prf=EvenSS prf} = S (div2 n {prf})

Co prosím tě znamená to S?

“Z” je nula a “S” je successor.

Supr.

Můžeš mi popsat tu šipku? Můžeš mi prosím rozvést, co dělá to Even : Nat -> Type? To jako že mám typovou funkci, která mi z přirozeného čísla udělá nový typ pomocí těch konstruktorů? Takže pokud je číslo 0, udělá z něho Even Z 0, pokud je to 4, udělá z něho Even 4 -> ... - tady se trochu ztrácím. Vidím rekurzi, vidím, že tam přeskakuje jednu hodnotu, takže to nějak vytvoří řadu ob hodnotu, ale nedokážu to přečíst.

Jak u

Kód: [Vybrat]

EvenSS : Even n -> Even (S (S n)) zajistím, že to bude zrovna sudá řada?

[BoneFlute]

div2 : (n:Nat) -> {auto prf:Even n} -> Nat
čtu jako: Vezmu číslo, a to číslo musí být aplikovatelné na typ Even. Tuto podmínku mám pojmenovanou jako prf.

div2 Z {prf=EvenZ} = 0
čtu jako: Pokud je číslo (n) nula, a je splněna podmínka prf, tzn číslo je Even, přesněji EvenZ. Toto ještě asi chápu.

div2 (S (S n)) {prf=EvenSS prf} = S (div2 n {prf})
čtu jako: Pokud následník následníka čísla n , a je splněna podmínka... Tady jsem v háji 

[BoneFlute]

Jak u

Kód: [Vybrat]

EvenSS : Even n -> Even (S (S n)) zajistím, že to bude zrovna sudá řada?

Pro každý Even n platí, že má následníka plus 2, přičemž prvním prvkem je EvenZ? to je jako definice následovníka, přičemž EvenZ je definice neutrálního prvku?

[Idris]

div2 (S (S n)) {prf=EvenSS prf} = S (div2 n {prf})

Co prosím tě znamená to S?

“Z” je nula a “S” je successor.

Můžeš mi popsat tu šipku? Můžeš mi prosím rozvést, co dělá to Even : Nat -> Type? To jako že mám typovou funkci, která mi z přirozeného čísla udělá nový typ pomocí těch konstruktorů?

Ano, je to generický typ, dostane přirozené číslo a vrátí konkrétní typ.

[Idris]

div2 (S (S n)) {prf=EvenSS prf} = S (div2 n {prf})

Co prosím tě znamená to S?

“Z” je nula a “S” je successor.

Jak u

Kód: [Vybrat]

EvenSS : Even n -> Even (S (S n)) zajistím, že to bude zrovna sudá řada?

Začíná se nulou (“Z”) a (S (S n)) v podstatě znamená n+2, takže to jsou násobky dvou.

[Idris]

div2 : (n:Nat) -> {auto prf:Even n} -> Nat
čtu jako: Vezmu číslo, a to číslo musí být aplikovatelné na typ Even. Tuto podmínku mám pojmenovanou jako prf.

div2 Z {prf=EvenZ} = 0
čtu jako: Pokud je číslo (n) nula, a je splněna podmínka prf, tzn číslo je Even, přesněji EvenZ. Toto ještě asi chápu.

div2 (S (S n)) {prf=EvenSS prf} = S (div2 n {prf})
čtu jako: Pokud následník následníka čísla n , a je splněna podmínka... Tady jsem v háji 

To prf je “proof”, tady je třeba “přepnout myšlení” z typů na formální logiku (Curry-Howardova korespondence). To prf je důkaz (formální, symbolický), že vstup je sudé číslo. Díky existenci toho důkazu můžu vesele dělit a vím, že dostanu přirozené číslo. U toho následníka si “půjčím” důkaz pro n-2 z konstruktoru predikátu, abych měl co předat v rekurzi. Zkus si to rozepsat ve FOL

[Idris]

Jak u

Kód: [Vybrat]

EvenSS : Even n -> Even (S (S n)) zajistím, že to bude zrovna sudá řada?

Pro každý Even n platí, že má následníka plus 2, přičemž prvním prvkem je EvenZ? to je jako definice následovníka, přičemž EvenZ je definice neutrálního prvku?

To není definice, je to důkaz (proof) platnosti formule. Hodnoty typů odpovídají důkazům formulí. Nedokazatelné formule odpovídají podle CHK typům bez hodnost (tzv. uninhabited types, “neobydlené”). Typově EvenZ je jedinou hodnotou typu Even 0 atd.

[Idris]

V obecnosti je vhodné představit si opravdu hodnoty typů jako důkazy příslušných výroků. Názornější je promyslet si reifikovanou verzi EvenReif : Nat -> Bool -> Type.