CSP v embedded světě

[Idris]

Clang si (oproti očekávání) s Picem celkem rozumí, takže kdo nechce stackful korutiny, stejně elegantně může mít kanály takto:

Kód: [Vybrat]

auto ch = channel_create();
dispatch_async(^{
  sleep_ms(1000);
  channel_send(ch, ...);
});
auto x = channel_receive(ch);

Vyjde to skoro nastejno, ale bez zbytečného zásobníku.

[Reklama]

[Mirek Prýmek]

Napadá mě jedině to, že budeš mít asi pravdu. Každopádně díky za příklad.

Mě teda napadá

1. že ji tak NEnazval Pokud je teda řeč o "Monde cruel"

2. že jedno album od Plastiků se jmenuje Vožralej jak slíva a nijak z toho neplyne, že "vožralej" je spisovně česky správně a kdybych to napsal do zdrojáku, neznělo by to jako špatná čeština

Každopádně je úsměvný, jak se tu schizofreně až sprostě častujete a zároveň se věcně bavíte o technice :-)

Nevím, jak to má Idris, ale z mé strany je to popichování s úsměvem, mám z toho prču, není v tom sebemenší zlej úmysl

[Mirek Prýmek]

Ale je fajn, že si aspoň nepleteš vokativ a použití jmenné fráze v názvu periodika jako MP

Ale pane kolego, zase argumentační klam?! Nikdo si tady přece tohle nepletl

[Idris]

Nikdo si tady přece tohle nepletl

Neříkej si “nikdo”, na to má copyright Terence Hill od raných 70. let (podle tebe “ranných”)

A teď k tématu?

[Idris]

BTW co ta intuicionistická logika, nějaký pokrok? Jsem si teď vzpomněl

[Reklama]

[Mirek Prýmek]

Neříkej si “nikdo”

Úroveň vtipů silně upadá, tohle je tak čtvrtá třída ZŠ

[BoneFlute]

BTW co ta intuicionistická logika, nějaký pokrok? Jsem si teď vzpomněl

Zatím u ledu. V knihovně to neměli a pak jsem byl převálcován prioritami :-)

[Idris]

BTW co ta intuicionistická logika, nějaký pokrok? Jsem si teď vzpomněl

Zatím u ledu. V knihovně to neměli a pak jsem byl převálcován prioritami :-)

To znám BTW ta kniha od Sitnikovského je zdá se ke stažení zdarma (zahlédl jsem ji někde na Research gate), kdyby tě to zajímalo.

[BoneFlute]

BTW co ta intuicionistická logika, nějaký pokrok? Jsem si teď vzpomněl

Zatím u ledu. V knihovně to neměli a pak jsem byl převálcován prioritami :-)

To znám BTW ta kniha od Sitnikovského je zdá se ke stažení zdarma (zahlédl jsem ji někde na Research gate), kdyby tě to zajímalo.

Tenhle https://bor0.wordpress.com/ ?

[Idris]

BTW co ta intuicionistická logika, nějaký pokrok? Jsem si teď vzpomněl

Zatím u ledu. V knihovně to neměli a pak jsem byl převálcován prioritami :-)

To znám BTW ta kniha od Sitnikovského je zdá se ke stažení zdarma (zahlédl jsem ji někde na Research gate), kdyby tě to zajímalo.

Tenhle https://bor0.wordpress.com/ ?

Ano. Ta kniha o "dependent types" byla na Leanpubu za nějaké drobné, ale teď se dá legálně stáhnout. Je dost stručná, ale základní věci tam vysvětluje celkem pěkně.

[BoneFlute]

BTW co ta intuicionistická logika, nějaký pokrok? Jsem si teď vzpomněl

Zatím u ledu. V knihovně to neměli a pak jsem byl převálcován prioritami :-)

To znám BTW ta kniha od Sitnikovského je zdá se ke stažení zdarma (zahlédl jsem ji někde na Research gate), kdyby tě to zajímalo.

Tenhle https://bor0.wordpress.com/ ?

Ano. Ta kniha o "dependent types" byla na Leanpubu za nějaké drobné, ale teď se dá legálně stáhnout. Je dost stručná, ale základní věci tam vysvětluje celkem pěkně.

https://github.com/bor0/gidti

Jsi pěknej prevít ti povím. Pochop. Nemám čas, jasný? Musím taky někdy spát.

[Idris]

BTW co ta intuicionistická logika, nějaký pokrok? Jsem si teď vzpomněl

Zatím u ledu. V knihovně to neměli a pak jsem byl převálcován prioritami :-)

To znám BTW ta kniha od Sitnikovského je zdá se ke stažení zdarma (zahlédl jsem ji někde na Research gate), kdyby tě to zajímalo.

Tenhle https://bor0.wordpress.com/ ?

Ano. Ta kniha o "dependent types" byla na Leanpubu za nějaké drobné, ale teď se dá legálně stáhnout. Je dost stručná, ale základní věci tam vysvětluje celkem pěkně.

https://github.com/bor0/gidti

Jsi pěknej prevít ti povím. Pochop. Nemám čas, jasný? Musím taky někdy spát.

Kdo ti brání?

[Idris]

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".

[BoneFlute]

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.

[Idris]

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

To vypadá celkem zajímavě.

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

Příklad čeho? Určitě není problém, jen to pls upřesni.