Jak validovat DTO v dynamicky typovaném jazyce?

[Wavelet]

A což o to. S tím nemám problém. Určitě je lepší dynamický jazyk, než žádný.

http://bracha.org/pluggable-types.pdf

- Type Systems are subtle and hard
- Relying on them is dangerous

 

Hele, jak dlouho jsme se tu přetahovali o tom, že kategorie silný/slabý typy je zbytná. Teď se tu budeme přetahovat o tom, že static/dynamic typy znamená hlavně compiletime/runtime? Asi jsem unaven. Tím spíše, že je to co půl roku znova, a nic z toho.

Jediný, kdo se o něčem neustále hádá jsi ty. Nevšiml jsem si, že by tu někdo kromě tebe psal hodnotící soudy o  dynamickém/statickém/silném/slabém typování. Jen se vypíchly nějaké výhody a nevýhody a případně přidal odkaz.
Je spousta lidí co jsou schopni psát v Clojure i Scala nebo Python, Haskell, Rust a nedělají z toho takové drama jako ty.
Teď to pár let bude holt Rust. Já se o Rust zajímal od doby vzniku, koment z roku 2016, ale už dřív jsem se tu po něm pídil v diskuzích: https://www.root.cz/clanky/programovaci-jazyk-rust-nahrada-c-nebo-slepa-cesta/nazory/vlakno/7/. Ale zdá se mi, že kolem něj roste skupina lidí, co budou zase slepě tlačit Rust všude, jeho typový systém je to nejlepší na světě... ehhh to už tu bylo s C++ , Java a atd. Ano, škoda ztrácet čas diskuzí.

[Reklama]

[Idris]

Teď to pár let bude holt Rust. […] Ale zdá se mi, že kolem něj roste skupina lidí, co budou zase slepě tlačit Rust všude, jeho typový systém je to nejlepší na světě... ehhh to už tu bylo s C++ , Java a atd.

Tady na fóru možná, jinak je rustí komunita celkem přátelská, když člověk nezmiňuje některé červené hadry

[BoneFlute]

A což o to. S tím nemám problém. Určitě je lepší dynamický jazyk, než žádný.

http://bracha.org/pluggable-types.pdf

- Type Systems are subtle and hard
- Relying on them is dangerous

 

Hele, jak dlouho jsme se tu přetahovali o tom, že kategorie silný/slabý typy je zbytná. Teď se tu budeme přetahovat o tom, že static/dynamic typy znamená hlavně compiletime/runtime? Asi jsem unaven. Tím spíše, že je to co půl roku znova, a nic z toho.

Jediný, kdo se o něčem neustále hádá jsi ty. Nevšiml jsem si, že by tu někdo kromě tebe psal hodnotící soudy o  dynamickém/statickém/silném/slabém typování. Jen se vypíchly nějaké výhody a nevýhody a případně přidal odkaz.
Je spousta lidí co jsou schopni psát v Clojure i Scala nebo Python, Haskell, Rust a nedělají z toho takové drama jako ty.
Teď to pár let bude holt Rust. Já se o Rust zajímal od doby vzniku, koment z roku 2016, ale už dřív jsem se tu po něm pídil v diskuzích: https://www.root.cz/clanky/programovaci-jazyk-rust-nahrada-c-nebo-slepa-cesta/nazory/vlakno/7/. Ale zdá se mi, že kolem něj roste skupina lidí, co budou zase slepě tlačit Rust všude, jeho typový systém je to nejlepší na světě... ehhh to už tu bylo s C++ , Java a atd. Ano, škoda ztrácet čas diskuzí.

Musíš mi odpustit mou zvědavost. Prostě tu zazněla absurdní tvrzení, že silné/slabé typování je podstatnější jak statické/dynamické. A neodolal jsem, abych nezačal zjišťovat, zda mi něco neuniklo. Mohu tě upokojit, že jsem svá data dostal, takže dám zase chvilku pokoj.

[Wavelet]

@BoneFlute
Tak většinou s čím přicházíš, s tím také odcházíš. Přijdeš všem vysvětlit důležitost typů i těm co o nich vědí víc než ty (Idris). Pak se ptáš na triviality a odcházíš se stejným světonázorem.  V pořádku, svět je dost velký pro nás všechny.

[BoneFlute]

@BoneFlute
Tak většinou s čím přicházíš, s tím také odcházíš.

Je to tak. Je to škoda, ale co nadělám. Někdy má člověk smůlu.

[Reklama]

[Idris]

@BoneFlute
Tak většinou s čím přicházíš, s tím také odcházíš.

Je to tak. Je to škoda, ale co nadělám. Někdy má člověk smůlu.

Ta diskuse o záv. typech zhruba před rokem byla náhodou celkem dobrá, a teď by byla ještě lepší, když mají účastníci o rok více zkušeností se sofistikovanými typovými systémy. Za sebe můžu říct, že před rokem jsem téměř neznal OCaml nebo (moderní) Adu (ta zajímavě kombinuje statické a dynamické typování), kde jsou taky lahůdky.

[BoneFlute]

... (moderní) Adu (ta zajímavě kombinuje statické a dynamické typování), kde jsou taky lahůdky.

Chceš to rozvést?

[Idris]

před rokem jsem téměř neznal ... (moderní) Adu (ta zajímavě kombinuje statické a dynamické typování), kde jsou taky lahůdky.

Chceš to rozvést?

Ani ne, furt ji moc neznám (tu nejnovější verzi), takže bych nerad psal blbosti. Nicméně jde o to, že Ada je poměrně přísně staticky typovaná, ale má (verze 2012, podle definice) závislostní typy, které jsou ale implementované pomocí tzv. predikátů, z nichž některé můžou být dynamické. Takže jestli jsem to dobře pochopil, částečně se chová jako třeba Julia s jejím existenciálním typovým kvantifikátorem. Právě čtu Ada 2012 rationale, ale je to bichle a mám i jiné věci, takže mi to jde jak psovi pastva.

[Wavelet]

před rokem jsem téměř neznal ... (moderní) Adu (ta zajímavě kombinuje statické a dynamické typování), kde jsou taky lahůdky.

Chceš to rozvést?

Ani ne, furt ji moc neznám (tu nejnovější verzi), takže bych nerad psal blbosti. Nicméně jde o to, že Ada je poměrně přísně staticky typovaná, ale má (verze 2012, podle definice) závislostní typy, které jsou ale implementované pomocí tzv. predikátů, z nichž některé můžou být dynamické. Takže jestli jsem to dobře pochopil, částečně se chová jako třeba Julia s jejím existenciálním typovým kvantifikátorem. Právě čtu Ada 2012 rationale, ale je to bichle a mám i jiné věci, takže mi to jde jak psovi pastva.

Nejsem tedy znalec typových systémů, ale Ada jsem drtil 10let zpátky tzn. že 2012 jsem ještě chytil. Co jsem tenkrát pochopil, tak velká energie se dávala do té podmnožiny která se jmenuje SPARK. Problém Ady je stejný jako byl u Fortranu, tzn. málo dostupných knihoven. Ale jazyk je to pěkný. Zde na rootu někdo občas přispěl komentářem, protože v něm měli produkční software. A to jsem jim záviděl

[Idris]

Nejsem tedy znalec typových systémů, ale Ada jsem drtil 10let zpátky tzn. že 2012 jsem ještě chytil. Co jsem tenkrát pochopil, tak velká energie se dávala do té podmnožiny která se jmenuje SPARK.

SPARK znám ještě méně, ale vypadá rozhodně sympaticky, má formální verifikaci a od verze 2014 kontrakty. Musím se na něj podívat podrobněji, zatím mě míjel.

[BoneFlute]

před rokem jsem téměř neznal ... (moderní) Adu (ta zajímavě kombinuje statické a dynamické typování), kde jsou taky lahůdky.

Chceš to rozvést?

Ani ne, furt ji moc neznám (tu nejnovější verzi), takže bych nerad psal blbosti. Nicméně jde o to, že Ada je poměrně přísně staticky typovaná, ale má (verze 2012, podle definice) závislostní typy, které jsou ale implementované pomocí tzv. predikátů, z nichž některé můžou být dynamické. Takže jestli jsem to dobře pochopil, částečně se chová jako třeba Julia s jejím existenciálním typovým kvantifikátorem. Právě čtu Ada 2012 rationale, ale je to bichle a mám i jiné věci, takže mi to jde jak psovi pastva.

Moc rád bych pochopil co si mám představit pod pojmem “kombinovat dynamické se statickým”. V mé hlavě ty dva pojmy defakto dokonvergovali do významu statické = compile time + přinutit vývojáře ohlídat, dynamické = runtime + nemusíš nic. (Tedy dva protichůdné póly.)

Je docela dost možné, ze si pod tím opět představuju něco jiného než většinová společnost.

Příklad:

Kód: [Vybrat]

fn inc(a: Number): Number {…} může být statický i dynamický.
Toto

Kód: [Vybrat]

fn concat(a, b) {…} taky. Nebo toto :

Kód: [Vybrat]

{
xs[] = module.loadFrom(name)
}
Nic z toho mi nepřijde jenom dynamické nebo jenom statické. Možná špatný příklady, možná omezený rozhled. Pravděpodobně špatné pojmenování věci?
Byl by si schopen uvést nějaký demonstrativní příklad? Co si mám představit co vidíš, když mluvíš o dynamickém typovaní? A jak jde statické a dynamické kombinovat?

[Ink]

Nic z toho mi nepřijde jenom dynamické nebo jenom statické. Možná špatný příklady, možná omezený rozhled. Pravděpodobně špatné pojmenování věci?
Byl by si schopen uvést nějaký demonstrativní příklad? Co si mám představit co vidíš, když mluvíš o dynamickém typovaní? A jak jde statické a dynamické kombinovat?

Dynamic_Predicate prisne vzato neresi typ v tom smyslu, jak ho zname v beznych jazycich, ale pouze constraints (neco jako kontrakt?) Aspon tak tomu rozumim ja:

http://www.ada-auth.org/standards/12rat/html/Rat12-2-5.html

Nic, co by neresil treba assert v konstruktoru, nebo?

[Idris]

Moc rád bych pochopil co si mám představit pod pojmem “kombinovat dynamické se statickým”.

Ada:

Kód: [Vybrat]

subtype Even is Integer with Dynamic_Predicate => Even mod 2 = 0;
Staticky se kontroluje přiřazení celého čísla, ale predikát je dynamický. To je rozdíl oproti jazykům jako Agda, kde můžu mít typ EvenNat, který je kompletně kontrolovaný v době překladu.

Staticky typované jazyky se dělí na dva základní typy: s běhovými chybami a bez (taky se říká bez výjimek, prostě nedojde k přerušení bloku kódu kvůli chybě). Ty druhé (Agda, SPARK…) vyžadují aspoň GADT nebo nějaký podobný mechanismus a predikáty jako sudost nebo nenulovost se vyjadřují staticky.

[Idris]

Dynamic_Predicate prisne vzato neresi typ v tom smyslu, jak ho zname v beznych jazycich, ale pouze constraints (neco jako kontrakt?)

Přesně, kontrakt. Ale v podstatě to je jen implementační detail, protože to staticky (přes typy) udělat jde a zápis typu je v podstatě stejný. Klidně by někdo mohl transpilovat takovéto predikáty z Ady do řekneme Agdy, kde už bude příslušná kontrola v době překladu.

Ostatně i SPARK má staticky ověřované kontrakty, a to je “skoro Ada”.

[BoneFlute]

Moc rád bych pochopil co si mám představit pod pojmem “kombinovat dynamické se statickým”.

Ada:

Kód: [Vybrat]

subtype Even is Integer with Dynamic_Predicate => Even mod 2 = 0;
Staticky se kontroluje přiřazení celého čísla, ale predikát je dynamický. To je rozdíl oproti jazykům jako Agda, kde můžu mít typ EvenNat, který je kompletně kontrolovaný v době překladu.

Staticky typované jazyky se dělí na dva základní typy: s běhovými chybami a bez (taky se říká bez výjimek, prostě nedojde k přerušení bloku kódu kvůli chybě). Ty druhé (Agda, SPARK…) vyžadují aspoň GADT nebo nějaký podobný mechanismus a predikáty jako sudost nebo nenulovost se vyjadřují staticky.

A to dynamické znamená, že mi:

Kód: [Vybrat]

function test (x: Even) return Even
begin
   return x + x;
end

test(13)
sice přeloží, ale při běhu to vyhodí výjimku při pokusu zavolat test(13), tak?