与えられた Haskell 関数は次のとおりです。
head . filter fst
問題は、手で「手動で」タイプを見つける方法です。Haskell にタイプを教えてもらうと、次のようになります。
head . filter fst :: [(Bool, b)] -> (Bool, b)
しかし、次のように定義されている使用済み関数のシグネチャのみを使用して、これがどのように機能するかを理解したいと思います。
head :: [a] -> a
(.) :: (b -> c) -> (a -> b) -> a -> c
filter :: (a -> Bool) -> [a] -> [a]
fst :: (a, b) -> a
編集：非常に多くの非常に優れた説明...最適なものを選択するのは簡単ではありません!
タイプは、一般に統合と呼ばれるプロセスを使用して推測されます。Haskellは、式のタイプを決定するために使用する統合アルゴリズムであるHindley-Milnerファミリーに属しています。
統合が失敗した場合、式は型エラーです。
表現
head . filter fst
パスします。手動で統合を実行して、取得したものを取得する理由を確認しましょう。
から始めましょうfilter fst：
filter :: (a -> Bool) -> [a] -> [a]
fst :: (a' , b') -> a' -- using a', b' to prevent confusion
filterを取り(a -> Bool)、次にaを取り、[a]別のを与え[a]ます。式
では、型が。である引数filter fstに渡します。これが機能するためには、型がの最初の引数の型と統合されている必要があります。filterfst(a', b') -> a'fst filter
(a -> Bool) UNIFY? ((a', b') -> a')
アルゴリズムは2つの型式を統合し、できるだけ多くの型変数（またはなど）を実際の型（など）にバインドしようとします。aa'Bool
そうして初めてfilter fst、有効な型付き式になります。
filter fst :: [a] -> [a]
a'明らかにBoolです。したがって、型変数 a'はに解決されBoolます。そして、(a', b')に統合することができaます。したがって、ais(a', b')とa'isの場合Bool、Thenaはちょうど(Bool, b')です。
（a ）のfilterように互換性のない引数をに渡した場合、2つの式は正しい型の式に統合できないため、withの統合は失敗します。42NumNum a => aa -> Bool
に戻って
filter fst :: [a] -> [a]
これはa私たちが話しているのと同じなので、代わりに前の統合の結果を置き換えます。
filter fst :: [(Bool, b')] -> [(Bool, b')]
次のビット、
head . (filter fst)
次のように書くことができます
(.) head (filter fst)
だから取る(.)
(.) :: (b -> c) -> (a -> b) -> a -> c
したがって、統一を成功させるには、
head :: [a] -> a統一する必要があります(b -> c)filter fst :: [(Bool, b')] -> [(Bool, b')]統一する必要があります(a -> b)（2）から、そのa IS bを式で
取得します(.) :: (b -> c) -> (a -> b) -> a -> c） `
したがって、 （1）はとの間の関係を与えるので、型変数と式の値は簡単にわかります。つまりa、c：はのリストです。そして、私たちが知っているように、(.) head (filter fst) :: a -> cbcbca[(Bool, b')]c(Bool, b')
したがってhead . filter fst、次のようにタイプチェックに成功します。
head . filter fst :: [(Bool, b')] -> (Bool, b')
アップデート
さまざまなポイントからプロセスの開始を統一する方法を見るのは興味深いことです。私は最初に選択filter fstし、次に進みましたが(.)、head他の例が示すように、統一はいくつかの方法で実行できます。これは、数学的な証明や定理の導出を複数の方法で実行できる方法とは異なります。
filter :: (a -> Bool) -> [a] -> [a](a -> Bool)同じ型のリストである関数を受け取り、aその型のリストも返しますa。
あなたの定義では、タイプを使用filter fstしますfst :: (a,b) -> a
filter (fst :: (Bool,b) -> Bool) :: [(Bool,b)] -> [(Bool,b)]
と推測されます。次に、結果[(Bool,b)]を で構成しますhead :: [a] -> a。
(.) :: (b -> c) -> (a -> b) -> a -> cは 2 つの関数の構成でありfunc2 :: (b -> c)、func1 :: (a -> b)です。あなたの場合、あなたは持っています
func2 = head :: [ a ] -> a
と
func1 = filter fst :: [(Bool,b)] -> [(Bool,b)]
したがって、headここでは[(Bool,b)]引数として取り、(Bool,b)定義ごとに返します。最終的には次のようになります。
head . filter fst :: [(Bool,b)] -> (Bool,b)
から始めましょう(.)。型注釈は
(.) :: (b -> c) -> (a -> b) -> a -> c
これは、「からへの関数、からへの関数、およびを与えられればb、私cはあなたに与えることができます」と言います。それをと
で使用したいので、 `：ababheadfilter fst
(.) :: (b -> c) -> (a -> b) -> a -> c
^^^^^^^^ ^^^^^^^^
head filter fst
さてhead、これは何かの配列から単一の何かへの関数です。これで、それがb配列になりc、その配列の要素になることがわかりました。したがって、私たちの表現の目的のために、私たち(.)は署名を持っていると考えることができます：
(.) :: ([d] -> d) -> (a -> [d]) -> a -> d -- Equation (1)
^^^^^^^^^^
filter fst
の署名filterは次のとおりです。
filter :: (e -> Bool) -> [e] -> [e] -- Equation (2)
^^^^^^^^^^^
fst
（すでに持っているsとの混同を避けるために、型変数の名前を変更したことに注意してください！）これは、「からBoolへaの関数と、sのリストがあれば、 sのリストを提供できます。"。関数
には次のシグネチャがあります。eeefst
fst :: (f, g) -> f
f「とを含むペアがgあれば、私はあなたに与えることができますf」と言います。eこれを式2と比較すると、値のペアになり、最初の要素はである必要があることがわかり
ますBool。filter
したがって、私たちの表現では、署名を持っていると考えることができます。
filter :: ((Bool, g) -> Bool) -> [(Bool, g)] -> [(Bool, g)]
（ここで行ったのは、式2で置き換えることだけですe。(Bool, g)）そして、式filter fstのタイプは次のとおりです。
filter fst :: [(Bool, g)] -> [(Bool, g)]
式1に戻ると、これはである必要があることがわかり(a -> [d])ます
。[(Bool, g)] -> [(Bool, g)]したがって、である必要があり、であるa必要が[(Bool, g)]ありd
ます(Bool, g)。(.)したがって、私たちの表現では、署名を持っていると考えることができます。
(.) :: ([(Bool, g)] -> (Bool, g)) -> ([(Bool, g)] -> [(Bool, g)]) -> [(Bool, g)] -> (Bool, g)
要約すると：
(.) :: ([(Bool, g)] -> (Bool, g)) -> ([(Bool, g)] -> [(Bool, g)]) -> [(Bool, g)] -> (Bool, g)
^^^^^^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
head filter fst
head :: [(Bool, g)] -> (Bool, g)
filter fst :: [(Bool, g)] -> [(Bool, g)]
すべてを一緒に入れて：
head . filter fst :: [(Bool, g)] -> (Bool, g)
gこれは、私が型変数としてではなく使用したことを除いて、あなたが持っていたものと同等ですb。
私はそれをひどい詳細で説明したので、これはおそらくすべて非常に複雑に聞こえます。しかし、この種の推論はすぐに第二の性質になり、頭の中でそれを行うことができます。
（手動導出のためにスキップします）
与えられたhead . filter fst==の型を見つける((.) head) (filter fst)
head :: [a] -> a
(.) :: (b -> c) -> ((a -> b) -> (a -> c))
filter :: (a -> Bool) -> ([a] -> [a])
fst :: (a, b) -> a
これは、小さな Prolog プログラムによって純粋に機械的な方法で実現されます。
type(head, arrow(list(A) , A)). %% -- known facts
type(compose, arrow(arrow(B, C) , arrow(arrow(A, B), arrow(A, C)))).
type(filter, arrow(arrow(A, bool), arrow(list(A) , list(A)))).
type(fst, arrow(pair(A, B) , A)).
type([F, X], T):- type(F, arrow(A, T)), type(X, A). %% -- application rule
Prologインタープリターで実行すると、自動的に生成されます
3 ?- type([[compose, head], [filter, fst]], T).
T = arrow(list(pair(bool, A)), pair(bool, A)) %% -- [(Bool,a)] -> (Bool,a)
ここで、型は、純粋に構文上の方法で、複合データ用語として表されます。たとえば、適切な定義が与えられた場合、型[a] -> aは で表されarrow(list(A), A)、Haskell の同等の可能性がある で表されます。Arrow (List (Logvar "a")) (Logvar "a")data
1 つの推論規則、アプリケーションの推論規則のみが使用され、Prolog の構造統一が使用されました。これにより、複合項が同じ形状を持ち、それらの構成要素が一致する場合に一致します: f(a 1 , a 2 , ... a n )およびg (b 1 , b 2 , ... b m ) fがg , n == mと同じであり、a iがb iと一致する場合に一致 します。論理変数は必要に応じて任意の値を取ることができますが、一度だけです。(変更できません)。
4 ?- type([compose, head], T1). %% -- (.) head :: (a -> [b]) -> (a -> b)
T1 = arrow(arrow(A, list(B)), arrow(A, B))
5 ?- type([filter, fst], T2). %% -- filter fst :: [(Bool,a)] -> [(Bool,a)]
T2 = arrow(list(pair(bool, A)), list(pair(bool, A)))
機械的な方法で手動で型推論を実行するには、物事を下に書き、側面の同等性に注意し、置換を実行して、Prolog の操作を模倣する必要があります。any ->, (_,_), []etc. を純粋に構文マーカーとして扱い、その意味をまったく理解せずに、構造の統一を使用して機械的にプロセスを実行できます。ここでは、型推論の 1 つのルールのみを使用します。適用規則: ( との並置をとに(a -> b) c ⊢ b {a ~ c}置き換えます)。名前の衝突を避けるために、一貫して論理変数の名前を変更することが重要です。(a -> b)cbac
(.) :: (b -> c ) -> ((a -> b ) -> (a -> c )) b ~ [a1],
head :: [a1] -> a1 c ~ a1
(.) head :: (a ->[a1]) -> (a -> c )
(a ->[c] ) -> (a -> c )
---------------------------------------------------------
filter :: ( a -> Bool) -> ([a] -> [a]) a ~ (a1,b),
fst :: (a1, b) -> a1 Bool ~ a1
filter fst :: [(a1,b)] -> [(a1,b)]
[(Bool,b)] -> [(Bool,b)]
---------------------------------------------------------
(.) head :: ( a -> [ c ]) -> (a -> c) a ~ [(Bool,b)]
filter fst :: [(Bool,b)] -> [(Bool,b)] c ~ (Bool,b)
((.) head) (filter fst) :: a -> c
[(Bool,b)] -> (Bool,b)
これは、多くの複雑な統合手順を使用して、「技術的な」方法で行うことができます。または、「直感的な」方法で、物事を見て「OK、ここで何を得たのか、これは何を期待しているのか」と考えることもできます。等々。
さて、filter関数とリストを期待し、リストを返します。filter fst関数を指定しますが、リストが指定されていないため、リストの入力を待機しています。したがってfilter fst、リストを取得して別のリストを返します。（ちなみに、これはかなり一般的なHaskellのフレーズです。）
次に、.演算子は出力をに「パイプ」しますhead。これはリストを期待し、そのリストから要素の1つを返します。（最初のものは、たまたまそうです。）それでfilter、思いついたものは何でも、headあなたにそれの最初の要素を与えます。この時点で、結論を出すことができます
head . filter foobar :: [x] -> x
しかし、何xですか？まあ、リストのすべての要素にfilter fst適用さfstれます（それを保持するかスローするかを決定するため）。したがってfst、リスト要素に適用可能である必要があります。そしてfst、2要素のタプルを期待し、そのタプルの最初の要素を返します。現在はを返すことをfilter期待しているので、タプルの最初の要素は。でなければならないことを意味します。fstBoolBool
これらすべてをまとめると、次のように結論付けられます。
head . filter fst :: [(Bool, y)] -> (Bool, y)
何yですか？わかりません。私たちは実際には気にしません！上記の関数は、それが何であれ機能します。これが型アノテーションです。
より複雑な例では、何が起こっているのかを理解するのが難しい場合があります。（特に奇妙なクラスインスタンスが関与する場合！）しかし、一般的な関数を含むこのような小さなインスタンスの場合、通常は「OK、ここに何が入るのか、そこに何が出るのか、この関数は何を期待するのか」と考えることができます。手動でアルゴリズムを追跡しすぎずに、答えにたどり着きます。