0

この非常に単純なSML関数の末尾再帰バージョンを作成しようとしていました。

fun suffixes [] = [[]]
  | suffixes (x::xs) = (x::xs) :: suffixes xs;

この過程で、私はパラメータに型注釈を使用していました。次のコードはこれを示しており、タイプエラーが発生します（以下を参照）が、タイプアノテーションを削除するだけで、SMLは問題なくそれを受け入れ、関数全体に上記のより単純な関数と同じシグネチャを与えます。

fun suffixes_tail xs =
    let
        fun suffixes_helper [] acc = []::acc
          | suffixes_helper (x::xs:'a list) (acc:'b list) =
                suffixes_helper xs ((x::xs)::acc)
    in
        suffixes_helper xs []
    end;

エラー：

$ sml typeerror.sml 
Standard ML of New Jersey v110.71 [built: Thu Sep 17 16:48:42 2009]
[opening typeerror.sml]
val suffixes = fn : 'a list -> 'a list list
typeerror.sml:17.81-17.93 Error: operator and operand don't agree [UBOUND match]
  operator domain: 'a list * 'a list list
  operand:         'a list * 'b list
  in expression:
    (x :: xs) :: acc
typeerror.sml:16.13-17.94 Error: types of rules don't agree [UBOUND match]
  earlier rule(s): 'a list * 'Z list list -> 'Z list list
  this rule: 'a list * 'b list -> 'Y
  in rule:
    (x :: xs : 'a list,acc : 'b list) =>
      (suffixes_helper xs) ((x :: xs) :: acc)
/usr/local/smlnj-110.71/bin/sml: Fatal error -- Uncaught exception Error with 0
 raised at ../compiler/TopLevel/interact/evalloop.sml:66.19-66.27

与えられた2つのエラーがあります。後者はここではそれほど重要ではないようです。suffixes_helperの2つの句の不一致です。最初は私が理解していないものです。'a:list最初のパラメータがタイプであり、2番目のパラメータがタイプであることを示すために注釈を付け'b:listます。私が理解しているように、一般的な統一の最上位に構築されているHindley-Milner型推論アルゴリズムは、？の置換を使用して、で'b:list統一できるべきではありません。'a:list list'b ---> 'a list

編集：答えは、ある意味で型注釈によって与えられたものよりも厳密な推論された型を許可しない型推論アルゴリズムと関係があるかもしれないことを示唆しています。このようなルールは、パラメーターと関数全体の注釈にのみ適用されると思います。これが正しいかどうかはわかりません。いずれにせよ、型アノテーションを関数本体に移動しようとすると、同じ種類のエラーが発生します。

fun suffixes_helper [] acc = []::acc
    | suffixes_helper (x::xs) acc =
          suffixes_helper (xs:'a list) (((x::xs)::acc):'b list);

エラーは次のとおりです。

typeerror.sml:5.67-5.89 Error: expression doesn't match constraint [UBOUND match]
  expression: 'a list list
  constraint: 'b list
  in expression:
    (x :: xs) :: acc: 'b list
4

3 に答える 3

3

これは機能します：

fun suffixes_tail xs =
    let
        fun suffixes_helper [] acc = []::acc
          | suffixes_helper (x::xs:'a list) (acc:'a list list) =
                suffixes_helper xs ((x::xs)::acc)
    in
        suffixes_helper xs []
    end

Johとnewacctが言うように、'b list緩すぎます。明示的な型注釈を付ける場合

fun suffixes_helper (_ : 'a list) (_ : 'b list) = ...

暗黙的に次のように定量化されます

fun suffixes_helper (_ : (All 'a).'a list) (_ : (All 'b).'b list) = ...

そして明らかに同時に真実で'b = 'a listあってはなりません。(All a') (All b')

明示的な型アノテーションがない場合、型推論は正しいことを行うことができます。つまり、型を統合することです。そして実際、SMLの型システムは十分に単純なので、（私が知る限り）決定不可能になることは決してないので、明示的な型注釈は必要ありません。なぜここに入れたいのですか？

于 2009-12-07T16:22:48.637 に答える
2

'aやのような型変数を使用する場合、それは、を独立して任意に設定できることを'b意味します。したがって、たとえば、それがそうであったと判断した場合は機能するはずです。しかし、明らかにそれはこの場合は有効ではありません。'a'b'bint'afloat'b'a list

于 2009-12-06T08:16:11.163 に答える
1

SMLについてはよくわかりませんが、別の関数型言語であるF＃は、このような状況で警告を出します。エラーを出すのは少し難しいかもしれませんが、それは理にかなっています。プログラマーが余分な型変数'bを導入し、' bが型'aリストでなければならない場合、関数はプログラマーが意図したほど一般的ではない可能性があります。報告する価値があります。

于 2009-12-05T23:13:10.050 に答える