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.
Díky, homebrew už mám a macports, fink prozkoumám.Já tu základní, bohatě stačí.
Používate pro terminal tu základní app co je v systému nebo něco "lepšího" z appstoru ?
Mac
Prostým zakoupením přímo na telefonuKde se vzal ten mýtus, že bez iTunes se iPhone nedá používat? Já sice nejsem příznivcem iPhonu, sám ho nepoužívám, i když bych ho mohl nafasovat, ale většina lidi, co znám, používá iTunes jako naprosto autonomní zařízení a o iTunes nepoužívají.
Chces rici, ze na ajFoun dneska dostanes hudbu prostym nakopirovanim
Ještě doplním, že v signaturách typů je typový operátor → zprava asociativní, takže a→b→c znamená, chceme-li být zcela přesní, a→(b→c) a ta curryfikace v podstatě formálně znamená, že ke každé funkci typu a→b→c existuje isomorfní funkce typu a×b→c (ty funkce nejsou formálně stejné, i když v konkrétní implementaci můžou být identické).Ha! Rozumím.funkce s libovolným počtem argumentů je funkce s jedním argumentem kde výsledek je funkce s libovolným počtem argumentů minus jednaTakže ve výsledku funkce s libovolným počtem parametrů, která vrací Monoid, je Monoid.To se mi nezdá. Funkce s libovolným počtem parametrů bude Monoid jen po ruční curryfikaci. Automaticky ne.
a0 -> a1 -> ... an -> t
je jako
a0 -> t' kde t' = (a1 -> ... -> an -> t)
nebo taky
a0 -> (a1 -> ... an -> t)
Jo, teď jsem se už definitivně ztratil jáNo ale přece String 0 ∞ není podtypem String 4 20, tady je ta kontrola ještě přímočará. Možná teda nejspíš nechápu otázku. BTW to Str.sub by mělo mít návratový typ také závislostní podle vstupních parametrů, jinak by byla typová kontrola příliš restriktivní.To Str.sub bude mít svůj návratový typ, a pokud ten není podtypem návratového typu té vnější funkce, překladač zařve.Tak v tom případě to není odpověď na mou otázku :-)
Str.sub vrací String 0 ∞, zatímco fn vrací String 4 20. Takže mi to může vrátit dvouznakový řetězec, a to už je špatně.
A přesto očekávám, že (v případě, když bych tam neměl tu záměrnou chybu) mi to překladač označí za korektní.
Počkej, počkej, mám pocit, že jsme se tu někdo z nás ztratil.
Str.sub má návratový typ String 0 ∞. Takže může vrátit dvouznakový řetězec. Vstupní argumenty jsou 20, což je ok na výstup, takže tento argument změní návratový typ na String 0 20. A dále String, jehož minimální velikost je určena tou kontrolou v if. Což je tedy defakto taky správně, a ta funkce bude pracovat korektně. A já se tedy táži, jak typový systém pozná, že díky podmínce if se z hodnoty String 0 20 stane hodnota typu String 2 20 (respektive String 4 20).
Zdůrazňuji, že já se táži na typový systém, který řeší mou úlohu. Netáži se jak fungují závislostní typy (i když zrovna třeba ony mohou řešit mou úlohu, a pak mě zajímá jak to řeší).
Co je myšleno tím "změnit návratový typ"?
No ale přece String 0 ∞ není podtypem String 4 20, tady je ta kontrola ještě přímočará. Možná teda nejspíš nechápu otázku. BTW to Str.sub by mělo mít návratový typ také závislostní podle vstupních parametrů, jinak by byla typová kontrola příliš restriktivní.To Str.sub bude mít svůj návratový typ, a pokud ten není podtypem návratového typu té vnější funkce, překladač zařve.Tak v tom případě to není odpověď na mou otázku :-)
Str.sub vrací String 0 ∞, zatímco fn vrací String 4 20. Takže mi to může vrátit dvouznakový řetězec, a to už je špatně.
A přesto očekávám, že (v případě, když bych tam neměl tu záměrnou chybu) mi to překladač označí za korektní.
To Str.sub bude mít svůj návratový typ, a pokud ten není podtypem návratového typu té vnější funkce, překladač zařve.Díky.Jako normální typová analýza, akorát typové operátory (konstruktory) berou i hodnoty krom typů. Třeba append na řetězcích by měl typ "String n m -> String k l -> String (n+k) (m+l)", takže v rámci typové kontroly (tj. během překladu, ne až za běhu) se počítá, v tomto případě s přirozenými čísly. Musí se dávat pozor na subsumpci a varianci, třeba String n m je podtypem String k l, pokud n>=k & m<=l.To jsou závislostní typy, verifikace se dělá přes theorem proving (takže překlad programu někdy trvá hodiny). Viz například jazyk Idris.Mohl by si prosím lidsky popsat princip, jak se ta verifikace dělá?
Uniká mi v tvé odpovědi, jak ten systém pozná, že Str.sub s 20 ve větvi else vrátí vždy korektní minimální čtyři znaky. (Tedy v mém případě pozná, že nevrátí, a tudíž nahlásí chybu.)
Jako normální typová analýza, akorát typové operátory (konstruktory) berou i hodnoty krom typů. Třeba append na řetězcích by měl typ "String n m -> String k l -> String (n+k) (m+l)", takže v rámci typové kontroly (tj. během překladu, ne až za běhu) se počítá, v tomto případě s přirozenými čísly. Musí se dávat pozor na subsumpci a varianci, třeba String n m je podtypem String k l, pokud n>=k & m<=l.To jsou závislostní typy, verifikace se dělá přes theorem proving (takže překlad programu někdy trvá hodiny). Viz například jazyk Idris.Mohl by si prosím lidsky popsat princip, jak se ta verifikace dělá?
Ten odkazovaný tech report je zajímavý, i když celkově to na mě působí jako mnoho povyku pro nic, protože takhle se to normálně dělá, jenom to akademicka přikrášlili a nafoukli.Prymku, mas neco na githubu? Udelam ti codereviewhttps://github.com/mprymek/symconfig
Je to typový konstruktor beroucí přirozené číslo, to není pro generika typické. Je to dependent type.Pole je typu typu ω→*→*, i když v tomto případě to je spíš jen nepodstatná náhoda.Tomu pořád nerozumím
Pole je typu typu ω→*→*, i když v tomto případě to je spíš jen nepodstatná náhoda.Ale zase má závislostní typy (typové konstruktory nad hodnotami)Co tím máš namysli? Teď si tohle vůbec nemůžu vybavit.
* nevím ovšem na jakou. Asi za mír [v duši všech, kdo píšou něco konkurentního]Nějakou cenu za civil engineering.
chan taky. Právě channels (a příslušný runtime) jsou dle mého skromného názoru na Go to nejlepší, jinak ten jazyk ničím nevyniká.Zajímavé. Některé typy tam generické jsou a nevybavuju si, že by mi někde jinde chyběly, a to jsem v tom napsal hodně kódu.Jestli myslíš ty zabudované, tak ty jsou iiirc jenom dva - array a map.
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.
