4

次のような関数を定義したいと思います。

(define (((lift fn) . gs) . args)
  (apply fn (map (lambda (g) (apply g args)) gs)))

これは基本的に関数を「持ち上げる」fnので、通常の引数を受け入れる代わりに、関数を受け入れて新しい関数を生成します。したがって、たとえば、

 (define add (lift +))
 (define sum-of-sin-and-cos (add sin cos))
 (sum-of-sin-and-cos 5) ; is equivalent to (+ (sin 5) (cos 5))

 (define sum-of-multiplication-and-division (add * /))
 (sum-of-multiplication-and-division 1 2 3 4 5) ; is equivalent to (+ (* 1 2 3 4 5) (/ 1 2 3 4 5))

これはプレーンラケットで機能します。ここで、この関数を型付きラケットに移動したいと思います。これが私が思いついた型宣言です：

(: lift (All (A ... ) (All (B ...) (All (C)
             ((B ... B -> C) ->
                     ((A -> B) ... B ->
                               (A ... B -> C)))))))

これが私が定義が言っていると思うA0ものです：すべてのタイプについてA1、、、 ..AnおよびB0、、B1... Bn、およびC：

  • liftB0（ 、、、B1... Bntoの関数）を取り、以下Cを生成します。
  • 多くの関数（AiからBi、i0からn）の関数。これにより、次の関数が生成されます。
  • 0からAi、までのの関数。これにより、次のようになります。in
  • aC

これは機能しません。最後の行(A ... B -> C)でType Checker: Type variable A must be used with ... in: A。

これは、Typed Racketを使用しているときに発生した省略記号の最初の問題ではありません。これは、省略記号の意味についての根本的な誤解の事例だと思います。

Allちなみに、句を次のように1つにまとめようとすると、次のようになります。

(All (A ... B ... C) blah blah blah)

次に、2行目((B ... B - C) ->に次のエラーが表示されますType Checker: Used a type variable (B) not bound with ... as a bound on a ... in: B（その行の2番目のBを参照）。私もそれをよく理解していません。

4

1 に答える 1

5

最後の質問に最初に答えるために、の型構文でAllは、複数のドット付き変数を一度にバインドすることはできません。これは、それらをインスタンス化する方法が明確ではないためです。これは、同じ関数で複数の残りのパラメーターを使用できないのと同じ理由です。

に関してはlift、あなたが望むタイプは次のとおりだと思います：

(: lift (All (C A ...)
             (All (B ...)
                  ((B ... B -> C)
                   ->
                   ((A ... A -> B) ... B 
                    ->
                    (A ... A -> C))))))

そして、関数は 1 つの注釈で処理されます。

(define (((lift fn) . gs) . args)
  (apply fn (map
             (λ: ([g : (A ... A -> B)])
               (apply g args))
             gs)))

forall がネストされているため、この関数を使用するには明示的な注釈が必要です。ここにあなたのテストケースがあります：

(define add ((inst (inst lift Number Number) Number Number) +))
(define add2 ((inst (inst lift Number Number Number Number Number Number)
                    Number Number)
              +))
(define sum-of-sin-and-cos (add sin cos))
(sum-of-sin-and-cos 5) ; is equivalent to (+ (sin 5) (cos 5))
(define sum-of-multiplication-and-division (add2 * /))    
(sum-of-multiplication-and-division 1 2 3 4 5)

add2異なる型で使用されるため、別のバインディングを作成する必要があることに注意してください。

于 2012-12-13T20:34:15.370 に答える