型推論 1 (変数、戻り型が単一の型に定まる物)
(define (ack m n)
(cond ((zero? m) (+ n 1))
((zero? n) (ack (- m 1) 1))
(else (ack (- m 1) (ack m (- n 1))))))

(ack (m ?x) (n ?y)) : (result ?z) から ?x ?y ?zの型を求める

(zero? m) => (type_a) : bool
1 => int
(+ n 1) => (int int) : int から ?x = int
(zero? n) => (type_a) : bool
m, nがintなのでzero?の引数は intと仮定して良い
(- m 1) => (int int) : int から ?y = int
末尾コンテキストは+ とackのみなので?z = int
これでack内の +-zero?演算子はintという前提で最適化でける

・・という感じで良い?