5

私はこれを持っている何らかの方法があるかどうか疑問に思いました：

type binary_operator = And | Or;;

type canonical;;
type not_canonical;;

type 'canonical boolean_expression =
  | Var : int -> not_canonical boolean_expression
  | Not : 'canonical boolean_expression -> 'canonical boolean_expression
  | BinOp : canonical boolean_expression * binary_operator * canonical boolean_expression -> canonical boolean_expression
  | BinOp : _ boolean_expression * binary_operator * _ boolean_expression -> not_canonical boolean_expression
;;

ここでの問題は、引数のタイプに応じて、BinOpを2回定義できないことです...

PS：「正規」とは、「式に含まれるn個の変数が0から（n-1）の範囲のintで表される」ことを意味します。一部の関数で必須にする必要があるのは不変条件です。

4

1 に答える 1

8

gadt が実際には adt のように動作する場合があるため、型コンストラクターには別の名前を付ける必要があります。

タイプを次のように定義したいとします。

type 'canonical boolean_expression =
  | Bool : bool -> canonical boolean_expression (* here I assume that you wanted to have that case too *)
  | Var : int -> not_canonical boolean_expression
  | Not : 'canonical boolean_expression -> 'canonical boolean_expression
  | BinOpC : canonical boolean_expression * binary_operator * canonical boolean_expression -> canonical boolean_expression
  | BinOpNC : _ boolean_expression * binary_operator * _ boolean_expression -> not_canonical boolean_expression
 ;;

少し変更を加えたタイプを考えてみましょう。

type 'canonical boolean_expression =
  | Bool : bool -> canonical boolean_expression
  | Var : int -> not_canonical boolean_expression
  | Not : 'canonical boolean_expression -> 'canonical boolean_expression
  | BinOpC : canonical boolean_expression * binary_operator * canonical boolean_expression -> canonical boolean_expression
  | BinOpNC : 'a boolean_expression * binary_operator * 'a boolean_expression -> 'a boolean_expression
;;

canonical boolean_expressionこれで、最後の 2 つのコンストラクターのいずれかを使用するバイナリ操作になる可能性があります。明らかに、結果の値の型を任意に選択することで得られる自由には、その結果があります。「型ケース」が重複するガジェットを作成できます。その場合、これらの値のいずれかを取る関数は、両方のケースをテストする必要があります。したがって、コンストラクターの名前を同一にすることはできません。なぜなら、型だけではどの値を扱っているかを知るのに十分ではない可能性があるからです。

たとえば、以下の関数:

 let rec compute = function 
    | Bool b -> b   
    | BinOpC (a,And,b) -> compute a && compute b
    | BinOpC (a,Or,b) -> compute a || compute b
 ;;

あなたの定義を考えると、問題なく正規表現を型チェックして処理する必要があります。BinOpNC私の変更により、コンパイラーは当然のことながら、式も含まれている可能性があると文句を言いcanonicalます。

これは、gadt のこの側面を公開するのはばかげた例のように思えます (そして実際にそうです)。なぜなら、ブール式の変更された定義は (意味的に言えば) 明らかに正しくありませんが、コンパイラは型の実用的な意味を気にしません。

本質的に、gadt は依然として adt です。適切なアクション コースを選択するためにコンストラクターに頼らなければならない状況が依然として存在する可能性があるからです。

于 2012-12-30T09:53:18.873 に答える