1

型シグネチャを持つ関数を証明できるという主張を何度も見てきました

α → α

パラメータの型について何も知らないため、引数を返すことによってのみ実装できます。

id :: α → α
id a = a

その主張の例はhttp://blog.precog.com/?p=431にあります。

しかし、このような if ステートメント (疑似コード) を作成できない理由は何でしょうか?

id :: α → α
id a = if ( a is_a_String) a + "hello"
       else a

私が行方不明であるという前提条件はありますか？

4

1 に答える 1

2

そのような定理は、パラメトリック性プロパティを持つ言語でのみ保持されます。つまり、コードは実行時に型を検査できないため、実行が型情報に依存することはありません。ほとんどの関数型言語にはこのプロパティがありますが、オブジェクト指向言語では、パラメトリック性を壊すダウンキャストや類似の機能を提供する必要性がしばしば見られます。

パラメトリック性は非常に強力なプロパティです。それは、あなたが言及したような特定の抽象化プロパティ、いわゆる「自由定理」を保証し、実行時に型を消去できる効率的な実装のイネーブラーです。

こちらの私の回答も参照してください。

于 2013-03-02T09:24:06.883 に答える