Příspěvky

1066

Vývoj / Re:Haskell, ExistentialQuantification, forall

« kdy: 04. 04. 2021, 23:59:06 »

Zkusme pro začátek nastřelit, k čemu ZT mohou být dobré. Tím pro blbečky stylem, který jsem ukázal výše.

To jde sfouknout rychle, prostě přinášejí vyšší bezpečnost v době překladu. Umožňují podchytit některé případy, které by se jinak projevily chybou za běhu, třeba “index out of bounds” nebo dělení nulou. Rozdíl mezi jazyky majícími záv. typy bývá v tom, jestli ty důkazy musí psát vývojář, nebo jestli je překladač musí odvodit sám (to druhé bývá z principu věci nedokonalé). IMHO je pro začátečníka dobré zabývat se nejprve tím prvním případem, tj. naučit se psát vše explicitně.

1067

Vývoj / Re:Haskell, ExistentialQuantification, forall

« kdy: 04. 04. 2021, 23:01:14 »

To beru! Rvi to do mě! (Posledně jsem to moc nedal, tak třeba teď mi to půjde líp.)

To není v principu problém, ale vyžaduje to netriviální základy, přinejmenším dobrou znalost Curryho-Howardovy korespondence (což ale není nijak složité). Navíc ta hlavní magie okolo záv. typů ("aha moment") přijde až poté, co se člověk prohrabe mnoha zdánlivě nudnými a neužitečnými příklady. Ale jestli tě to neodrazuje, tak to můžeme zkusit, akorát moc nevím, kde začít, aby to na tebe nebylo ze začátku moc náročné, nebo naopak směšně triviální.

1068

Vývoj / Re:Haskell, ExistentialQuantification, forall

« kdy: 03. 04. 2021, 21:40:58 »

[...]
... takhle jsem myslel to česky.

“Takhle česky” to moc nejde, přinejmenším ne slušně, IMHO je to dost na houby, protože univerzálně kvantifikovaná typová proměnná v antecedentu předpokládá generickou funkci, a těch je v praxi jak šafránu. Možná nějaký kovaný haskellista má nějaký triviální příklad.

Takhle polopatisticky umím vysvětlit možná závislostní typy, ale higher rank ne.

1069

/dev/null / Re:Práce pro české společnosti

« kdy: 03. 04. 2021, 15:04:16 »

V Irsku to je evidentne taky v pohode

V Irsku děti dostanou automaticky občanství, když se narodí občanovi EU, co tam bydlí aspoň 3 roky. Jinak až za pět let. Nicméně nikde v EU není zvláštní výhodou mít občanství země, kde člověk bydlí, když má sám občanství jiné země EU, někdy to je dokonce nevýhoda.
Irsko je zvláštní tím, že jeho občanství zaručuje nárok na neomezený pobyt a práci ve Spojeném království (bez nově zavedených omezení a kvót).

1070

/dev/null / Re:Práce pro české společnosti

« kdy: 02. 04. 2021, 22:25:27 »

Získat občanství není jednoduché, mimo jiné se musíš naučit plynule jazyk a sloužit zkoušku něčeho jako "vlastenectví" 

Záleží na konkrétní zemi, každý stát to má jinak. Třeba v Irsku stačí pár let bydlet. Irské občanství je teď vůbec celkem žádané, jednak někteří Britové ho chtějí kvůli občanství EU a na druhou stranu Irové jsou jediní EUropané, co můžou po Brexitu (resp. po už skončivším pobrexitovém přechodném období) ve Spojeném království pracovat bez povolení, studovat za místní taxu atd.

1071

/dev/null / Re:Práce pro české společnosti

« kdy: 02. 04. 2021, 13:21:45 »

Bohužel je pravda, že manažeři stojí za kulové, ale to je tím, jak se "to" učí, jaké školy je vychovávají.

Chce to studovat v zahraničí.

1072

/dev/null / Re:Práce pro české společnosti

« kdy: 02. 04. 2021, 12:34:14 »

Pas už tam nějakou dobu je, ale potom co nastoupil první lockdown tak úředníci mají prázdniny.

Stejná zkušenost. Když to tak půjde dál, ten pas vyprší před vyzvednutím.

1073

/dev/null / Re:Práce pro české společnosti

« kdy: 01. 04. 2021, 15:59:00 »

Nechápu co se češi tak čepýří když někdo řekne východní evropa, vždyť je to pravda...

Mentalitou určitě.

1074

Vývoj / Re:CSP v embedded světě

« kdy: 01. 04. 2021, 11:31:08 »

Jestli si chceš trochu pohrát s prapůvodní teorií typů, tady je zdá se implementace: https://simpl-eval.netlify.app
Příslušný článek je nějakým nedopatřením taky volně ke stažení: https://www.semanticscholar.org/paper/A-Formulation-of-the-Simple-Theory-of-Types-Church/28bf123690205ae5bbd9f8c84b1330025e8476e4
Tohle není přímo intuicionistická logika, ale "simple type theory, also known as higher-order logic".

Díky za zdroje. Ještě jsem ani nezpracoval ta původní.

Každopádně můj fokus je momentálně na tomto: https://amulet.works/

Slibuje to hodně. A já si od toho slibuju, kromě praktického užití (mám projekt v lue, lua mi vyhovuje svou minimaličností a rychlostí, nevyhovuje mi tím, že nemá typy), taky to, že si v praxi ošahám, k čemu jsou konkrétní koncepty. Například tomu forall jsem ještě furt nepřišel nachuť (ne že bych se tak moc snažil).

Když by si se nudil a napadl tě nějaký pěkný demonstrativní příkládek, zlobit se nebudu.

Tak z ML světa bych vzal Rust, díky jeho praktičnosti a k tématu - hodí se na embedded.

Rust má forall?

1075

Hardware / Re:Lenovo Thinkpad vs Dell Latitude pro vyvojare

« kdy: 01. 04. 2021, 11:13:33 »

Jednoduché pravidlo u Intelu je, že procesory značené U jsou úsporné, H nebo starší HQ jsou naopak optimalizované pro výkon. U TP se dívejte po řadách, protože Lenovo začalo dávat označené Thinkpad na ledacos. U Dellu obdobně. Je velký rozdíl mezi řadami 3xxx, 5xxx a 7xxx. Chcete Dell Latitude 7xxx nebo Lenovo X, T, P. Kdyžtak můžete být konkrétnější a přiblížit plénu kandidáty.

Neboli U znamená Unusable

Proc by U melo byt unusable, ty delas jakovyvojar nejake pulhodinove vypocetni tasky? Pro dev by melo stacit mit dobrou core boost frekvenci.

On jen blábolí.

1076

Vývoj / Re:Haskell, ExistentialQuantification, forall

« kdy: 31. 03. 2021, 21:37:32 »

Umí to víc?

Umí to "higher-rank types". Když se forall explicitně neuvede, je jeho působnost v případě funkcí přes celý typ. Kvantifikátory jdou vytáhnout jen z konsekventu, takže v antecedentu je nutné uvést forall explicitně.

Když by si to řekl česky (A tím nemám na mysli konsekvent a antecedent.)

Jde o to, že ∀x.(A→B) je něco jiného, než (∀x.A)→B, to první je běžný rozsah platnosti kvantifikátoru u generických typů (nejen v Haskellu), kdežto to druhé je divná haskellí věc (rank 2). Ten kvantifikátor nejde vytáhnout ven bez změny významu.

1077

Hardware / Re:Lenovo Thinkpad vs Dell Latitude pro vývojáře

« kdy: 31. 03. 2021, 20:21:24 »

A zase z jineho soudku, kdybych zvazoval XPS s 11. generaci intel, tak si rikam, ze bych mozna raedji koupil Macbook AIR M1 a dal si tam treba Windowzy, protoze ta M1 ma jeste lepsi vykon.

O trošku lepší výkon. Pozor na to, že M1 neumí 32-bitové instrukce.

1078

Vývoj / Re:Zajímá se tady někdo o blockchain a programování aplikací na něm?

« kdy: 31. 03. 2021, 19:13:23 »

Jen zlehka, zajímá mě technická stránka věci.

1079

Vývoj / Re:Haskell, ExistentialQuantification, forall

« kdy: 31. 03. 2021, 18:43:55 »

Umí to víc?

Umí to "higher-rank types". Když se forall explicitně neuvede, je jeho působnost v případě funkcí přes celý typ. Kvantifikátory jdou vytáhnout jen z konsekventu, takže v antecedentu je nutné uvést forall explicitně.

1080

Vývoj / Re:Haskell, ExistentialQuantification, forall

« kdy: 31. 03. 2021, 17:55:59 »

toto naivní v Haskellu neprojde:

Kód: [Vybrat]

format :: [Show] -> String
...
... format ["text", 42, True]

To neprojde, protože Show má druh *→* a pokud se uvede typová proměnná, musela by mít stejnou hodnotu pro všechny prvky kolekce.