Jak validovat DTO v dynamicky typovaném jazyce?

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

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.

[Reklama]

[Idris]

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]

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