http://www.ats-lang.org/DOCUMENT/INT2PROGINATS/HTML/p2220.html の例をAdaにしてみる

.gitignore

*.ali
*.o

x2382.ads

-- http://www.ats-lang.org/DOCUMENT/INT2PROGINATS/HTML/x2382.html
package x2382 is

   -- Natural is predefined type.
   -- subtype Natural is Integer range 0 .. Integer'Last;

   function fact (x : Natural) return Natural is
     (if x > 0 then x * fact (x - 1) else 1);

end x2382;

x2407.ads

-- http://www.ats-lang.org/DOCUMENT/INT2PROGINATS/HTML/x2407.html
package x2407 is

   -- String is predefined type.
   -- type String is array (Positive range <>) of Character;

   function string_is_atend (str : String; i : Natural) return Boolean is
     (Natural'Succ (i) = str'Last)
      with Pre => i in str'First .. Natural'Succ (str'Last);

   function string_isnot_atend (str : String; i : Natural) return Boolean is
     (i <= str'Last)
      with Pre => i in str'First .. Natural'Succ (str'Last);

   function inner_loop_1 (str : String; i : Natural) return Natural is
     (if string_isnot_atend (str, i) then inner_loop_1 (str, Natural'Succ (i)) else i);

   function string_length (str : String) return Natural is
     (inner_loop_1 (str, str'First));

   subtype charNZ is Character
      range Character'Val (1) .. Character'Last;

   function string_get_at (str : String; i : Natural) return charNZ;
   procedure string_set_at (str : String; i : Natural; c : charNZ);
   -- implementation is omitted...

   type sizeLt (n : Integer) is record
      i : Integer;
   end record
      with Dynamic_Predicate => sizeLt.i < sizeLt.n;

   type Option_sizeLt (Has_Element : Boolean; n : Integer) is record
      case Has_Element is
         when False =>
            null;
         when True =>
            Item : sizeLt (n);
      end case;
   end record;

   function inner_loop_2 (str : String; c0 : Character; i : Natural) return Option_sizeLt is
     (if string_isnot_atend (str, i) then
        (if c0 = str (i) then (Has_Element => True, n => str'Last, Item => (n => str'Last, i => i))
         else inner_loop_2 (str, c0, Natural'Succ (i)))
      else (Has_Element => False, n => str'Last));

   function string_find (str : String; c0 : Character) return Option_sizeLt is
     (inner_loop_2 (str, c0, str'First));

   function string_test_at (str : String; i : Natural) return Character
      with Pre => i <= str'Last,
           Post => (string_test_at'Result /= Character'Val (0) and then i <= str'Last)
                   or else (string_test_at'Result = Character'Val (0) and then i > str'Last);

   function inner_loop_3 (str : String; c0 : Character; i : Natural) return Option_sizeLt is
     (if string_test_at (str, i) /= Character'Val (0) then
        (if c0 = str (i) then (Has_Element => True, n => str'Last, Item => (n => str'Last, i => i))
         else inner_loop_3 (str, c0, Natural'Succ (i)))
      else (Has_Element => False, n => str'Last));

   function string_find_2 (str : String; c0 : Character) return Option_sizeLt is
     (inner_loop_3 (str, c0, str'First));

end x2407;

x2454.ads

-- http://www.ats-lang.org/DOCUMENT/INT2PROGINATS/HTML/x2454.html
package x2454 is

   generic
      type a is private;
      type size_t is (<>);
      type arrayref is array (size_t range <>) of a;
   function array_make_elt (asz : size_t; elt : a) return arrayref;
   -- implementation is omitted...

   generic
      type a is private;
      type size_t is (<>);
      type arrayref is array (size_t range <>) of a;
   function arrayref_get_at (Ar : arrayref; i : size_t) return a
      with Pre => i in Ar'Range;
   -- implementation is omitted...

   generic
      type a is private;
      type size_t is (<>);
      type arrayref is array (size_t range <>) of a;
   procedure arrayref_set_at (Ar : arrayref; i : size_t; x : a)
      with Pre => i in Ar'Range;
   -- implementation is omitted...

   generic
      type a is private;
      type size_t is range <>;
      type arrayref is array (size_t range <>) of a;
      with function cmp (Left, Right : a) return Integer;
   package bsearch_arr_Package is

      function inner_loop (Ar : arrayref; x0 : a; l, u : size_t) return size_t is
        (if l <= u then
           (if cmp (x0, Ar ((l + u) / 2)) >= 0 then inner_loop (Ar, x0, (l + u) / 2 + 1, u)
            else inner_loop (Ar, x0, l, (l + u) / 2 - 1))
         else u)
         with Pre => l in Ar'Range and then u in Ar'Range and then l <= u;

      function bsearch_arr (Ar : arrayref; x0 : a) return size_t is
        (inner_loop (Ar, x0, Ar'First, Ar'Last));

   end bsearch_arr_Package;

end x2454;

x2479.ads

-- http://www.ats-lang.org/DOCUMENT/INT2PROGINATS/HTML/x2479.html
package x2479 is

   -- 再帰深度を限定する方法はAdaにもgccにも無い
   -- スタックの使用量を解析させて調べるか
   -- inline展開させて関数呼び出しが消えるのを確認するか
   -- 再帰の回数を数える引数を追加するか
   -- SPARKに機能がないか調べるか(SPARK知らない)
   -- まあこの程度の例は再帰させずに手続き型で書けばいいのですけれど
   -- そして、"Introduction to Dependent Types"の章にあった例だけれども
   -- 依存型あんまり関係ない機能の気がする...

   -- limited to x times
   function fact (x : Natural) return Natural is
     (if x > 0 then x * fact (x - 1) else 1);

   -- limited to Integer'Max (101 - x, 0) times
   function f91 (x : Integer) return Integer is
     (if x >= 101 then x - 10 else f91 (f91 (x + 11)))
     with Post => (x < 101 and then f91'Result = 91)
                  or else (x >= 101 and then f91'Result = x - 10);

   -- limited to (m, n) ???
   function acker (x, y : Integer) return Natural is
     (if x > 0 then
        (if y > 0 then acker (x - 1, acker (x, y - 1)) else acker (x - 1, 1))
      else y + 1);

   -- limited to 2 * n
   function isevn (n : Integer) return Boolean;
   -- limited to 2 * n + 1
   function isodd (n : Integer) return Boolean;

   function isevn (n : Integer) return Boolean is
     (if n = 0 then true else isodd (n - 1));

   function isodd (n : Integer) return Boolean is
     (not isevn (n));

end x2479;

x2529.ads

-- http://www.ats-lang.org/DOCUMENT/INT2PROGINATS/HTML/x2529.html
package x2529 is

   package Plain is

      function diff (r : Integer) return Integer is
        (r - 1);

      function m (l, r : Integer) return Integer is
        (l + diff (r) / 2);

      function search (x, l, r : Integer) return Integer is
        (if diff (r) > 0 then
           (if x / m (l, r) < m (l, r) then search (x, l, m (l, r))
            else search (x, m (l, r), r))
         else l);

      function isqrt (x : Integer) return Integer is
        (search (x, 0, x));

   end Plain;

   package Annotated is

      function diff (r : Integer) return Integer is
        (r - 1);

      function m (l, r : Integer) return Integer is
        (l + diff (r) / 2);

      -- limited to r - l
      function search (x, l, r : Natural) return Integer is
        (if diff (r) > 1 then
           (if x / m (l, r) < m (l, r) then search (x, l, m (l, r))
            else search (x, m (l, r), r))
         else l)
         with Pre => l < r;

      function isqrt (x : Integer) return Integer is
        (if x > 0 then search (x, 0, x) else 0);

   end Annotated;

end x2529;

https://gist.github.com/ytomino/3e617b80d91a22e9ae8c#file-x2382-ads-L8 この部分なんですが"(if x > 0 then x * fact (x - 10) else 1);"にしてもコンパイル通っちゃいませんか？？？

ATS2の場合以下のコードはエラーになります

casper$ cat fact.dats
#include
"share/atspre_staload.hats"

fun fact {n:nat} .<n>.
  (x: int n): int = if x > 0 then x * fact (x-10) else 1

implement main0 () = ()
casper$ patscc fact.dats
exec(patsopt --output fact_dats.c --dynamic fact.dats)
Hello from ATS2(ATS/Postiats)!
The 1st translation (fixity) of [fact.dats] is successfully completed!
The 2nd translation (binding) of [fact.dats] is successfully completed!
/home/kiwamu/tmp/fact.dats: 104(line=5, offs=43) -- 104(line=5, offs=43): error(3): unsolved constraint: C3NSTRprop(main; S2Eapp(S2Ecst(>=); S2EVar(4097->S2Eapp(S2Ecst(sub_int_int); S2EVar(4095->S2Evar(n(7574))), S2EVar(4096->S2Eintinf(10)))), S2Eintinf(0)))
typechecking has failed: there are some unsolved constraints: please inspect the above reported error message(s) for information.
exit(ATS): uncaught exception: _2home_2kiwamu_2src_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorException(1025)
exec(patsopt --output fact_dats.c --dynamic fact.dats) = 256

もちろん元のコードはコンパイルに成功します

casper$ cat fact.dats
#include
"share/atspre_staload.hats"

fun fact {n:nat} .<n>.
  (x: int n): int = if x > 0 then x * fact (x-1) else 1

implement main0 () = ()
casper$ patscc fact.dats
exec(patsopt --output fact_dats.c --dynamic fact.dats)
Hello from ATS2(ATS/Postiats)!
The 1st translation (fixity) of [fact.dats] is successfully completed!
The 2nd translation (binding) of [fact.dats] is successfully completed!
The 3rd translation (type-checking) of [fact.dats] is successfully completed!
The 4th translation (type/proof-erasing) of [fact.dats] is successfully completed!
exec(patsopt --output fact_dats.c --dynamic fact.dats) = 0
exec(gcc -std=c99 -D_XOPEN_SOURCE -I${PATSHOME} -I${PATSHOME}/ccomp/runtime -L${PATSHOME}/ccomp/atslib/lib -L${PATSHOME}/ccomp/atslib/lib64  fact_dats.c)
exec(gcc -std=c99 -D_XOPEN_SOURCE -I${PATSHOME} -I${PATSHOME}/ccomp/runtime -L${PATSHOME}/ccomp/atslib/lib -L${PATSHOME}/ccomp/atslib/lib64  fact_dats.c) = 0

casper$ cat x2382.ads
-- http://www.ats-lang.org/DOCUMENT/INT2PROGINATS/HTML/x2382.html
package x2382 is

   -- Natural is predefined type.
   -- subtype Natural is Integer range 0 .. Integer'Last;

   function fact (x : Natural) return Natural is
     (if x > 0 then x * fact (x - 10) else 1);

end x2382;
casper$ gnatmake -gnat2012 x2382.ads
gcc-4.6 -c -gnat2012 x2382.ads

Adaのsubtypeや*_Predicateは実行時チェックの機能ですので……
実行時にConstraint_Error(またはAssertion_Error)になります。
後はコンパイラが超賢ければ警告ぐらいは出してくれるかも、といったところです。

そもそもそれを静的にエラーにするには"-"演算子に引数と返り値の関係を示す注釈が入ってないといけないと思うのですが、Adaの既定義の"-"にそんなものはないです。

あー。実行時エラーは個人的に興味がありません。。。関数型言語もどーでもよくって、ぼくは実行時エラーをコンパイル時エラーにしたいのです。 http://www.slideshare.net/master_q/20140726-ajhc-tlug/9

"-"をオーバロードすることはできないんですか？

ということは値の検査器のようなものがGNATのランタイムに入っていることになりますね。。。

手習いでサンプルをなぞっては見てますが、そもそもIntegerは割とどうでもよくて、Adaに依存型モドキと言える物があるとすればdiscriminantsではないか(↑で言えばOption_sizeLt)とは思うのですが……