1

この質問は試験から取られています。どうすればいいのかわかりません。:-(

質問：タイプがであるhaskellまたはml関数の例を挙げてください

（a-> b）->（c-> a）-> c-> b

どうやってするか？

4

3 に答える 3

7

どのような意味のある関数がそのタイプを持つことができますmystery :: ( a -> b ) -> ( c -> a ) -> c -> bか？

見てみましょう、何ができますか

mystery f g x

なれ？

使用するものが3つあります。

  • xタイプの1つの値c、
  • gタイプの1つの関数c -> aと
  • fタイプの1つの関数a -> b。

タイプの値を生成しますb。

関係する唯一の引数bは関数fであるため、結果はである必要がありますf ???。

fここでの議論は何でしょうか？タイプが必要aであり、指定された引数からそのタイプの値を生成する唯一の方法（ボトムス、、を無視undefined）error "foo"は何かに適用gすることであるため、

mystery f g x = f (g ??)

しかし、何gに適用できるでしょうか？これは、タイプの値である必要がありますc。ボトムスを除いてc、引数から構築できる型の唯一の値はx、です。

mystery f g x = f (g x)

関数合成（または未定義）である必要があります。

于 2012-12-31T05:27:57.380 に答える
4

これまでの他の回答は、これを一般的に行うための論理的な手順を実際には示していません。100％詳細には示しませんが、例を示します。

これに対する「深い」トリックは、与えられたタイプの関数を見つけることは、論理定理を証明することと同等であるということです。LemmonのシステムLの形式（いくつかの最初の論理コースで使用される自然演繹のより親しみやすい形式）を使用すると、例は次のようになります。

Theorem:  ??? :: (a -> b) -> (c -> a) -> c -> b

1.                 f :: a -> b  (aux. assumption)
2.                 g :: c -> a  (aux. assumption)
3.                 x :: c       (aux. assumption)
4.               g x :: a       (2, 3, -> elim; assumes 2, 3)
5.           f (g x) :: b       (1, 4, -> elim; assumes 1, 2, 3)
6.     \x -> f (g x) :: c -> b  (3, 4, -> intro; discharges 3, assumes 1, 2)

7.   \g x -> f (g x) :: (c -> a) -> c -> b
                        (2, 6, -> intro; discharges 2, assumes 1)

8. \f g x -> f (g x) :: (a -> b) -> (c -> a) -> c -> b  
                        (1, 7, -> intro; discharges 1)

ここでの考え方は、関数型プログラミング言語とロジックの間に次のような密接な対応があるということです。

  1. タイプは論理命題に対応します
  2. 関数定義は論理証明に対応します
  3. 論理的証明規則は、プログラミング言語式の作成方法に関する規則に対応しています。

したがって、「補助仮定」の論理的証明規則（ステップ1〜3）は、新しい自由変数の導入に対応します。含意除去規則（ステップ4-5、別名「モーダスポネンス」）は関数適用に対応します。含意導入ルール（ステップ6〜8、別名「仮説的推論」）は、ラムダ抽象化に対応します。補助的な仮定を解くという概念は、自由変数の束縛に対応しています。前提のない証明の概念は、自由変数のない式の概念に対応します。

于 2012-12-31T20:05:17.940 に答える
2

その関数は関数合成演算子であり、関数のタイプをHoogleに入力すると、次のことがわかります。http://www.haskell.org/hoogle/?hoogle = %28+a+-%3E+b+%29+- ％3E +％28 + c +-％3E + a +％29 +-％3E + c +-％3E + b ++

次に、クリックしてソースを表示できます。

(.)    :: (b -> c) -> (a -> b) -> a -> c
(.) f g = \x -> f (g x)
于 2012-12-31T05:21:53.043 に答える