ATS и арифметика в типах

Сегодня тема попроще.

Мы видели, что зависимые типы в ATS позволяют логически связать между собой разные значения и во время компиляции проверить выполнимость всех статических условий. Как это работает и какие имеет ограничения? Напишем в качестве примера функцию поиска подстроки. В ней будут два цикла, в которых так легко где-нибудь ошибиться на единичку:

fn search {n,m:nat | m <= n}
  (str : string n, sub : string m) : [p:int | p <= n - m] int p = let
  val n = int1_of_size1 (string_length str)
  val m = int1_of_size1 (string_length sub)
  fun cmp {i,j:nat | i < n-m; j <= m} .<m-j>. 
    (i : int i, j : int j) :<cloref0> bool = 
      if j = m then true 
      else if str[i+j] = sub[j] then cmp(i, j+1) else false
    
  fun search_loop {k:nat | k <= n-m} .<n-k>. 
    (k : int k):<cloref0> [r:int | r <= n-m] int r = 
      if cmp(k, 0) then k 
      else if k < n - m then search_loop(k+1) else ~1
in
  if m <= n then search_loop(0) else ~1
end

Видите ошибку?
Что делает компилятор. ( Read more... )