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.
V Idrisu jsem taky našel funkci á la panic (builtins.idris_crash).Jenže to normálně použít nejde, jen ve funkci, která je explicitně partial, což se prakticky nepoužívá (a v produkci nikdy). Takže tohle se taky vůbec nepřeloží.
Tak jistě, když se ti počítač vznítí a ty na něj chrstneš kýbl vody, tak to asi Idris nezachrání. Ale donutí tě náležitě ošetřit všechny logické chyby v kódu (typu dělení nulou, že se nevolá head na prázdný seznam apod.).Věřim ti, že obecně Idris více tlačí uživatele do ošetření chyb, ale ten rozdíl je kvantitativní...Je to stejně jako v Haskellu, panikovat v konstruktoru můžeš, ale slušné je vrátit `Result` což je to samé co `Either`...Lepší by bylo si tu slušnost od autora kódu vynutit: Kašleš na chyby? Tak to mi můžeš, syntax error
Lepší by bylo si tu slušnost od autora kódu vynutit: Kašleš na chyby? Tak to mi můžeš, syntax errorJe to stejně jako v Haskellu, panikovat v konstruktoru můžeš, ale slušné je vrátit `Result` což je to samé co `Either`...V Rustu to bude panic?Problém je v tom, že v Idrisu se mi nestane to, co se mi stane v C# v tom příkladu, který jsem uváděl. Že tu chybu neodchytím, tedy nezpracuji, tedy jsem tu chybu nezohlednil.To je jedno ne? Hodnota toho typu nebude vytvořena, pokud konstruktor vyhodil výjimku...
Taky že je, například v Julii (ta je extrabuřt, je dynamicky typovaná, ale pozná stabilně otypovaný kód a odvodí si všechny typy).Jsou náročné na čas výpočtu v době překladu, za běhu ne.Ano, ano, sorry.
A platí o opak, že za běhu by to mělo být rychlejší.
Teď jsi na to kápnul, ten program v Idrisu se nepřeloží, pokud nejsou správně ošetřeny všechny chyby.Zákazník: Tak jsem zkoušel vaši aplikaci a je úplně k ničemu. Jsem tam normálně zadal číslo, a ono to spadlo.To je ale něco jiného, to spadlo, protože nebyla dobře ošetřena chyba
Já: To je jedno ne?
V Rustu to bude panic?Problém je v tom, že v Idrisu se mi nestane to, co se mi stane v C# v tom příkladu, který jsem uváděl. Že tu chybu neodchytím, tedy nezpracuji, tedy jsem tu chybu nezohlednil.To je jedno ne? Hodnota toho typu nebude vytvořena, pokud konstruktor vyhodil výjimku...
Slušný vývojář tu výjimku odchytí a vypíše třeba “Sorry vole error”.Zákazník: Tak jsem zkoušel vaši aplikaci a je úplně k ničemu. Jsem tam normálně zadal číslo, a ono to spadlo.Problém je v tom, že v Idrisu se mi nestane to, co se mi stane v C# v tom příkladu, který jsem uváděl. Že tu chybu neodchytím, tedy nezpracuji, tedy jsem tu chybu nezohlednil.To je jedno ne? Hodnota toho typu nebude vytvořena, pokud konstruktor vyhodil výjimku...
Já: To je jedno ne?
Doplnění: Jsou náročné na čas výpočtu v době překladu, za běhu ne. Nicméně SPARK se svou formální verifikací je na tom hůře, kdysi na nějaké přednášce někdo z NASA vykládal, jak se jim kód překládá týden. Ale pak věděli, že je absolutně bezpečnýAkorát cena za to je,Imho statické typy mají jiné problémy.
Namátkou:
- jsou náročné na čas výpočtu
- jsou náročné na vývoj jazyka
- jsou náročné na skill uživatele
- lidé nechápou co to je statické typování
Idris to má stejně.Případně ještě se zeptám obecně: Jaké jsou v Haskellu a Idrisu pravidla ohledně koherence? Dejme tomu, že ve svém programu používám knihovny libA a libB, knihovna libA definuje typeclass Tc a libB typ Foo. Můžu instanciovat Tc pro Foo?
Na toto jsem nedostal odpověď, tak jsem se zeptal na SO. TL;DR Haskell dovoluje orphan type instances vč. odvozených z dependencí. (Je Idris v tomto jiný? Asi bych to nečekal.)
BTW v Idrisu jde garantovat i vlastnosti návratových hodnot, nejen vstupních parametrů.O to nejde.C#, Java,Bavíme se o vstupu od uživatele, tzn. tam z principu to musí vyhodit chybu za běhu při načítání dat. Pokud při načítání dat chyba nenastane a úspěšně je vytvořena příslušná hodnota příslušného typu v C# nebo Javě (o Py to neplatí), tak pak přece není už důvod, aby to padalo někde dále, ne?Pythonmi tu kontrolu udělat nepřinutí. Data corupted sice nenastane (jsi-li alespoň trochu šikovnej), ale spadne to až za běhu.
Samozřejmě, že ten scénář musím zohlednit v runtime.
Problém je v tom, že v Idrisu se mi nestane to, co se mi stane v C# v tom příkladu, který jsem uváděl. Že tu chybu neodchytím, tedy nezpracuji, tedy jsem tu chybu nezohlednil.
Částečně by toto řešil systém Checked Exception, od kterých se ale bohužel upouští. Úplně netuším proč. (C# je třeba schválně nemá.)
BTW až se budeš cítit na definici decIsEven, dej vědětKdybych tam cpal čísla ze vstupu, musel bych si to ověření sudosti (prfX) vyrobit sám a předat ho explicitně.Mohl by si mi ukázat, jak by to vypadalo?
Akorát cena za to je, že ty šikovné typy pro ověření musí někdo napsat. Pro základní věci (čísla, seznamy) je má standardní knihovna, nicméně pro méně typické věci (třeba i ta jednoduchá sudost) to musí napsat laskavýTechnicky vzato to ekvivalentní samozřejmě není (specificky tahle řádka uričtě ne), ale smysl kódu je v zásadě stejný. Na začátku se buď vytvoří hodnota daného typu, nebo se vyhodí chyba...Je ekvivalentne.Není.
Liší se technické detaily, v Javě například to bude muset mít objekt, nebudeš moct použít infixové operátory a řada dalších technických rozdílů...
Na technické detaily ti zvrací alík.
Liší se hlavně záruky.
V C# můžu tu validaci zapomenout. Skončí mi to výjimkou u assert v run-time. Zatímco v Idrisu mi to přinutí tu kontrolu udělat compile-time. To je ta zásadní motivace, proč se všechny ty šaškárny s typama dělají.
Idris mě přinutí tu kontrolu udělat.
C#, Java, Python mi tu kontrolu udělat nepřinutí. Data corupted sice nenastane (jsi-li alespoň trochu šikovnej), ale spadne to až za běhu.
Do třetice:
V Idrisu (a Haskellu) - nalinkuju si nějakou knihovnu, použiju a pokusím se přeložit, a ono to začne řvát tady a tady a tady a tady... opravím, přeložím, běží.
V C# - nalinkuju si nějakou knihovnu, použiju, a úspěšně přeložím, spustím, a ono to začne padat tehdy, a tehdy, a tehdy, a tehdy... nejlépe u zákazníka.
To nevím, specifikované to není a závisí to na verzi překladače (novější jsou chytřejší). Když to překladač nenajde, musí se předat explictně {prf1 = isevenN}.Tady by mě zajímalo, jaká jsou pravidla pro scoping té anonymní instance IsEven. Jak daleko může být od místa volání sumx, aby to kompilátor ještě našel / dosadil implicitní arg? Pokud by to bylo v externím kódu, muselo by se to třeba nějak importovat?Kód: [Vybrat]total main : IO ()
main = do
Just n <- readNat | _ => putStrLn "not a natural number"
let Yes _ = decIsEven n | _ => putStrLn "n isn't even"
Just m <- readNat | _ => putStrLn "not a natural number"
let Yes _ = decIsEven m | _ => putStrLn "m isn't even"
putStrLn $ "Hello: " ++ (show (sumx n m))
Jasně, včera jsem to už zkoušel, abych viděl, jak se současná verze chová.Kdybych tam cpal čísla ze vstupu, musel bych si to ověření sudosti (prfX) vyrobit sám a předat ho explicitně.Mohl by si mi ukázat, jak by to vypadalo?
total main : IO ()
main = do
Just n <- readNat | _ => putStrLn "not a natural number"
let Yes _ = decIsEven n | _ => putStrLn "n isn't even"
Just m <- readNat | _ => putStrLn "not a natural number"
let Yes _ = decIsEven m | _ => putStrLn "m isn't even"
putStrLn $ "Hello: " ++ (show (sumx n m))
Tak mám spousta více či méně blbejch otázek:1. To jsou prerekvizity, které chceš (sudost argumentů). To "auto" znamená, že si to má překladač ověřit sám.
1/ proč tam musím uvádět {auto 0 prf1 : IsEven n} ?
2/ proč je to mezi šipkama? Ta funkce má jen tři parametry, ne pět.
3/ co to vlastně to {auto 0 prf1 : IsEven n} říká?
4/ proč tam ten prf1 musí být, když tam nikde nefiguruje? Proč musí být různý? prf1 a prf2
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.