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.
Motáme se pořád v kruhu. Lazy vyhodnocení je hezké, ale má nezanedbatelný overhead. Pokud chci, aby Haskell nebyl lazy, jde to udělat, ale je to narovnávák na ohýbák, lazy kód tím rozbiju.Už to tu zaznělo. Proč v C striktnost není ohýbák? Když v C použiju lazy techniky, tak se mi nemůže stát, že tím něco rozbiju (dosáhnu nežádoucího chování)?
Zkusím tady nadhodit myšlenkový experiment, který snad ukáže, co se mi celé na té myšlence náhrady testů typy nelíbí.Díky za příspěvek. Já jsem to celé sice původně podával jako, že praktičnost mě až tak moc nezajímá, ale děkuji za pěkný rozbor. V mnohém máš určitě i pravdu.
...
Myslím, že alespoň v tom, co dělám já, by ty ukázky často byly k ničemu. Třeba u toho polygonu by ze stroje vypadla řada čísel - souřadnic bodů polygonu, ale dokud si to nenakreslíš, tak nevidíš co to vlastně testuje. A to už je jednodušší si ty zajímavé příklady nejprve nakreslit a potom je, u komplikovaných případů třeba i okomentované a s naskenovaným obrázkem, zadat do unit testů.Hmm, může být.
Ok, beru osobní věci zpět. Každopádně můj příspěvek byl z výrazně větší části k tématu, možná bys tedy mohl zareagovat spíš na ty věcné kusy.Byl. Už jsem si myslel, že to tady nikoho nezajímá ;-)
Dependent typy z principu nemohou dokázat korektnost např. převodu stringu na číslo. Jak by se v typu fce convert: String -> Maybe Nat vyjádřilo, zda se očekává stringový vstup v desítkové nebo šestnáctkové soustavě? Podle mě je to principiálně nemožné, a stejně tak není možné ani vyjádřit korektnost implementace převodu. V Idris se asi dá vyjádřit, že funkce doběhne, a že nezpanikaří, ale to je málo.Já v těch závislostních typech nejsem kovanej, takže takto si to předstvuju v pseudokódu, jak to chápe typový systém:
parseFromDec :: Str -> Int = ('0' -> 0) | ('1' -> 1) | ... | ('9' -> 9)parseFromDecM :: Str -> Maybe Int = ('0' -> Just 0) | ('1' -> Just 1) | ... | ('9' -> Just 9) | _ -> NothingUnit testy slouží jako vždy up-to-date dokumentace. U jednoduchých věcí se dá samozřejmě hodně věcí vyčíst z typů (hezký příklad je tady: http://funkcionalne.cz/2014/08/types-will-carry-you-over-the-monads/), ale u složitějších je prostě hezké mít chování zdokumentované na příkladech, místo potřeby rozjímat nad důsledky komplikované typové signatury. Navíc je slušnost mít knihovny zdokumentované, tak proč to rovnou nedělat unit testy? (podívejte např. sem: https://doc.rust-lang.org/std/iter/trait.Iterator.html), všechny Examples jsou rovnou spustitelné unittesty zapsané do docstringů funkcí.Obecně s tebou naprosto souhlasím. Však já jsem nikde nepsal, že testy jsou zlo.
Unit testy jednoduchým způsobem ověřují chování v krajních a nečekaných případech. Když jsem psal implementaci funkce testující, zda je bod uvnitř polygonu, rovnou napíšu test, jak se chová bod na hraně, jak se chová v polygonu, který není uzavřený, jak se chová v polygonu který protíná sám sebe. Nedovedu si představit, jak by mohlo být takové chování zřejmé z typu funkce. Možná, až BoneFlute přestane "být stále student", nějak pěkně to vyřeší, to by mě pak docela zajímalo.Byl jsem línej, a napsal jsem si generátor unittestů. Takovej ten postup, kdy si napíšeš prototyp, a pak na něj začneš psát testy - úplně špatně podle TDD, já vím.
Unit testy jsou šablony funkčního kódu, který používá knihovnu kanonickým způsobem. Kód mohu copy'n'pastnout do vlastního projektu a upravit podle potřeby. Typy tohle neumí.Viz ten generátor.
Každopádně co se týče (abych trochu poskočil v tématu) původního dotazu BoneFluteho, mám dost podobný dojem jako Jirsák, že BoneFlute našel novou modlu, o které téměř nic neví, ale o to více ji chválí. Tím dependent typy nechci shazovat, je možné že se v budoucnu ukáží užitečné a rozšíří se.Psal jsem hned můj první příspěvek: "získal jsem nezdravé přesvědčení". A nebo, že "A snažím se zchladit své nadšení hledáním, kde to má hranice." Taky jsem psal, že se snažím použít typy co to jde, a na zbytek testy.
Ale myslenka zustava stejna. Ja jako programator nemuzu ve vysokourovnovem jazyce optimalizovat na nizke urovni.Ano. To prakticky vždycky. Rád na přednáškách tvrdím, že je třeba psát kód tak, aby ho kolegové mohli intuitivně použít i když budou našrot.
Musim spolehat na kompilator. A asi je to vetsinou dobre (v mem pripade urcite :-D)
Nepřímou.Příklad: mám kolekci objektů, u které si kompilátor z typové signatury odvodí, že jsou imutablePardon že se vám do toho pletu, ale co má immutabilita společného s datovými typy? Takovou optimalizaci můžu stejně tak udělat i v dynamicky typovaném jazyce. V typovém systému to žádnou výhodu navíc mít nebude.
Důležitější je asi obsah, než název. Název vlákna naznačuje, že jde o srovnání, ale text prvního příspěvku je jednoznačný pokus (úspěšný) o rozpoutání flamewar.Já jsem o žádné flamewar zájem neměl. Text mého příspěvku k flamewar nenabádal. Ale beru tě jako nutné zlo.
Iterátor nemá typ? To, že neumožňuje náhodný přístup je typová vlastnost. Iterátor jsem zvolil z nějakého důvodu. Pokud ten důvod nemám, tak nebudu kompilátoru tvrdit, že má použítá iterátor, ale nechám to na něm.To je ale dost nizkourovnova zalezitost. Myslim, ze v jazycich vyssi urovne s tim stejne moc neudelame, protoze jsme tak daleko abstrahovali od HW, ze nemuzeme optimalizovat na urovni l1 a l2 cache.
To je dan kterou platime za expresivnost jazyku.
Zde bych si dovolil nesouhlasit.
Právě expresivnost jazyka nám, minimálně teoreticky, dovoluje agresivně optimalizovat. Tudíž se docela dobře na tu úroveň cache můžeme dostat.
Příklad: mám kolekci objektů, u které si kompilátor z typové signatury odvodí, že jsou imutable, tak mohu nejenom neřešit zámky, ale klidně můžu tu kolekci umístit na stacku, nebo ji inlinovat/rozkopírovat. Mě, jako uživatele to nezajímá, a kompilátor má volné ruce.
V praxi se to i dost ukazuje: http://funkcionalne.cz/2015/04/bez-typu-se-obejdeme-ale/
V kontextu tohoto vlákna: kompilátor píšou parta lidí, kteří se soustředí na různé tyto optimalizace. Obvykle můžeme očekávat špičky ve svém oboru. V případě, kdy to samé dělám testy, tak to píšeš zas a znova, a optimalizovat musíš opět zas a znova ty sám. Snad je z toho vidět ta motivace po typech.
iterátor neumožňuje náhodný přístup, z toho plyne ten problém, o kterém psal jirsák. Typy prvků vám nepomohou.
To je ale dost nizkourovnova zalezitost. Myslim, ze v jazycich vyssi urovne s tim stejne moc neudelame, protoze jsme tak daleko abstrahovali od HW, ze nemuzeme optimalizovat na urovni l1 a l2 cache.
To je dan kterou platime za expresivnost jazyku.
Jmeno toho vlakna naznacuje, ze jde o srovnani toho co jde a nejde udelat typy vs unit testy.
Takze nevim jak BoneFlute, ale za me:
Az uvidim unit test ktery pri behu na Xeonu zahlasi ze dana funkce selze na 486 zacnu resit jak je mozne, ze tohle nedokaze typovy system.
O závislostních typechDoporučil bych knihu "Seven more languages in seven weeks", tam stručně popisují Idris, který se přesně na tohle hodí.Díky! Mrknu na to.
Můžeš mě trochu navnadit, o čem všem se tam píše?Je to úvod do toho jazyka se zaměřením na právě závislostní typy, protože znalost toho, na čem staví (FP à la Haskell), se předpokládá.
Doporučil bych knihu "Seven more languages in seven weeks", tam stručně popisují Idris, který se přesně na tohle hodí.Díky! Mrknu na to.
Že limit nemá být záporný, a že start musí být menší jak str nebudu psát do dokumentace ani do testů. Napíšu to pomocí závislostních typů, protože je to výhodnější.
A jak by si tu funkci substr těmi závislostními typy napsal?
function substr(str: String, start: Int 0 (strlen str), len: Int 0 (strlen str)) : String 0 (strlen str)Ale to neznamená že to nejde.
dosud jsi neukázal, že to jde ani u jednoduchých funkcí pro sčítání a odčítání.
To ze se nekdo rozhodl, ze nebude formalizovat veskere pozadavky na funkci, a ze neco jen popise v dokumentaci, neni proto, ze by to neslo, ale proto ze se mu nechtelo.A když se to spojí, tak máme ten hypotetický jazyk, který by dokázal nahradit testy v případech užití, které byly uváděny.Uváděn byl příklad dvou funkcí pro sumaci. Nějak ho stále přehlížíte.Obávám se, že to není nijak podstatné.Ale já nepíšu o signatuře, píšu o API. A součástí API té funkce substr je, že někde v dokumentaci, např. v manuálové stránce, je napsáno, co ta funkce má dělat, a v lepším případě i jaké jsou možné parametry a co to bude dělat, pokud budou parametry mimo rozsah. V horším případě tam zejména ty chybové stavy moc dobře popsané nebudou , a pak nastává ten případ, o kterém jsem také psal, že se mohou lišit názory na to, jaké je vlastně přesné API té funkce.
Byly časy, kdy API funkce (říkejme tomu spíše signatura) vypadala nějak takto:
function substr(String str, Int start, Int len) : String
A v praxi jsme pak museli ošetřit testem, co se stane, když zavoláme substr("abc", 6, -2). Někde uvnitř té funkce bylo definováno, že to má vyhodit výjimku, prázdný řetězec, nebo něco takového. Podstatné ale je, že signatura funkce o této nesmyslnosti nic nevěděla.
Dnes už máme typy na takové úrovni, že dokážeme zohlednit, že substr("abc", 6, -2) nepůjde vůbec přeložit. A myslím, že nikoho nijak zvlášť nezajímá, že kdysi dávno se tvrdilo, že ošetření těchto nesmyslných vstupů je otázka implementace, a nikoliv API/Signatury.
Takže pokud trváš na tom, že API/Signatura a implemnetace/chování jsou dva oddělené světy, tak já ti tvůj názor přeji, ale v takovém případě nám nejde o stejnou věc.
BoneFluteovi se chce.
Ano, ty jsou mocné, docela rád bych tu viděl nějaké příklady problémů, které záv. typy řeší.jak by tedy vypadaly ty funkce v Elmu?To, že změním chování nějaké funkce, ale vnější signatura (vstup a výstup) zůstane stejná, to by zase mohli podchytit závislostní typy.
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.