Naivní závislostní typ (úvaha)

[Idris]

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).

[Reklama]

[BoneFlute]

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í:

Kód [Vybrat] Rozbalit


Even n → Even (S (S n))

nebo

Kód [Vybrat] Rozbalit


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":

Kód [Vybrat] Rozbalit

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í:

Kód [Vybrat] Rozbalit


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


ty tam máš spoustu bordelu kolem:

Kód [Vybrat] Rozbalit

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

Každopádně by mě zajímalo, když zavolám:

Kód [Vybrat] Rozbalit


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?

[Idris]

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í:

Kód [Vybrat] Rozbalit


Even n → Even (S (S n))

nebo

Kód [Vybrat] Rozbalit


EvenZ : Even Z a
EvenSS : Even n -> Even (S (S n))


To první je typ, to druhé konstruktory typu Even (z toho logického pohledu důkazy sudosti). Možná to umí lépe vysvětlit MiPr.

[Idris]

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).

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":

Kód [Vybrat] Rozbalit

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í:

Kód [Vybrat] Rozbalit


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


ty tam máš spoustu bordelu kolem:

Kód [Vybrat] Rozbalit

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

Každopádně by mě zajímalo, když zavolám:

Kód [Vybrat] Rozbalit


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?

To jsou dvě různé věci, já se nebavil o typu reprezentujícím množinu sudých přirozených čísel, to by byl prostě podtyp bez záv. typů. Šlo o vytvoření typu, který zaručí sudost čísla *na úrovni typů*, třeba u toho div2 mi zabrání tomu, aby někdo předal liché číslo. Záv. typy se většinou používají k vynucení kontraktů, to je jejich hlavní přínos.

[BoneFlute]

Trochu jsem se v tom ztratil. Co platí:

Kód [Vybrat] Rozbalit


Even n → Even (S (S n))

nebo

Kód [Vybrat] Rozbalit


EvenZ : Even Z a
EvenSS : Even n -> Even (S (S n))


To první je typ, to druhé konstruktory typu Even (z toho logického pohledu důkazy sudosti). Možná to umí lépe vysvětlit MiPr.

É, jasně. Chtěl jsem vlastně jenom vědět, jestli se pro ta lichá čísla taky uvádí explicitně počáteční prvek, nebo jak. Takže takhle?

Kód [Vybrat] Rozbalit


Odd n → Odd (S (S n))
OddZ : Odd (S Z)
OddSS : Odd n -> Odd (S (S n))


Takhle by to neslo?

Kód [Vybrat] Rozbalit


Odd n → Odd (S (S n))
OddZ : Odd 1
OddSS : Odd n -> Odd (S (S n))


[Reklama]

[BoneFlute]

To jsou dvě různé věci, já se nebavil o typu reprezentujícím množinu sudých přirozených čísel, to by byl prostě podtyp bez záv. typů. Šlo o vytvoření typu, který zaručí sudost čísla *na úrovni typů*, třeba u toho div2 mi zabrání tomu, aby někdo předal liché číslo. Záv. typy se většinou používají k vynucení kontraktů, to je jejich hlavní přínos.

Rozumím. Zatímco já jsem vytvořil klasickou funkci kde platilo jen omezení na typ, ty jsi vytvořil košaťejší omezení jen pro tu funkci. Správně?
Díky tomu by šlo pak vytvořit "pravidla" kde by se výstupní typ funkce měnil podle toho co má za vstupy. Tak?

Každopádně ještě zopakuji otázku: Při volání té funkce na sudá čísla si stejně bude muset volající zajistit aby předával jen sudá. DT tomu nedodají žádnou další magii proti mému řešení?

[Idris]

Trochu jsem se v tom ztratil. Co platí:

Kód [Vybrat] Rozbalit


Even n → Even (S (S n))

nebo

Kód [Vybrat] Rozbalit


EvenZ : Even Z a
EvenSS : Even n -> Even (S (S n))


To první je typ, to druhé konstruktory typu Even (z toho logického pohledu důkazy sudosti). Možná to umí lépe vysvětlit MiPr.

É, jasně. Chtěl jsem vlastně jenom vědět, jestli se pro ta lichá čísla taky uvádí explicitně počáteční prvek, nebo jak. Takže takhle?

Kód [Vybrat] Rozbalit


Odd n → Odd (S (S n))
OddZ : Odd (S Z)
OddSS : Odd n -> Odd (S (S n))


Takhle by to neslo?

Kód [Vybrat] Rozbalit


Odd n → Odd (S (S n))
OddZ : Odd 1
OddSS : Odd n -> Odd (S (S n))


Jo, takto. Ta 1 se expanduje na (S Z), ale to je jen pozornost od překladače.

[Idris]

To jsou dvě různé věci, já se nebavil o typu reprezentujícím množinu sudých přirozených čísel, to by byl prostě podtyp bez záv. typů. Šlo o vytvoření typu, který zaručí sudost čísla *na úrovni typů*, třeba u toho div2 mi zabrání tomu, aby někdo předal liché číslo. Záv. typy se většinou používají k vynucení kontraktů, to je jejich hlavní přínos.

Každopádně ještě zopakuji otázku: Při volání té funkce na sudá čísla si stejně bude muset volající zajistit aby předával jen sudá. DT tomu nedodají žádnou další magii proti mému řešení?

Ano, volající to musí zajistit, většinou to ale zařídí překladač automaticky. To je princip záv. typů, když volající něco nezajistí, co je dáno kontraktem, program se nepřeloží místo zkolabování za běhu.