이 Standard-ML 유형 오류의 원인은 무엇입니까?

Question

내가이 매우 간단한 SML 기능의 꼬리 재귀 버전을 만들려고 :이 과정 중에

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

을, 나는 PARAMATERS에 유형 약어를 사용했다. 다음 코드는 이것을 보여주고 타입 에러를 발생시킵니다 (아래에 주어짐). 반면 타입 어노테이션을 단순히 제거하면, 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 

주어진 두 가지 오류가 있습니다. 후자는 여기서는 덜 중요하게 여겨지는데 접미어의 두 절 사이의 불일치. 헬퍼. 첫 번째는 내가 이해하지 못하는 것입니다. 첫 번째 매개 변수의 형식이 'a:list이고 두 번째 매개 변수의 형식이 'b:list임을 설명하기 위해 주석을 달았습니다. Hendley-Milner 유형 추론 알고리즘은 일반 통일의 최상위 구조로 이해해야합니다. 'b:list과 'a:list list을 통합 할 수 있습니까? 'b ---> 'a list?

EDIT : 유추 된 형식을 허용하지 않는 형식 유추 알고리즘과 관련이있을 수 있습니다. 어떤 점에서는 형식 주석에 지정된 형식보다 엄격합니다. 그러한 규칙은 매개 변수에 대한 주석과 함수 전체에 대해서만 적용될 것입니다. 이것이 올바른지 나는 모른다. 어떤 경우에는, 나는 함수 몸에 이상 유형의 주석을 이동했는데, 나는 오류 같은 종류의 수 :

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 

Answer 1

나는 SML에 대해 확실하지 않다 , 그러나 다른 함수 언어 인 F #은 이러한 상황에서 경고를줍니다. 프로그래머가 여분의 변수 'b를 도입하고'b가 유형이어야한다 '면리스트는 프로그래머가 의도 한 것처럼 일반적인 것이 아닐 수 있습니다. 가치가있다. 당신이 'a 및 'b 같은 유형의 변수를 사용하는 경우

Answer 2

, 즉 'a 및 'b이 아무것도, 독립적으로로 설정 될 수 있다는 것을 의미한다. 예를 들어, 'b이 int이고 'a이 float 인 것으로 결정하면 작동합니다. 하지만이 경우에는 'b이 'a list이어야하므로 분명히 유효하지 않습니다.

Answer 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 

요로 말할 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의 타입 시스템은 간단합니다. (알고있는 한, 결코 결정할 수 없습니다.) 그래서 명시 적 타입 주석은 절대로 필요하지 않습니다. 왜 여기에 넣고 싶니?