Je ekvivalentne.
Není.
Technicky vzato to ekvivalentní samozřejmě není (specificky tahle řádka uričtě ne), ale smysl kódu je v zásadě stejný. Na začátku se buď vytvoří hodnota daného typu, nebo se vyhodí chyba...
Liší se technické detaily, v Javě například to bude muset mít objekt, nebudeš moct použít infixové operátory a řada dalších technických rozdílů...
Na technické detaily ti zvrací alík.
Liší se hlavně záruky.
V C# můžu tu validaci zapomenout. Skončí mi to výjimkou u assert v
run-time. Zatímco v Idrisu mi to přinutí tu kontrolu udělat
compile-time. To je ta zásadní motivace, proč se všechny ty šaškárny s typama dělají.
Idris mě
přinutí tu kontrolu udělat.
C#, Java, Python mi tu kontrolu udělat
nepřinutí. Data corupted sice nenastane (jsi-li alespoň trochu šikovnej), ale spadne to
až za běhu.
Do třetice:
V Idrisu (a Haskellu) - nalinkuju si nějakou knihovnu, použiju a pokusím se přeložit, a ono to začne řvát tady a tady a tady a tady... opravím, přeložím, běží.
V C# - nalinkuju si nějakou knihovnu, použiju, a úspěšně přeložím, spustím, a ono to začne padat tehdy, a tehdy, a tehdy, a tehdy... nejlépe u zákazníka.