Haskell, ExistentialQuantification, forall

Idris

  • *****
  • 1 248
    • Zobrazit profil
    • E-mail
Re:Haskell, ExistentialQuantification, forall
« Odpověď #45 kdy: 06. 04. 2021, 23:20:05 »
Kód: [Vybrat]
isNotZero x = x /= 0
Ta validační funkce je úplně nudná.
Tímto by ses dostal k typům identit, to příslušné jazyky mají, můžeš mít třeba typ n = Z a k tomu funkci:
Kód: [Vybrat]
isZero : (n:Nat) -> Dec (n = Z)Tohle je ta méně nudná část teorie záv. typů :)
(https://en.wikipedia.org/wiki/Intuitionistic_type_theory#=_type_constructor)


BoneFlute

  • *****
  • 1 599
    • Zobrazit profil
Re:Haskell, ExistentialQuantification, forall
« Odpověď #46 kdy: 06. 04. 2021, 23:45:48 »
Statické ověřování se týká konstantního kódu. Jakmile je tam nějaká dynamika, to znamená vnější svět, tak se opět vracíme k Maybe, protože to jinak nejde.
Tohle tak úplně neplatí. Když mám třeba
Kód: [Vybrat]
inc : Nat -> Nat
inc n = S n
a vyhodnotím isNonZero (inc anyNat), tak mám dokonalou typovou analýzu i pro dynamická data. Podobně jde pomocí záv. typů udělat filtr podle predikátu na Vect n a, aniž by bylo předem známo, kolik prvků predikát splňuje. Záv. typy (resp. jejich implementace založená na unifikaci) je silnější právě díky symbolickému dokazování (a má v rukávu pár dalších triků, například kvantifikované typy).

Tady si možná nerozumíme v tom, co si představujeme pod pojmem dynamika. Mám-li parsovací funkci, která mi ze stringu dělá číslo, tak nemůže vracet číslo jen tak. Bez ohledu na to, jaký nástroj zvolím. Prostě je tam rozdvojka. Pokud mám funkci, která na vstupu přijímá číslo, a volá funkci, která vyžaduje jen sudé, tak se nevyhnu rozhodování co s lichejma.

Ale to je jen jeden scénář, na který typy použiju.


Proto nejsou záv. typy zbytečná blbost,
Nic takového jsem ani nenaznačoval. Jen si prošlapávám půdu.

Idris

  • *****
  • 1 248
    • Zobrazit profil
    • E-mail
Re:Haskell, ExistentialQuantification, forall
« Odpověď #47 kdy: 06. 04. 2021, 23:52:59 »
Mám-li parsovací funkci, která mi ze stringu dělá číslo, tak nemůže vracet číslo jen tak. Bez ohledu na to, jaký nástroj zvolím. Prostě je tam rozdvojka. Pokud mám funkci, která na vstupu přijímá číslo, a volá funkci, která vyžaduje jen sudé, tak se nevyhnu rozhodování co s lichejma.
Jasně, ale pokud třeba z kódu nějak vyplyne, že například predikát Even dostává vždy dvojnásobek nějakého neznámého čísla, tak taky automaticky víš, že je sudé. Tohle jsou umělé příklady, v praxi jsou vztahy mezi hodnotami, typy a funkcemi mnohem složitější a symbolická analýza obecně odhalí víc chyb, než jen prosté kontroly konstant.

Obecně to je o tom, kde je dno rekurze. U konstant to je nula, ale mnohdy stačí nějaké větší číslo. To je třeba případ konkatenace seznamů.

BoneFlute

  • *****
  • 1 599
    • Zobrazit profil
Re:Haskell, ExistentialQuantification, forall
« Odpověď #48 kdy: 07. 04. 2021, 00:26:59 »
že například predikát Even dostává vždy dvojnásobek nějakého neznámého čísla, tak taky automaticky víš, že je sudé.

Rozumím. Toto jsem si tak docela neuvědomil.

Každopádně tato session byla užitečná, díky moc, hodně mi to dalo. Jdu žvejkat. A někdy zase.

Idris

  • *****
  • 1 248
    • Zobrazit profil
    • E-mail
Re:Haskell, ExistentialQuantification, forall
« Odpověď #49 kdy: 07. 04. 2021, 00:36:34 »
že například predikát Even dostává vždy dvojnásobek nějakého neznámého čísla, tak taky automaticky víš, že je sudé.
Rozumím. Toto jsem si tak docela neuvědomil.

Každopádně tato session byla užitečná, díky moc, hodně mi to dalo. Jdu žvejkat. A někdy zase.
Paráda :) Tak příště o těch záv. vektorech a maticích ;) Enjoy