5

このコンビネータを考えてみましょう。

S (S K)

引数XYに適用します。

S (S K) X Y

それは以下に契約します：

X Y

S（SK）を対応するラムダ項に変換し、次の結果を得ました。

(\x y -> x y)

Haskell WinGHCiツールを使用して（\ xy-> xy）の型アノテーションを取得すると、次のように返されます。

(t1 -> t) -> t1 -> t

それは私には理にかなっています。

次に、WinGHCiを使用してs（sk）の型シグネチャを取得すると、次のように返されます。

((t -> t1) -> t) -> (t -> t1) -> t

それは私には意味がありません。型アノテーションが異なるのはなぜですか？

注：s、k、およびiを次のように定義しました。

s = (\f g x -> f x (g x))
k = (\a x -> a)
i = (\f -> f)
4

3 に答える 3

9

kとの種類から始めますs

k :: t1 -> t2 -> t1
k = (\a x -> a)

s :: (t3 -> t4 -> t5) -> (t3 -> t4) -> t3 -> t5
s = (\f g x -> f x (g x))

kしたがって、の最初の引数として渡すと、のタイプをの最初の引数のタイプとs統合し、タイプで使用しますkss

s :: (t1 -> t2 -> t1) -> (t1 -> t2) -> t1 -> t1

したがって、

s k :: (t1 -> t2) -> t1 -> t1
s k = (\g x -> k x (g x)) = (\g x -> x)

次に、s (s k)では、アウターsはタイプ（t3 = t1 -> t2、t4 = t5 = t1）で使用されます

s :: ((t1 -> t2) -> t1 -> t1) -> ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1

これを適用するとs k、最初の引数の型が削除され、

s (s k) :: ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1

要約すると：Haskellでは、の型はs (s k)その引数への影響からではなく、その構成部分式の型から派生しています。したがって、の効果を示すラムダ式よりも一般的なタイプではありませんs (s k)。

于 2012-03-06T21:33:30.777 に答える
7

使用している型システムは、基本的に単純型付きラムダ計算と同じです (再帰関数や再帰型は使用していません)。単純型付けラムダ計算は完全に一般的ではありません。これはチューリング完全ではなく、一般的な再帰の記述には使用できません。SKI コンビネータ計算はチューリング完全であり、固定小数点コンビネータと一般的な再帰を記述するために使用できます。したがって、SKI コンビネーター計算の全機能は、単純型付けされたラムダ計算では表現できません (ただし、型指定されていないラムダ計算では表現できます)。

于 2012-03-07T01:10:07.977 に答える
2

私の質問に答えてくれたすべての人に感謝します。私はあなたの反応を研究しました。私が学んだことを確実に理解するために、私は自分の質問に対する自分自身の答えを書きました。私の答えが正しくない場合は、私に知らせてください。

kとのタイプから始めますs：

   k  :: t1 -> t2 -> t1 
   k  =  (\a x -> a) 

   s  :: (t3 -> t4 -> t5) -> (t3 -> t4) -> t3 -> t5 
   s  =  (\f g x -> f x (g x))

まず、の型アノテーションの決定に取り組みましょう(s k)。

sの定義を思い出してください。

s = (\f g x -> f x (g x))

結果を代用kすると、次の契約が成立します。f(\f g x -> f x (g x))

(\g x -> k x (g x))

重要kgとxの型は、の型署名と一致している必要があります。

kこの型署名があることを思い出してください。

   k :: t1 -> t2 -> t1

したがって、この関数定義k x (g x)については、次のように推測できます。

  • のタイプxは、kの最初の引数のタイプであり、タイプt1です。

  • kの2番目の引数の型は。t2であるため、の結果は。で(g x)なければなりませんt2。

  • gxすでに決定した引数として、タイプがありますt1。したがって、の型アノテーションは(g x)です(t1 -> t2)。

  • kの結果のタイプはt1、であるため、の結果は(s k)ですt1。

したがって、の型アノテーション(\g x -> k x (g x))は次のとおりです。

   (t1 -> t2) -> t1 -> t1

次に、k常に最初の引数を返すように定義されています。したがって、この：

k x (g x)

これとの契約：

x

この：

(\g x -> k x (g x))

これとの契約：

(\g x -> x)

さて、今私たちは理解しました(s k)：

   s k  :: (t1 -> t2) -> t1 -> t1 
   s k  =  (\g x -> x)

次に、の型アノテーションを決定しましょうs (s k)。

同じように進めます。

sの定義を思い出してください。

s = (\f g x -> f x (g x))

結果を代用(s k)すると、次の契約が成立します。f(\f g x -> f x (g x))

(\g x -> (s k) x (g x))

重要gおよびの型は、の型署名xと一致している必要があります。(s k)

(s k)この型署名があることを思い出してください。

   s k :: (t1 -> t2) -> t1 -> t1

したがって、この関数定義(s k) x (g x)については、次のように推測できます。

  • のタイプxは、(s k)の最初の引数のタイプであり、タイプ(t1 -> t2)です。

  • (s k)の2番目の引数の型は。t1であるため、の結果は。で(g x)なければなりませんt1。

  • g引数としてhasxがありますが、これはすでにタイプがであると判断してい(t1 -> t2)ます。したがって、の型アノテーションは(g x)です((t1 -> t2) -> t1)。

  • (s k)の結果のタイプはt1、であるため、の結果はs (s k)ですt1。

したがって、の型アノテーション(\g x -> (s k) x (g x))は次のとおりです。

   ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1

s k以前、この定義があると判断しました。

   (\g x -> x)

つまり、2つの引数を取り、2番目の引数を返す関数です。

したがって、これは：

   (s k) x (g x)

これに対する契約：

   (g x)

この：

   (\g x -> (s k) x (g x))

これとの契約：

   (\g x -> g x)

さて、今私たちは理解しましたs (s k)。

   s (s k)  :: ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1 
   s (s k)  =  (\g x -> g x)

最後に、s (s k)の型シグネチャをこの関数の型シグネチャと比較します。

   p = (\g x -> g x)

タイプpは次のとおりです。

   p :: (t1 -> t) -> t1 -> t

ps (s k)同じ定義を持っ(\g x -> g x)ているのに、なぜそれらは異なる型シグネチャを持っているのですか？

s (s k)型シグネチャがとは異なる理由pは、に制約がないためpです。sinは、(s k)の型シグネチャと一致するように制約されkており、最初のsins (s k)は、の型シグネチャと一致するように制約されていることがわかりました(s k)。したがって、の型アノテーションはs (s k)その引数のために制約されます。pとは同じ定義を持っていますが、とs (s k)の制約は異なります。gx

于 2012-03-10T20:12:52.510 に答える