CSP v embedded světě

[BoneFlute]

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.

forall patří do skupiny kvantifikačních typů. Takové to každý, žádný. Potuď mi teorie ok. Ale zatím mi nedochází, k čemu v praxi to může být dobré? Myslím tím nějaký vulgární praktický příklad.

Příklad s monádama: Monáda Maybe je dobrá k tomu, když chceš vrátit hodnotu nebo chybu. Užitek: Maybe je generická. Tudíž nemusíš řešit NullObject pro každý svůj vlastní typ. Díky tomu, že je to generické, můžeš udělat takovou tu věc (neznám názvosloví), kdy řadíš Maybe za sebou a nemusíš řešit rozbalení, zabalení. Máš to otypováné, tudíž se ti nemůže stát, že ti uteče nějaká větev programu, protože ty nemůžeš hned pracovat s tou hodnotou, ale musíš ji nejdřív vybalit... A podle signatury hned poznám, zda mi to vrací číslo, či číslo nebo chybu. A tak.

Jiný příklad s třídama. Třídy nedefinují typ, ale povinnost mít správnou funkci, funkce. A tím mi to rozvazuje ruce, že já nemusím řešit co je to za objekt, jeho strukturu, nedejbože jméno, ale má implementované ty funkce? To mi stačí, stejně víc nepotřebuju.

A prostě by se mi líbil nějaký příkládek pro forall. Abych věděl, že "jo ahaá, takže já si tenhle kousek kódu můžu zjednodušit na..."

[Reklama]

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

forall patří do skupiny kvantifikačních typů. Takové to každý, žádný. Potuď mi teorie ok. Ale zatím mi nedochází, k čemu v praxi to může být dobré? Myslím tím nějaký vulgární praktický příklad.

Příklad s monádama: Monáda Maybe je dobrá k tomu, když chceš vrátit hodnotu nebo chybu. Užitek: Maybe je generická. Tudíž nemusíš řešit NullObject pro každý svůj vlastní typ. Díky tomu, že je to generické, můžeš udělat takovou tu věc (neznám názvosloví), kdy řadíš Maybe za sebou a nemusíš řešit rozbalení, zabalení. Máš to otypováné, tudíž se ti nemůže stát, že ti uteče nějaká větev programu, protože ty nemůžeš hned pracovat s tou hodnotou, ale musíš ji nejdřív vybalit... A podle signatury hned poznám, zda mi to vrací číslo, či číslo nebo chybu. A tak.

Jiný příklad s třídama. Třídy nedefinují typ, ale povinnost mít správnou funkci, funkce. A tím mi to rozvazuje ruce, že já nemusím řešit co je to za objekt, jeho strukturu, nedejbože jméno, ale má implementované ty funkce? To mi stačí, stejně víc nepotřebuju.

A prostě by se mi líbil nějaký příkládek pro forall. Abych věděl, že "jo ahaá, takže já si tenhle kousek kódu můžu zjednodušit na..."

Haskell má několik rozšíření, přičemž v každém znamená forall něco trochu jiného. IMHO nejpraktičtější je jeho použití v existenčních typech, například:

Kód: [Vybrat]

data Explosive = forall x. Exploder x => Expl xTímto způsobem se dá zbavit explicitního typového parametru, takže pak můžu mít seznam typu [Explosive], třeba [Expl Landmine, Expl Torpedo, Expl Turkey].

[BoneFlute]

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.

forall patří do skupiny kvantifikačních typů. Takové to každý, žádný. Potuď mi teorie ok. Ale zatím mi nedochází, k čemu v praxi to může být dobré? Myslím tím nějaký vulgární praktický příklad.

Příklad s monádama: Monáda Maybe je dobrá k tomu, když chceš vrátit hodnotu nebo chybu. Užitek: Maybe je generická. Tudíž nemusíš řešit NullObject pro každý svůj vlastní typ. Díky tomu, že je to generické, můžeš udělat takovou tu věc (neznám názvosloví), kdy řadíš Maybe za sebou a nemusíš řešit rozbalení, zabalení. Máš to otypováné, tudíž se ti nemůže stát, že ti uteče nějaká větev programu, protože ty nemůžeš hned pracovat s tou hodnotou, ale musíš ji nejdřív vybalit... A podle signatury hned poznám, zda mi to vrací číslo, či číslo nebo chybu. A tak.

Jiný příklad s třídama. Třídy nedefinují typ, ale povinnost mít správnou funkci, funkce. A tím mi to rozvazuje ruce, že já nemusím řešit co je to za objekt, jeho strukturu, nedejbože jméno, ale má implementované ty funkce? To mi stačí, stejně víc nepotřebuju.

A prostě by se mi líbil nějaký příkládek pro forall. Abych věděl, že "jo ahaá, takže já si tenhle kousek kódu můžu zjednodušit na..."

Haskell má několik rozšíření, přičemž v každém znamená forall něco trochu jiného. IMHO nejpraktičtější je jeho použití v existenčních typech, například:

Kód: [Vybrat]

data Explosive = forall x. Exploder x => Expl xTímto způsobem se dá zbavit explicitního typového parametru, takže pak můžu mít seznam typu [Explosive], třeba [Expl Landmine, Expl Torpedo, Expl Turkey].

Co značí to Exploder?

Takže analogicky:

Kód: [Vybrat]

data Err = forall x. Maybe x => Just x
apply :: [Err] -> String
apply xs = ...
apply [Just "text", Just 42, Just True]
?

Přidám otázku: Dokážeš popsat tu ideu existenčních typů?

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

forall patří do skupiny kvantifikačních typů. Takové to každý, žádný. Potuď mi teorie ok. Ale zatím mi nedochází, k čemu v praxi to může být dobré? Myslím tím nějaký vulgární praktický příklad.

Příklad s monádama: Monáda Maybe je dobrá k tomu, když chceš vrátit hodnotu nebo chybu. Užitek: Maybe je generická. Tudíž nemusíš řešit NullObject pro každý svůj vlastní typ. Díky tomu, že je to generické, můžeš udělat takovou tu věc (neznám názvosloví), kdy řadíš Maybe za sebou a nemusíš řešit rozbalení, zabalení. Máš to otypováné, tudíž se ti nemůže stát, že ti uteče nějaká větev programu, protože ty nemůžeš hned pracovat s tou hodnotou, ale musíš ji nejdřív vybalit... A podle signatury hned poznám, zda mi to vrací číslo, či číslo nebo chybu. A tak.

Jiný příklad s třídama. Třídy nedefinují typ, ale povinnost mít správnou funkci, funkce. A tím mi to rozvazuje ruce, že já nemusím řešit co je to za objekt, jeho strukturu, nedejbože jméno, ale má implementované ty funkce? To mi stačí, stejně víc nepotřebuju.

A prostě by se mi líbil nějaký příkládek pro forall. Abych věděl, že "jo ahaá, takže já si tenhle kousek kódu můžu zjednodušit na..."

Haskell má několik rozšíření, přičemž v každém znamená forall něco trochu jiného. IMHO nejpraktičtější je jeho použití v existenčních typech, například:

Kód: [Vybrat]

data Explosive = forall x. Exploder x => Expl xTímto způsobem se dá zbavit explicitního typového parametru, takže pak můžu mít seznam typu [Explosive], třeba [Expl Landmine, Expl Torpedo, Expl Turkey].

Co značí to Exploder?

Takže analogicky:

Kód: [Vybrat]

data Err = forall x. Maybe x => Just x
apply :: [Err] -> String
apply xs = ...
apply [Just "text", Just 42, Just True]
?

Přidám otázku: Dokážeš popsat tu ideu existenčních typů?

Exploder je nějaká třída, třeba s funkcemi explode a defuse. Ve svém příkladu akorát dosaď za Maybe nějakou třídu (a Just bych přejmenoval na nějaký unikátní konstruktor hodnot), pak to bude přesně ono.

Když máš v definici typu na pravé straně proměnnou, musí se vyskytovat i na levé straně (tím se deklaruje). Myšlenka ex. typů je, že se typová proměnná vyskytuje pouze napravo. Proto se někdy operátoru forall říká "type hider". Není třeba v tom hledat nic složitého, je to jednoduchý koncept, jen asi neintuitivně nazvaný.

[okalousek]

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.

[Reklama]

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

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?