Zobrazit příspěvky
Tato sekce Vám umožňuje zobrazit všechny příspěvky tohoto uživatele. Prosím uvědomte si, že můžete vidět příspěvky pouze z oblastí Vám přístupných.
Jo, to jde.Aha, ok. Dalo by se to principelně doplnit syntaxí s anonymním argumentem, něco jako `auto _ : IsEven n`? Anonymní arugment by nešlo ve funkci použít, tj. efektivně multiplicita 0. Edit: Resp. asi lepší syntaxe by byla `auto 0: IsEven n`.Co znamená ta 0 mezi `auto` a jménem implicitního argumentu?To je multiplicita (viz kvantitativní typový systém). Nula znamená erasure
Tam ten kód funguje, zkus to zkopírovat ještě jednou do zdrojáku.Jakou máš verzi Idrisu? Funguje to v 0.6.0.IsEven musí mít typový parametr. A je to jen kontrakt, že ten parametr je sudé číslo. Nějak takto to bude fungovat:No tak to je teda hnusný zápisKód: [Vybrat]data IsEven : Nat -> Type where
ZIsEven : IsEven 0
SuccSuccIsEven : IsEven n -> IsEven (2+n)
sumx : (n : Nat) -> {auto 0 prf1 : IsEven n} -> (m : Nat) -> {auto 0 prf2 : IsEven m} -> Nat
sumx n m = n + m
Pak mi musíš vysvětlit, proč to tam je.
Bohužel: "Can't find an implementation for IsEven 2."
idris2 --version # 0.6.0
Z idris2-0.6.0.tgz, stažený z webu, kompiluju na Fedoře.
Co znamená ta 0 mezi `auto` a jménem implicitního argumentu?https://idris2.readthedocs.io/en/latest/tutorial/multiplicities.html
Co znamená ta 0 mezi `auto` a jménem implicitního argumentu?To je multiplicita (viz kvantitativní typový systém). Nula znamená erasure
Jakou máš verzi Idrisu? Funguje to v 0.6.0.IsEven musí mít typový parametr. A je to jen kontrakt, že ten parametr je sudé číslo. Nějak takto to bude fungovat:No tak to je teda hnusný zápisKód: [Vybrat]data IsEven : Nat -> Type where
ZIsEven : IsEven 0
SuccSuccIsEven : IsEven n -> IsEven (2+n)
sumx : (n : Nat) -> {auto 0 prf1 : IsEven n} -> (m : Nat) -> {auto 0 prf2 : IsEven m} -> Nat
sumx n m = n + m
Bohužel: "Can't find an implementation for IsEven 2."
IsEven musí mít typový parametr. A je to jen kontrakt, že ten parametr je sudé číslo. Nějak takto to bude fungovat:Kód: [Vybrat]Ještě mi něco schází vědět?: "Mismatch between: Nat -> Type and Type."data IsEven : Nat -> Type where
ZIsEven : IsEven 0
SuccSuccIsEven : IsEven n -> IsEven (n+2)
sumx : IsEven -> IsEven -> IsEven
-- sumx : Int -> Int -> Int
sumx x y = x * y
main : IO ()
main = putStrLn $ "Hello: " ++ (show (sumx 2 4))
data IsEven : Nat -> Type where
ZIsEven : IsEven 0
SuccSuccIsEven : IsEven n -> IsEven (2+n)
sumx : (n : Nat) -> {auto 0 prf1 : IsEven n} -> (m : Nat) -> {auto 0 prf2 : IsEven m} -> Nat
sumx n m = n + m
Třeba to forall mi přišlo poněkud složité oproti přímočarým rozhraním v průmyslových jazycích.Ono je složitější, protože typové třídy mají typový parametr, kdežto rozhraní v Javě nebo Go ho mít nemusí. Jsou to rozdílné věci. Ale jak jsem psal, forall se dá zbavit použitím GADT.
Je schopen Rust vunutit, aby text byl neprázdný? Haskell to umíA Idris to umí ještě lépe, nemusíš kvůli tomu definovat nový typ
Teď mě napadlo, jak jsi zmiňoval to tehdejší forall, že existenční typy jdou vyjádřit jednodušeji pomocí GADT.Chceš na to ještě nějak navázat? Otázky k tomuto konkrétnímu příkladu?Určitě ano, ale nyní mám povinnosti.
Večer.
já se snažil vždycky psát, že ty typové informace se vymažou (můžou vymazat), když nejsou potřeba. A když jsou potřeba, tak je samozřejmě třeba je neodstraňovatOno to je matoucí, protože k type erasure dochází vždy (v tom smyslu, že tam není žádný reifikovaný typ Vect nebo Matrix, tj. instance neví, jakého jsou typu), ale používané typové parametry se předávají přímo funkcím, které je potřebují.
Přesně tak.Ano, indukční definice typu sudá čísla je pěkná ukázka. A v dalším kódu už pak opravdu můžeme mít jenom krásné garantované sudé číslo a optimalizátor tu informaci může pěkně využít.Naopak!
Jenže co se stane, když načtete uživatelský vstup a bude tam číslo liché? Nějaký implicitní nebo explicitní parser musí rozhodnout, jestli ta hodnota je v pořádku nebo není a nějak zareagovat. A to je část, co se z ukázek síly funkcionálního programování typicky vypouští.
To je na tom právě to kouzelné, že staticky typované jazyky tě přinutí, aby si zohlednil situaci když je to číslo liché. To je právě ta smetana, po které toužíme. Garance.
Na stránce o memory managementu mají hezkou ukázku, jak move semantics v jazyce bez GC potřebují od typového systémuJako v Mercury. Jo, mít u typů multiplicitu se hodí.
Však si to přelož.Tam bude zajímavější i ten vygenerovaný kód, protože s typem Nat se pojí zajímavé optimalizace.Hořím zvědavostí...
parametr tam můžeme zpropagovat, pokud to potřebujeme, pomocí této fíčury ('implicit arguments')Je rozdíl mezi type erasure a type parameter erasure
bylo by možné to opravdu udělat bez runtime prostě zpropagováním toho parametru jako běžného parametru funkce.To je přece princip těch tzv. implicitních parametrů (těch ve složených závorkách). Proto se může dělat type erasure (Vect nebo Matrix tam nikde není). Koukám, že už to začínáš chápat, to je fajn, diskuse nese ovoce.
Root.cz (www.root.cz), informace nejen ze světa Linuxu. ISSN 1212-8309
Copyright © 1998 – 2023 Internet Info, s.r.o. Všechna práva vyhrazena. Powered by Linux.