Jak validovat DTO v dynamicky typovaném jazyce?

Idris

  • *****
  • 1 910
    • Zobrazit profil
    • E-mail
Re:Jak validovat DTO v dynamicky typovaném jazyce?
« Odpověď #120 kdy: 27. 01. 2022, 13:43:15 »
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?
Jo. Aby se to nepřeložilo, chce to mocnější typový systém.


Idris

  • *****
  • 1 910
    • Zobrazit profil
    • E-mail
Re:Jak validovat DTO v dynamicky typovaném jazyce?
« Odpověď #121 kdy: 28. 01. 2022, 12:06:49 »
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?
Doporučuji mrknout, jak se kontrakty kontrolují v době překladu ve SPARKu (GNATprove), zejména na hinty přímo v kódu (Pragma Assert — nesouvisí s asercí v době běhu). IMHO je tento způsob statické verifikace intuitivnější než holá int. logika à la Agda.

Idris

  • *****
  • 1 910
    • Zobrazit profil
    • E-mail
Re:Jak validovat DTO v dynamicky typovaném jazyce?
« Odpověď #122 kdy: 20. 02. 2022, 14:18:16 »
- místo řešení rozhraní a tříd jako typových omezení, se používá forall, který je sice matematicky čistější, ale programátorsky neintuitivní
Teď jsem zrovna na tento “problém” narazil při psaní kódu. Tak jen dodám, že v jazyce s GADT se ten neintuitivní forall v existenčním významu používat nemusí, v GADT to jde stejně bez nepříjemných syntaktických konstrukcí.