3

それ自体を再帰的に使用するパラメーター化された型がありますが、型パラメーターが特殊化されており、汎用演算子を実装すると、特殊化されたサブツリーを処理するケースのために、その演算子の型が厳密にバインドされすぎます。最初のコード サンプルは問題を示しており、2 番目のサンプル コードは使用したくない回避策を示しています。実際のコードにはさらに多くのケースがあるため、この方法でコードを複製すると保守上の問題が生じるからです。

問題を示す最小限のテスト ケースを次に示します。

module Op1 = struct
  type 'a t = A | B  (* 'a is unused but it and the _ below satisfy a sig *)

  let map _ x = match x with
    | A -> A
    | B -> B
end

module type SIG = sig
  type ('a, 'b) t =
    | Leaf  of 'a * 'b
    (* Here a generic ('a, 'b) t contains a specialized ('a, 'a Op1.t) t. *)
    | Inner of 'a * ('a, 'a Op1.t) t * ('a, 'b) t

  val map : ('a -> 'b) -> ('a_t -> 'b_t) -> ('a, 'a_t) t -> ('b, 'b_t) t
end

module Impl : SIG = struct
  type ('a, 'b) t =
    | Leaf  of 'a * 'b
    | Inner of 'a * ('a, 'a Op1.t) t * ('a, 'b) t

  (* Fails signature check:
       Values do not match:
         val map :
           ('a -> 'b) ->
           ('a Op1.t -> 'b Op1.t) -> ('a, 'a Op1.t) t -> ('b, 'b Op1.t) t
       is not included in
         val map :
           ('a -> 'b) -> ('a_t -> 'b_t) -> ('a, 'a_t) t -> ('b, 'b_t) t
   *)
  let rec map f g n = match n with
    | Leaf  (a, b)    -> Leaf  (f a, g b)
    (* possibly because rec call is applied to specialized sub-tree *)
    | Inner (a, x, y) -> Inner (f a, map f (Op1.map f) x, map f g y)
end

この修正版のは問題をImpl.map修正しましたが、メンテナンス上の問題が発生します。

  let rec map f g n = match n with
    | Leaf  (a, b)    -> Leaf  (f a, g b)
    | Inner (a, x, y) -> Inner (f a, map_spec f x, map f g y)
  and map_spec f n = match n with
    | Leaf  (a, b)    -> Leaf  (f a, Op1.map f b)
    | Inner (a, x, y) -> Inner (f a, map_spec f x, map_spec f y)

の本体を複製せずにこれを機能させる方法はありますlet rec mapか?

Gasche のソリューションを適用すると、次の作業コードが生成されます。

let rec map
    : 'a 'b 'c 'd . ('a -> 'b) -> ('c -> 'd) -> ('a, 'c) t -> ('b, 'd) t
  = fun f g n -> match n with
    | Leaf  (a, b)    -> Leaf  (f a, g b)
    | Inner (a, x, y) -> Inner (f a, map f (Op1.map f) x, map f g y)
4

1 に答える 1

5

データ型定義におけるこのスタイルの再帰は「非正規」と呼ばれます。再帰型は、定義で使用される単一の変数とは異なる'a tインスタンスfoo tで再利用されます。もう 1 つのよく知られている例は、完全な二分木 (正確に 2^n の葉を持つ) のタイプです。foo'a

type 'a full_tree =
  | Leaf of 'a
  | Node of ('a * 'a) full_tree

これらのデータ型を操作する再帰関数は、通常、型推論を伴う言語の単相再帰の​​制限を受けます。型推論を行う場合、再帰関数の本体を型チェックする前に (内部で使用されている可能性があるため)、再帰関数の型が何であるかを推測する必要があります。ML 言語は、統一/推論によってこの推測を改良しますが、推論できるのは単相型のみです。関数がそれ自体をポリモーフィックに使用する場合 (入力として受け取った型とは異なる型で再帰的に自身を呼び出す場合)、これは推論できません (一般的なケースでは判断できません)。

let rec depth = function
| Leaf _ -> 1
| Node t -> 1 + depth t
                      ^
   Error: This expression has type ('a * 'a) full_tree
   but an expression was expected of type 'a full_tree

3.12 から、OCaml は形式の明示的なポリモーフィック アノテーションの使用を許可します。これは次のこと'a 'b . fooを意味しforall 'a 'b. fooます。

let rec depth : 'a . 'a full_tree -> int = function
| Leaf _ -> 1
| Node t -> 1 + depth t

あなたの例でも同じことができます。ただし、モジュール署名にある注釈を使用した後、型をコンパイルできませんでした'a_t. これが私がそれを機能させるために使用したものです：

let rec map : 'a 'b . ('a -> 'b) -> ('a Op1.t -> 'b Op1.t) ->
                      ('a, 'a Op1.t) t -> ('b, 'b Op1.t) t
= fun f g n -> match n with
  | Leaf  (a, b)    -> Leaf  (f a, g b)
  | Inner (a, x, y) -> Inner (f a, map f (Op1.map f) x, map f g y)
于 2013-04-10T20:14:14.197 に答える