# fixedpoint.jp

## ケーススタディ -- Prolog と型システム (2008-02-08)

> I consider this a limitation (bug) in current Prolog compilers. Every
> Prolog compiler should compile this code into something like this:

> a(N,_) :- var(X), original_code_for_a(X).
> a(N,_) :- ( N> 0 -> .. ; ... ).

Don't forget that N > 0 and N =< 0 may both fail with ieee floats.
So to be safe you'd need some analysis too. 

の辺りから、型によるデータの整合性をチェックするという話になっています。

This is getting interesting.

If we observe that the constant 0 is an integer, then we may avoid the
problem by using:

a(N,_) :- ( integer(N) -> (N> 0 -> ... ;  ... ) ; original_code ).

or, in case we want to accept expressions that evaluate to an integer:

a(N,_) :- ( evaluates_to_integer(N,N1) -> (N1 > 0 -> ... ;  ... ) ;
original_code ).

This would allow to further simplify the code for N1>0, as no type-
checking would now be required.

But I am sure Bart will find something wrong with this :) Or he is



この述語の役割は型によるチェックであり、こういった型の有用性を生かすために型の宣言を利用するべきだという意見が出ます。

Given that experts (Jan, Vitor) make subtle mistakes, and given the
pitfalls of floating point arithmetic (see what Joachim wrote), and
because of the pitfalls of unification (with 0 for instance) is quite
different from arithmetic equality testing (=:= 0) ...

wouldn't the following be a better way to write fac/2:

:- type facbartpref(nonnegint:in, int:out). % (*)

facbartpref(0,1).
facbartpref(N,Res) :-
N == 0,
M is N - 1,
facbartpref(M,Temp),
Res is N * Temp.

I have replaced the N > 0 by N == 0. A decent compiler should be able
to avoid choicepoints, and if statically, it cannot prove that
facbartpref is called correctly, it can insert a minimal set of tests
to ensure this.

Why is the Prolog community still so scared of type/mode declarations,
when their advantage is so obvious.
(*) modulo choice of syntax and type system


これに対するさまざまな反応;

• こういうときに宣言的にやる必要ないよ、Mercury じゃないんだし。
• 処理系によっては実行時に変数の値の型をチェックする述語(e.g. SWI-Prolog の must_be/2)が宣言的に使えるよ。
• 型(タイプ)のシステムだとたくさん指でタイプしなきゃいけなくなるよね。
• "型なし"言語は業界では歓迎されないよね。
• なぜ型付き言語は論理プログラミングの研究分野では歓迎されないの?
• 型付き言語に進化しようとしないなんて、Prolog は生き残りを拒否してるみたいなもんだ。
• 確かに自前で型チェックできるけど、ランタイムが勝手にやってくれたらいいのに。

この議論の中で最も共感できたのは、SWI-Prolog の開発者 Jan Wielemaker の次の意見です:

So my first reading was correct after all.  There is 75% characters
replace these tests.