Naivní závislostní typ (úvaha)

Idris

  • *****
  • 923
    • Zobrazit profil
    • E-mail
Re:Naivní závislostní typ (úvaha)
« Odpověď #90 kdy: 23. 11. 2019, 08:54:43 »
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).


BoneFlute

  • *****
  • 1 472
    • Zobrazit profil
Re:Naivní závislostní typ (úvaha)
« Odpověď #91 kdy: 25. 11. 2019, 00:58:34 »
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]
Even n → Even (S (S n))
nebo
Kód: [Vybrat]
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]
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]
inc :: Even -> Number
inc a = a + 1

ty tam máš spoustu bordelu kolem:
Kód: [Vybrat]
div2 (S (S n)) {prf=EvenSS prf} = S (div2 n {prf})
Každopádně by mě zajímalo, když zavolám:
Kód: [Vybrat]
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

  • *****
  • 923
    • Zobrazit profil
    • E-mail
Re:Naivní závislostní typ (úvaha)
« Odpověď #92 kdy: 25. 11. 2019, 10:44:28 »
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]
Even n → Even (S (S n))
nebo
Kód: [Vybrat]
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

  • *****
  • 923
    • Zobrazit profil
    • E-mail
Re:Naivní závislostní typ (úvaha)
« Odpověď #93 kdy: 25. 11. 2019, 10:48:53 »
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]
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]
inc :: Even -> Number
inc a = a + 1

ty tam máš spoustu bordelu kolem:
Kód: [Vybrat]
div2 (S (S n)) {prf=EvenSS prf} = S (div2 n {prf})
Každopádně by mě zajímalo, když zavolám:
Kód: [Vybrat]
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

  • *****
  • 1 472
    • Zobrazit profil
Re:Naivní závislostní typ (úvaha)
« Odpověď #94 kdy: 25. 11. 2019, 13:57:27 »
Trochu jsem se v tom ztratil. Co platí:
Kód: [Vybrat]
Even n → Even (S (S n))
nebo
Kód: [Vybrat]
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]
Odd n → Odd (S (S n))
OddZ : Odd (S Z)
OddSS : Odd n -> Odd (S (S n))

Takhle by to neslo?
Kód: [Vybrat]
Odd n → Odd (S (S n))
OddZ : Odd 1
OddSS : Odd n -> Odd (S (S n))


BoneFlute

  • *****
  • 1 472
    • Zobrazit profil
Re:Naivní závislostní typ (úvaha)
« Odpověď #95 kdy: 25. 11. 2019, 14:05:51 »
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

  • *****
  • 923
    • Zobrazit profil
    • E-mail
Re:Naivní závislostní typ (úvaha)
« Odpověď #96 kdy: 25. 11. 2019, 14:39:19 »
Trochu jsem se v tom ztratil. Co platí:
Kód: [Vybrat]
Even n → Even (S (S n))
nebo
Kód: [Vybrat]
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]
Odd n → Odd (S (S n))
OddZ : Odd (S Z)
OddSS : Odd n -> Odd (S (S n))

Takhle by to neslo?
Kód: [Vybrat]
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

  • *****
  • 923
    • Zobrazit profil
    • E-mail
Re:Naivní závislostní typ (úvaha)
« Odpověď #97 kdy: 25. 11. 2019, 14:42:18 »
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.