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.
kamarad v zamestnani furt jede z prikazove radkyTo dělám dost často taky
někdy z donucení (vzdáleně na serveru), ale často i lokálně. Na mnohé věci to stačí.
Cestovat lze kupodivu i s manželkou a dětmi, dokud jsou malé.Právě, dokud jsou malé, pak už se to komplikuje...
WSL jakozto emulator Linuxoveho prostrediOn to ani není emulátor, ale virtualizace s plným linuxovým jádrem (ve WSL 2, první verze jen překládala syscally). Ale to je nepodstatné.
ovladal i Windowsovskou cast disku. Dale bych chtel, abych Python i Javu mohl mit nainstalovanou jenom na to WSLTo není problém, na disk má WSL přístup a aplikace instalované ve WSL jsou jen pro WSL.
pripadne jake to ma nevyhody?Nevýhody to asi nemá, WSL 1 mělo pomalejší I/O, WSL 2 naopak chce o něco více paměti (plná virtualizace si alokuje velký blok paměti, ve WSL 1 běží každá aplikace nezávisle a jen syscally se překládají za běhu). Pokud je cílem mít Linux pro vývoj (nestačí unixový macOS), tak mě nenapadá žádný potenciální problém (sám jsem na nic nenarazil při používání WSL).
Parádaž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.
Tak příště o těch záv. vektorech a maticích 
Enjoy
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.
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]Ta validační funkce je úplně nudná.isNotZero x = x /= 0
isZero : (n:Nat) -> Dec (n = Z)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
inc : Nat -> Nat
inc n = S n
Umí to víc?Z jiného soudku pak jsou záv. součtové a součinové typy, ty se hodí třeba u těch vektorů.
Takže pokud to chápu dobře, tak ZT dělají to, že nechají ten Int Intem, jen přidají pravidla navíc. To pravidlo se tam propaguje pomocí těch dalších argumentů. A kompilátor to "nějak" použije pro ověření.Přesně! Nechají celočíselný typ (nebo jakýkoliv jiný) na pokoji a jen přidají další argument s "důkazem".
Mám otázky:1. Zdá se, že správně
- Uvažuju správně?
- Proč jsou ty ZT tak složitý? Proč nestačí primitivní validační funkce? že by mi unikl ještě třetí scénář validace? Nebo to umí víc?
- Umí to víc?
safeminus : (n:Nat) -> (m:Nat) -> GreaterEq n m -> NatTady se domnívám že se jeden z nás plete. Podle mne bez závislostních typů si můžeš ohlídat i nenulovost, neprázdnost řetězce, etc.Chápeš to dobře, nenapsal jsem explicitně "v době překladu" (compile time). Mea culpa.
[...]
Rozdíl je v tom, že, pokud to dobře chápu, bez ZT mi to vynutí (zbytečný) Maybe, což bude trochu matoucí. Zatímco ZT v pohodě při překladu odvodí, že to "nechci" a nepřeloží. Bez ZT runtime, s ZT compiletime.
Ale ta funkce div tam je, ne? A počítá za běhu.No, trochu si zatrucuju: já bych to tak řekl :-) Ale rád si to nechám vysvětlit.- 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ží.To bych takhle neřekl, myslím, že jádro věci je, že za běhu nikoho nezajímá její třetí argument.
Teď jsem si uvědomil, že to parsování vstupu je trochu zavádějící. Protože je to jen jedna množina problémů. Pak tu mám druhou, například takto:Tohle je super příklad, vybízí k napsání funkce minus nad Nat, která je totální a akceptuje jen vstupy, kde menšenec je větší nebo roven menšiteli.Kód: [Vybrat]Tam mě žádné Maybe nezachrání.divide a b = a `div` b
calculate x = divide 42 x
main :: IO ()
main = do
putStrLn $ "--> " ++ (show (calculate (a + b)))
where
a = 4
b = -4
Jo, to by šlo.Kód: [Vybrat]Šlo by? Nebo se vzdaluju té myšlence ZT, a přiohýbám si to klasice?calculate : Nat -> Maybe Nat
calculate n = case isNonZero n of
Yes prf1 => case isNotAllowedValues n of
Yes prf2 => Just $ div 42 n prf1 prf2
No _ => Nothing
No _ => Nothing
- 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ží.To bych takhle neřekl, myslím, že jádro věci je, že za běhu nikoho nezajímá její třetí argument.
- Cílem typů (Maybe nebo závislostních), nebo čehokoliv jiného, je přinutit mě, abych ošetřil všechny vstupy.[...] jsem přinucen zohlednit, když se parsování nepovede. To je cíl - nedovolit překlad.Jo, takhle to je. Bez záv. typů si může člověk ohlídat jen běžné typy (číslo vs. řetězec apod.), ktežto u záv. typů jdou hlídat i hodnoty (nenulovost, neprázdnost řetězce atd.). Je to prostě stejný princip o krok dál (i když implementačně to je o dost složitější a matematicky taky, typy už nejsou jedna kategorie, ale celá kumulativní hierarichie toposů).
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.