Příspěvky

391

Vývoj / Re:Haskell, ExistentialQuantification, forall

« kdy: 06. 04. 2021, 17:08:53 »

Jak by si ho upravil aby nepadal na dělení nulou?

V principu nějak takto:

Kód: [Vybrat]

calculate : Nat -> Nat
calculate n = case isNonZero n of
  Yes prf => div 42 n prf
  No contra => ...

Ten pattern mi přijde povědomej:

Kód: [Vybrat]

calculate : Nat -> Maybe Nat
calculate n = case isNonZero n of
  Yes prf => Just $ div 42 n prf
  No contra => Nothing

versus

Kód: [Vybrat]

calculate : Nat -> Maybe Nat
calculate n = case isNonZero n of
  Just x => Just $ div 42 x
  Nothing => Nothing

Čímž v žádném případě neútočím proti ZT. Jen chci najít tu pointu.

Tahle funkce je už trochu pozdě na ten test na nenulovost, ale podstatné je, že isNonZero ti dá na zlatém podnosu důkaz nenulovosti, jejž chce div. A na rozdíl od testování obsahu Maybe se tady (u Dec) nic nezbaluje, ten důkaz (prf) existuje jen v době překladu, takže za běhu má div pouze dva argumenty, jak by běžný matematik čekal.

Tady si možná trochu ujasněme výraziva (a následně prosím vypíchni znova tu pointu):
- Za běhu funkce div nikoho nezajímá, nemá dva argumenty, není vůbec... Za běhu je na všechno pozdě a prostě děj se vůle boží.
- Cílem typů (Maybe nebo závislostních), nebo čehokoliv jiného, je přinutit mě, abych ošetřil všechny vstupy. To jsem demonstroval na tom ukázkovém kódu. Přijde string, ten může, ale také nemusí být číslo. A já se musím poprat s oběma variantama. Díky tomu, že funkce div přijímá číslo, a neexistuje funkce pro převod stringu na číslo (ale pouze převod stringu na Maybe číslo), jsem přinucen zohlednit, když se parsování nepovede. To je cíl - nedovolit překlad.

A cílem je něco takového i pro další nevalidní stavy, abych neumožnil nevalidní stav, a pokud to jinak nejde tak byl přinucen zohlednit výjimky.

392

Vývoj / Re:Haskell, ExistentialQuantification, forall

« kdy: 06. 04. 2021, 16:53:10 »

Tahle funkce je už trochu pozdě na ten test na nenulovost,

Co tím myslíš? Že jsi ten příklad přizpůsobil mému kódu, nebo to je idiomatické použití ZT?

393

Vývoj / Re:Geekovská automatická závlaha, vodárna a měření hladiny ve studni

« kdy: 06. 04. 2021, 16:25:22 »

přiložit pytlíček silikagelu nebo jiného pohlcovače vlhkosti.

Hej! To je skvělej nápad! Si budu pamatovat.

394

Vývoj / Re:Haskell, ExistentialQuantification, forall

« kdy: 06. 04. 2021, 16:14:12 »

... čímž se zvýší bezpečnost (nedojde k chybě za běhu).

Tato motivace je mi zcela jasná :-) Proto se vůbec statickými jazyky zabejvám.

395

Vývoj / Re:Haskell, ExistentialQuantification, forall

« kdy: 06. 04. 2021, 16:11:42 »

Skutečně se přidávají (v době překladu), ... "důkazy", ...

Takže ta funkce je tvořena: jméno + argumenty + důkazy? Tak je to myšleno?

Volání by pak bylo něco jako

Kód: [Vybrat]

div 10 5 (SuccNZ 4)

Takže:

Kód: [Vybrat]

calculate x = divide 42 x (SuccNZ (dec x))

?

396

Vývoj / Re:Haskell, ExistentialQuantification, forall

« kdy: 06. 04. 2021, 15:52:54 »

BTW všimni si, jak se mění signatura. Při použití záv. typů se nemění typy vstupních parametrů ani výstupu, jen se přidá dodatečný parametr, se kterým se pracuje jen v době překladu. Bez použití záv. typů musím buď změnit typ(y) vstupu (PosNat), nebo výstupu (div : Nat -> Nat -> Maybe Nat). Většinou se dělá to druhé, z čehož vyplývá, že musím nějak ověřit nebo rozbalit výstupní hodnotu (jestli tam není Nothing). U záv. typů naopak ověřuju ("dokazuju") správnost vstupu, se špatným nejde funkce vůbec zavolat (resp. vyhodnotit). Dělám tak z nějaké problematické funkce funkci totální omezením jejího def. oboru (domény). Jakmile tohle člověk pochopí, je to hezký praktický příklad omílaného "the analytical and problem solving skills acquired by studying mathematics", sice to není moc praktické (mainstreamové jazyky záv. typy téměř nemají), ale přinejmenším to rozšiřuje obzory, člověk pak ví, že vrcholem typového systému nejsou generické typy ani HKT.

Tady si tě trochu nasměruju - toto je mi velmi dobře jasné. I když se hodí, že jsi to vyjádřil.

Já mám problém se dvěma věcmi:
1/ Syntaxe
2/ Myšlenka

Můžeš si všimnout, že si mlátím zuby o to, proč přidáváš argumenty té funkci div. (Skutečně je přidáváš, nebo jen jako přidáváš? Jak vypadá volání té funkce?)

Představuji si následující kód:

Kód: [Vybrat]

divide a b = a `div` b


calculate x = divide 42 x


main :: IO ()
main = do
    args <- getArgs
    case parseArgs args of
        Left x -> putStrLn $ "ERROR: " ++ x
        Right x -> putStrLn $ "--> " ++ (show (calculate x))
    where
        parseArgs [] = Left "uvedte argument"
        parseArgs (x:_) = case (readMaybe x :: Maybe Int) of
            Nothing -> Left $ "uvedte číselný argument: " ++ (show x)
            Just x -> Right x

Jak by si ho upravil aby nepadal na dělení nulou?
Tedy předpokládám, že už někde u volání funkce calculate mi kompiler musí vynadat, že parsuju na prosté Int. Bez závislostních typů bych udělal něco jako readMaybe x :: Maybe NotZeroInt, což by mohlo fungovat (nebo jakkoliv jinak podobně).

Jak to udělám pomocí závislostních typů?

Zatím nabírám pocit, že ty ZT fungují tak nějak jako že mám obecnou kostru nějakého typu/funkce/výrazu - a pak k němu přilepuju další a další podmínky. Ale taky mohu být úplně mimo.

397

Vývoj / Re:Haskell, ExistentialQuantification, forall

« kdy: 06. 04. 2021, 01:47:57 »

Asi nejjednodušší příklad je dokazování, že nějaké číslo není nula (aby například nedošlo k dělení nulou). Takový predikát se dá jednoduše vyjádřit záv. typem:

Kód: [Vybrat]

data NonZero : Nat -> Type

Dá se to brát jako běžná uzavřená formule v logice, jež je unární a říká něco o přirozených číslech.

NonZero určuje tu nenulovost, ok. Nat určuje přirozené číslo - "pro každé přirozené číslo". A to Type tam hraje jakou roli?

NonZero je prachobyčejná funkce, takže Nat->Type je funkce z přirozených čísel do typů. Tohle je v praxi trochu trik, protože Type v překladači reprezentuje nekonečnou množinu (meta)typů různých úrovní (něco na způsob Cantorova paradoxu). To ale není pro základní pochopení záv. typů podstatné. Type je prostě "typ typů".

Kód: [Vybrat]

data NonZero : Nat -> Type

"typ NonZero je funkce která mi pro přirozené číslo vrátí typ Type". Snad ok.

Aby to bylo k něčemu v praxi, musí se k tomu ale navíc napsat funkce, která pro každý typově správný vstup řekne, zda je predikát splněn:

Kód: [Vybrat]

isNonZero : (n:Nat) -> Dec (NonZero n)

Generický typ Dec má dva konstruktory, Yes a No, kde Yes má jako parametr důkaz platnosti predikátu pro daný vstup a No důkaz kontradikce (tj. důkaz Pred->Void, protože jsme v intuicionistické logice). Existence takovéto funkce vlastně říká, že daný predikát je úplný (pro každý vstup existuje důkaz buď jeho platnosti, nebo neplatnosti).

Dobře. A tak já si tu funkci takto (humpolácky naimplementuju):

Kód: [Vybrat]

isNonZero 0 =  No (NonZero 0)
isNonZero x =  Yes (NonZero x)

Chytám se?

Problém je, že NonZero n je typ, ale Yes musí mít jako parametr nějakou jeho hodnotu. Takže třeba si všimnu, že když n je přirozené číslo, tak jeho následovník je nenulový. Takže můžu mít konstruktor SuccNZ, který mi potřebný důkaz poskytne:

Kód: [Vybrat]

isNonZero : (n:Nat) -> Dec (NonZero n)
isNonZero Z = No absurd
isNonZero (S n) = Yes (SuccNZ n)

U No je to trochu složitější, protože musím prokázat, že NonZero 0 neplatí (implikuje Void). K tomu má překladač magickou pomůcku: absurd.

OK, je to tedy hodně jinak.
Já mám teď problém, že jsi přihodil další neznámé.
Z by mohlo být Neutrální prvek.
S by mohl být ... nechytám se. A SuccNZ by mohl být následující prvek. Ale následující v jaké řadě? Jako definován pro čísla, něco jako Ord? A co znamená to *NZ?

Potom můžu mít funkci pro dělení:

Kód: [Vybrat]

div : Nat -> (y:Nat) -> NonZero y -> Nat

Tato funkce je totální, protože pro nulu ve druhém parametru není definovaná (nejde zavolat, protože nejde vytvořit instance (důkaz) predikátu NonZero Z). Takový program je zřejmě bezpečnější, protože za běhu nemůže dojít k chybě při volání div.

Všemu rozumím, až na počet těch argumentů.

Kód: [Vybrat]

let a = 5
let b = 0
let x = div a b .... ?

Proč není ta signatura takto?

Kód: [Vybrat]

div : Nat -> NonZero -> Nat

Potřebuješ dva číselné parametry, první je dělenec a to y je dělitel. Třetí argument typu NonZero y zajistí, že dělitel není nula, viz SuccNZ výše. Ten třetí "dokazovací" argument může překladač za určitých okolností uhádnout sám, ale o to teď nejde.

Proč potřebuju ten dokazovací argument? Proč prostě nemohu napsat

Kód: [Vybrat]

div : Nat -> NonZero -> Nat

, tím přeci vyjadřuju, že dělenec  je nenulový. A mašina si na pozadí odvodí, že nemohu zapsat

Kód: [Vybrat]

let a = 5
let b = 0
let x = div a b

, protože nesedí typ, b je Nat, zatímco očekvám NonZero (ten jsem si definoval výše).


Předpokládám, že to bude podobná zábava jako u těch forall. Tedy, že bych sice mohl napsat [Show], ale ExistentialQuantification jsou obecnější, a tak se na to zneužijí. Mýlím se?

398

Vývoj / Re:Haskell, ExistentialQuantification, forall

« kdy: 06. 04. 2021, 00:34:24 »

Asi nejjednodušší příklad je dokazování, že nějaké číslo není nula (aby například nedošlo k dělení nulou). Takový predikát se dá jednoduše vyjádřit záv. typem:

Kód: [Vybrat]

data NonZero : Nat -> Type

Dá se to brát jako běžná uzavřená formule v logice, jež je unární a říká něco o přirozených číslech.

NonZero určuje tu nenulovost, ok. Nat určuje přirozené číslo - "pro každé přirozené číslo". A to Type tam hraje jakou roli?

Aby to bylo k něčemu v praxi, musí se k tomu ale navíc napsat funkce, která pro každý typově správný vstup řekne, zda je predikát splněn:

Kód: [Vybrat]

isNonZero : (n:Nat) -> Dec (NonZero n)

Generický typ Dec má dva konstruktory, Yes a No, kde Yes má jako parametr důkaz platnosti predikátu pro daný vstup a No důkaz kontradikce (tj. důkaz Pred->Void, protože jsme v intuicionistické logice). Existence takovéto funkce vlastně říká, že daný predikát je úplný (pro každý vstup existuje důkaz buď jeho platnosti, nebo neplatnosti).

Dobře. A tak já si tu funkci takto (humpolácky naimplementuju):

Kód: [Vybrat]

isNonZero 0 =  No (NonZero 0)
isNonZero x =  Yes (NonZero x)

Chytám se?

Potom můžu mít funkci pro dělení:

Kód: [Vybrat]

div : Nat -> (y:Nat) -> NonZero y -> Nat

Tato funkce je totální, protože pro nulu ve druhém parametru není definovaná (nejde zavolat, protože nejde vytvořit instance (důkaz) predikátu NonZero Z). Takový program je zřejmě bezpečnější, protože za běhu nemůže dojít k chybě při volání div.

Všemu rozumím, až na počet těch argumentů.

Kód: [Vybrat]

let a = 5
let b = 0
let x = div a b .... ?

Proč není ta signatura takto?

Kód: [Vybrat]

div : Nat -> NonZero -> Nat

399

Vývoj / Re:Haskell, ExistentialQuantification, forall

« kdy: 04. 04. 2021, 23:10:47 »

To beru! Rvi to do mě! (Posledně jsem to moc nedal, tak třeba teď mi to půjde líp.)

To není v principu problém, ale vyžaduje to netriviální základy, přinejmenším dobrou znalost Curryho-Howardovy korespondence (což ale není nijak složité). Navíc ta hlavní magie okolo záv. typů ("aha moment") přijde až poté, co se člověk prohrabe mnoha zdánlivě nudnými a neužitečnými příklady. Ale jestli tě to neodrazuje, tak to můžeme zkusit, akorát moc nevím, kde začít, aby to na tebe nebylo ze začátku moc náročné, nebo naopak směšně triviální.

Zkusme pro začátek nastřelit, k čemu ZT mohou být dobré. Tím pro blbečky stylem, který jsem ukázal výše.

400

Vývoj / Re:Haskell, ExistentialQuantification, forall

« kdy: 04. 04. 2021, 22:28:35 »

[...]
... takhle jsem myslel to česky.

“Takhle česky” to moc nejde, přinejmenším ne slušně, IMHO je to dost na houby, protože univerzálně kvantifikovaná typová proměnná v antecedentu předpokládá generickou funkci, a těch je v praxi jak šafránu. Možná nějaký kovaný haskellista má nějaký triviální příklad.

Rozumím. To neva. Už jen s tím forall jsi mi ohromně pomohl. Pánbůch ti to oplať na dětech.

Takhle polopatisticky umím vysvětlit možná závislostní typy, ...

To beru! Rvi to do mě! (Posledně jsem to moc nedal, tak třeba teď mi to půjde líp.)

401

Vývoj / Re:PHP - knihovna pro generování QR

« kdy: 01. 04. 2021, 13:01:13 »

https://packagist.org/?query=qrcode

402

Vývoj / Re:Haskell, ExistentialQuantification, forall

« kdy: 31. 03. 2021, 23:53:47 »

Umí to víc?

Umí to "higher-rank types". Když se forall explicitně neuvede, je jeho působnost v případě funkcí přes celý typ. Kvantifikátory jdou vytáhnout jen z konsekventu, takže v antecedentu je nutné uvést forall explicitně.

Když by si to řekl česky (A tím nemám na mysli konsekvent a antecedent.)

Jde o to, že ∀x.(A→B) je něco jiného, než (∀x.A)→B, to první je běžný rozsah platnosti kvantifikátoru u generických typů (nejen v Haskellu), kdežto to druhé je divná haskellí věc (rank 2). Ten kvantifikátor nejde vytáhnout ven bez změny významu.

Typ je taková věc, která zajistí, aby ti tam nepřišla špatná data.

Maybe je k tomu, aby si mohl vrátit libovolnou hodnotu nebo chybu, a nemusel jsi tu hodnotu na chybu znásilňovat.

Výjimka je systém, který umožní, aby si psal optimistickej kód, protože chyba (například dělení nulou) se ti vrátí jiným způsobem a automaticky a zaručeně.

forall a ExistentialQuantification se v Haskelu používají na to, aby si mohl mít omezení jen na třídu. Například pole prvků nějaké třídy. Protože normálně by si to pole musel mít homogení, tedy pole typu. Pole třídy nejde.

... takhle jsem myslel to česky.

403

Vývoj / Re:Haskell, ExistentialQuantification, forall

« kdy: 31. 03. 2021, 21:22:42 »

Umí to víc?

Umí to "higher-rank types". Když se forall explicitně neuvede, je jeho působnost v případě funkcí přes celý typ. Kvantifikátory jdou vytáhnout jen z konsekventu, takže v antecedentu je nutné uvést forall explicitně.

Když by si to řekl česky (A tím nemám na mysli konsekvent a antecedent.)

404

Vývoj / Re:Haskell, ExistentialQuantification, forall

« kdy: 31. 03. 2021, 16:08:13 »

Tak už to mám:

Kód: [Vybrat]

{-# LANGUAGE ExistentialQuantification #-}

data Person = Person String String

x = Person "John" "Dee"

data Printable = forall x. Show x => Print x

instance Show Person where
    show (Person name surname) = "name: " ++ name ++ ", surname: " ++ surname

format :: [Printable] -> String
format xs = concat $ map apply xs
    where
        apply (Print x) = show x


main = do
    putStrLn $ format [Print x, Print 42, Print "!"]

Takže závěr: V tomto případě jsou ExistentialQuantification zneužitý na to, aby šlo vytvářet kolekci tříd, protože toto naivní v Haskellu neprojde:

Kód: [Vybrat]

format :: [Show] -> String
...
... format ["text", 42, True]

Chápu to dobře?

Předpokládám, že je to obecný koncept. Třeba na https://en.wikibooks.org/wiki/Haskell/Existentially_quantified_types píšou, že

Kód: [Vybrat]

data ShowBox = forall s. Show s => SB s

je ekvivalentní:

Kód: [Vybrat]

data ShowBox = SBUnit | SBInt Int | SBBool Bool | SBIntList [Int] | ...

s tím, že si domýšlím, že jakmile přidám instanci Show, tak se automaticky rozšíří.
Ale furt mi to příjde jen jako řešení problému pole tříd. Užitečné, a supr.

Umí to víc?

405

Vývoj / Haskell, ExistentialQuantification, forall

« kdy: 31. 03. 2021, 15:50:31 »

spinof z https://forum.root.cz/index.php?topic=24432.120

Každopádně můj fokus je momentálně na tomto: https://amulet.works/

To vypadá celkem zajímavě.

Když by si se nudil a napadl tě nějaký pěkný demonstrativní příkládek, zlobit se nebudu.

Příklad čeho? Určitě není problém, jen to pls upřesni.

forall patří do skupiny kvantifikačních typů. Takové to každý, žádný. Potuď mi teorie ok. Ale zatím mi nedochází, k čemu v praxi to může být dobré? Myslím tím nějaký vulgární praktický příklad.

Příklad s monádama: Monáda Maybe je dobrá k tomu, když chceš vrátit hodnotu nebo chybu. Užitek: Maybe je generická. Tudíž nemusíš řešit NullObject pro každý svůj vlastní typ. Díky tomu, že je to generické, můžeš udělat takovou tu věc (neznám názvosloví), kdy řadíš Maybe za sebou a nemusíš řešit rozbalení, zabalení. Máš to otypováné, tudíž se ti nemůže stát, že ti uteče nějaká větev programu, protože ty nemůžeš hned pracovat s tou hodnotou, ale musíš ji nejdřív vybalit... A podle signatury hned poznám, zda mi to vrací číslo, či číslo nebo chybu. A tak.

Jiný příklad s třídama. Třídy nedefinují typ, ale povinnost mít správnou funkci, funkce. A tím mi to rozvazuje ruce, že já nemusím řešit co je to za objekt, jeho strukturu, nedejbože jméno, ale má implementované ty funkce? To mi stačí, stejně víc nepotřebuju.

A prostě by se mi líbil nějaký příkládek pro forall. Abych věděl, že "jo ahaá, takže já si tenhle kousek kódu můžu zjednodušit na..."

Haskell má několik rozšíření, přičemž v každém znamená forall něco trochu jiného. IMHO nejpraktičtější je jeho použití v existenčních typech, například:

Kód: [Vybrat]

data Explosive = forall x. Exploder x => Expl x

Tímto způsobem se dá zbavit explicitního typového parametru, takže pak můžu mít seznam typu [Explosive], třeba [Expl Landmine, Expl Torpedo, Expl Turkey].

Co značí to Exploder?

Takže analogicky:

Kód: [Vybrat]

data Err = forall x. Maybe x => Just x
apply :: [Err] -> String
apply xs = ...
apply [Just "text", Just 42, Just True]

?

Přidám otázku: Dokážeš popsat tu ideu existenčních typů?

Exploder je nějaká třída, třeba s funkcemi explode a defuse. Ve svém příkladu akorát dosaď za Maybe nějakou třídu (a Just bych přejmenoval na nějaký unikátní konstruktor hodnot), pak to bude přesně ono.

Kód: [Vybrat]

{-# LANGUAGE ExistentialQuantification #-}

data Person = Person String String

x = Person "John" "Dee"
x2 = Person "Jan" "Marek"
x3 = 42

data Printable = forall x. Show x => x

instance Show Person where
    show (Person name surname) = "name: " ++ name ++ ", surname: " ++ surname

format :: [Printable] -> String
format xs = concat $ map show xs

main = do
    putStrLn $ format [x, x2, x3]

Pokud jsem to dobře pochopil, tak si nevím rady s tím data Printable = forall x. Show x => x. Když to zkouším podle typů, tak se mi to celé rozpadne. Evidentně špatně chápu nějaký princip.