2016-04-13 10 views
6

私はちょうどハスケルを学び始めました。 Haskellは静的入力されおよび多形型推論を有するように、識別関数の種類はハスケル型推論について混乱します

IDは、そのパラメータとして任意の型を取り、それ自体を返すことができ示唆
id :: a -> a 

あります。私がしようとすると、それが正常に動作します:

a = (id 1, id True) 

私は、コンパイル時に、最初のIDはテンキーであると仮定:: - >、および第2のIDがブール値である - >ブール。それは

result = foo id 1 2 

で正常に動作しますしかし、それは事実であることから、

foo f a b = (f a, f b) 
result = foo id 1 True 

それはBと同じタイプでなければならないの種類を示しています。私は、次のコードをしようとすると、それはエラーを出しますidのパラメータの型は多相であるため、aとbは異なる型になる可能性があります。

+0

が何をしたいhttp://stackoverflow.com/questions/32496864/what-is-the-monomorphism-restrictionですか? – hao

+5

@haoformayorいいえ、これは「フォーオール」についてのことですが、単相性の制限ではありません。 AFAIK haskellは、 'forall'を持つ型を推論することはありません(rank()と呼ばれます)。' 'foo''の型は' '(forall a.a - > a) -2種類、私は思いますか?)、monomorphismの制限を無効にしても。 – amalloy

+1

ああ、それは答えです。 ghcは、ランク1型のforall a bを推論します。 (a - > b) - > a - > a - >(b、b) 'ですが、本当に' 'a a - > a - > a - > b - >(a、b)'が必要です。 – hao

答えて

8

これは、Haskellのタイプシステムの変わった奇妙なコーナーです。ここでの問題は、あなたの関数を推論する2つの方法があることです。foo

第2のタイプはあなたが望むものですが、最初のタイプは入手しているタイプです。第2のタイプは、アモロイが指摘しているように、ランク2型です(2つの意味は無視しますが、"Practical type inference for arbitrary-rank types"で紹介を読んでください)。ランクの良い説明が必要な場合は、初めにPDFファイルの性質がアクセシブルで明確に書かれています)。

上位ランクのタイプの定義を延期し、GHCがランク2タイプを推論できないという問題があるとします。

Complete type inference is known to be undecidable for higher-rank (impredicative) type systems, but in practice programmers are more than willing to add type annotations to guide the type inference engine, and to document their code....

Kfoury and Wells show that typeability is decidable for rank ≤ 2, and undecidable for all ranks ≥ 3 (Kfoury & Wells, 1994). For the rank-2 fragment, the same paper gives a type inference algorithm. This inference algorithm is somewhat subtle, does not interact well with user-supplied type annotations, and has not, to our knowledge, been implemented in a production compiler.

不可能なことは、常に正しいyes-or-noの決定につながるアルゴリズムがないことを意味します。それで、あなたはそれを持っています:ランク3以上のタイプを推論することは不可能であり、ランク2型を推論するのはあまりにも大変です。

ここでは、ランク2に戻ります。(forall a. a -> a)は、ランク2になります。 There's already an excellent Stack Overflow question about what the forall keyword meansので、私はあなたがそれを参照しますが、基本的にそれはあなたがab前にすべての、あなたが最初の場所で何を望むかで異なる種類、あることをしながら表現(f a, f b)f af bを呼び出すことができるしている意味この熱い混乱。

最後に1つ:GHCiで通常forallが表示されない理由は、非常に外側のスコープにあるforallがオフのままであることです。従ってforall a b. (a -> b) -> a -> a -> (b, b)(a -> b) -> a -> a -> (b, b)に相当します。

全体的にこれはあまり説明されていない言語の痛みです。

(コメントでハットチップを@amalloyします。)

+3

これらの2つのタイプのどちらも他よりも一般的ではないことは注目に値する。それぞれは、他の人ができない方法で使用することができます。したがって、 'foo f a b =(f a、f b)'は、実際にどの関数が定義されているかについて曖昧です。ランク1型の解釈をとることによってあいまいさが解決された瞬間です。 GHCが完全なランク2の推論を持ち、ランク1の解釈を好む歴史的な荷物がないという仮説的な世界では、選択肢を特定するものを追加する必要があります。あなたのために選ぶコンパイラ。 – Ben

+1

さて、 'forall a。 a - > aは正確に1つの非底値( '' id'')が存在するので '' foo''は本質的に '(、)'と同型です。 – user2407038

関連する問題