17

私はあなたに機能を与えて、あなたにそれぞれのタイプを推測するように頼むたくさんのエクササイズに出くわしました。

次の例があります。これは私がやらなければならない宿題ではないことに注意してください。私はこの特定の例に対する答えを持っており、それを以下に提供します。たぶん誰かがこの種のエクササイズを推論する方法を学ぶのを手伝ってくれるでしょう。

関数：

h1 f g x y = f (g x y) x

想定されるタイプ：

h1 :: (a -> b -> c) -> (b -> d -> a) -> b -> d -> c

ありがとう！

ここ にソリューションなしで27の演習を追加しました。

それらのいくつかには、ここにソリューションが含まれています。ただし、GHCiコマンドを使用してタイプを知ることは可能です。:t

4

4 に答える 4

23 
h1 f g x y = f (g x y) x

したがって、引数リストを左から右に取得します。

  • fは2つの引数に適用される関数です。1つ目はの結果で(g x y)、2つ目はの結果です。x
    • 最初の引数がどのタイプかはまだわからないので、それを呼び出しましょうa
    • 2番目のタイプもわからないので、それを呼びましょうb
    • また、結果のタイプもわかりません（したがって、これを呼び出しますc）が、これはによって返されるタイプである必要があることはわかっています。h1
      • 今fは関数マッピングですa -> b -> c
  • gは2つの引数に適用される関数です：最初の引数xと2番目の引数y
    • の最初の引数gはの2番目の引数と同じであるfことがわかっているので、同じタイプである必要があります。b
    • の2番目の引数gはですy。これはまだプレースホルダータイプを割り当てていないため、次の引数を順番に取得します。d
    • gの結果はへの最初の引数fであり、すでにそれをラベル付けしていますa
      • これgで関数マッピングになりますb -> d -> a
  • 3番目の引数はです。これxはの2番目の引数なのでf、すでにその型にラベルを付けています。b
  • 4番目の引数はy、の2番目の引数であるため、その型gにはすでにラベルが付けられていますd
  • の結果は、前に述べたように、h1に適用fした結果であるため、同じタイプであり、すでにラベルが付けられています(g x y) xc

引数リストを順番に調べましたが、これらの各引数の型のラベル付け、推測、および統合の実際のプロセスは、の本体を調べることによって行われましたh1。

したがって、私の最初の弾丸は次のように詳しく説明できます。

  • fを検討する最初の引数なので、h1（の後にあるすべての=）の本体を見て、それがどのように使用されているかを 見てみましょう。
    • f (g x y) xfに適用されることを意味する(g x y) xのでf、関数である必要があります
    • (g x y)は括弧内にあります。これは、それらの括弧内にあるものはすべて評価されていることを意味し、その評価の結果は次の引数になります。f
    • xの単純な引数であり、の独自の引数リストfから直接渡されますh1
    • つまり、f2つの引数を取る関数です

読みやすくなる場合はf (g x y) x、Cのような表記法での同等の式は。と見なすことができますf(g(x,y), x)。fここでは、とgが2つの引数を取る関数であることがすぐにわかります。f最初の引数は、g返されるものなどです。

式の左側の、はh1 f g x y、それ自体で1つの型情報のみを提供することに注意してくださいh1。は4つの引数の関数です。引数名自体は、式の右側（の本体h1）で使用される単なるプレースホルダーです。ここでの引数の相対的な順序は、を呼び出す方法を示しているだけですが、引数を内部でどのように使用するかについては何もh1示していません。h1

繰り返しになりますが、これは手続き型の同等物です（Pythonを使用するので、タイプを入力する必要はありません）：

def h1(f, g, x, y):
    return f(g(x,y),x)

これはまったく同じ意味です

h1 f g x y = f (g x y) x

（1つの警告-部分適用-ここで問題をさらに混乱させるだけだと私は思う）。

どちらの場合も、宣言（=Haskellでは左:、Pythonでは前）は関数名とそれが取る引数の数だけを教えてくれます。

どちらの場合も、定義（Haskellの右側、Pythonの後にインデントされたブロック）から、両方とも2つの引数の関数であり、最初の引数は2番目の引数と同じであると推測できます。Haskellでは、コンパイラがこれを行います。間違った数の引数で呼び出すと、Pythonは実行時に文句を言うだけです。そうしないと、最初の引数として使用できないものが返されます。:fggfgf

于 2012-07-24T20:06:58.327 に答える
10

何もすることがない場合は、使用方法からタイプを段階的に推測し、推測された部分を統合します。定義があります

h f g x y = f (g x y) x

hしたがって、これまで完全に未知の型の4つの引数を取ることがわかります。それらa, b, c, dを呼び出して、結果の型をと呼びrます。したがって、hのタイプはと統合可能でなければなりません

a -> b -> c -> d -> r

ここで、引数の型について何が言えるかを確認する必要があります。そのために、定義の右側を見てみましょう。

f (g x y) x

したがってf、2つの引数に適用され、そのうちの2番目はの3番目の引数であるためh、その型は。であることがわかりますc。fの最初の引数のタイプについてはまだ何も知りません。の適用の結果は、の適用のf結果であるhため、fの結果タイプはrです。

f :: u -> c -> r
a = u -> c -> r

f右側のの最初の引数はですg x y。したがって、私たちは推測することができます

g :: c -> d -> u
b = c -> d -> u

gの引数はの3番目と4番目の引数であるhため、それらの型は既知であり、結果はの最初の引数になりfます。

まとめ、

f :: u -> c -> r
g :: c -> d -> u
x :: c
y :: d
h :: (u -> c -> r) -> (c -> d -> u) -> c -> d -> r

必要に応じて型変数の名前を変更します。

于 2012-07-24T20:06:54.880 に答える
6

If you want to do it the formal way, you can follow the inference rules of the type system. If all you have are applications, the rules of the simply typed lambda calculus will do (see section 2.3 of these lecture notes on lambda calculus).

The algorithm consists of building a deduction tree using the typing rules of the type system and then calculating the final type of the term by unification.

于 2012-07-24T20:14:22.847 に答える
1

関数の型の決定は、使用する型システムによって異なります。関数型プログラミング言語のほとんどは、型推論アルゴリズム（Hindley-Milnerとも呼ばれます）があるHindley-Milner型システムに基づいています。与えられた式に対して、アルゴリズムはいわゆるプリンシパルタイプを導き出します。これは基本的に、式がタイプできない場合に関数が持つことができる、または失敗する最も一般的なタイプです。これは、GHCiが入力するときに使用するものです。:t expression

Hindley-Milner型システムではポリモーフィック関数を使用できますが、すべての全称記号は型の外にある必要があります。（通常、型を操作するときに数量詞は表示されません。数量詞は省略され、想定されるだけです。）たとえば、const型a -> (b -> a)があり、数量詞をとして記述できます(∀a)(∀b)(a -> (b -> a))。ただし、HMでは次のようなタイプは許可されていません(∀a)(a -> (((∀b)b) -> a))

System Fなど、どこでも型変数の全称記号を使用できる、より表現力豊かな型システムがありますが、その型推論は決定不可能であり、主要な型の適切な概念はありません。GHCには、そのような型を使用できるようにするさまざまな言語拡張機能がありますが、型推論が失われるため、関数に型で明示的に注釈を付ける必要があります。

例：HMでは、関数xx = \f -> f fは入力できません（GHCiで試してください）。しかし、どこでもユニバーサル型数量詞を使用できる型システムでは、型があります。適切なGHC拡張子を持つHas​​kellでは、次のように書くことができます。 

{-# LANGUAGE RankNTypes #-}

xx :: (forall a. a -> a) -> (forall b. b -> b)
xx = \f -> f f

（そのRankNTypesような定量化された型を書くことはできますが、そのような関数の型推論を与えることはできないことに注意してください-あなたは自分で型を述べる必要があります。）

Hindley-Milner型システムは、優れたトレードオフです。型推論とともにポリモーフィック関数を使用できます。

興味があれば、原著を読むことができます。ただし、いくつかのタイプミスが含まれているため、読むときは注意が必要です。

于 2012-08-12T08:13:17.823 に答える