그런 다음 자연스럽게 <code>id</code>은 물론 <code>'a -> 'a</code></p> <p>을 입력했다, 내가</p> <pre><code>fun id x = x </code></pre> <p>를 정의하면 특정 유형의

Question

에 다형성 함수를 적용 고차 함수를 정의 id 0는 만드는, 0로 평가하는 방법 완벽한 감각.

이 완벽 의미가 있기 때문에, 나는 기능하여 캡슐화 할 수 있어야한다 : applyToZero 유형 ('a -> 'a) -> int을하고 때 applyToZero id가 0

을 평가하지만 것이라는 희망으로

fun applyToZero (f: 'a -> 'a) = f 0 

위와 같이 applyToZero을 정의하려고하면 SML/NJ가 시작하는 이상한 오류 메시지를 표시합니다.

unexpected exception (bug?) in SML/NJ: Match [nonexhaustive match failure] 
    raised at: ../compiler/Elaborator/types/unify.sml:84.37 

이것은 거의 컴파일러 자체의 버그처럼 보입니다. 이상하지만 가능합니다.

그러나 PolyML 중 하나를 좋아하지 않는다 (의 오류 메시지가 덜 이상한하지만) : 유추 유형 ('a -> 'a) -> int와

fun ignoreF (f: 'a -> 'a) = 1 

:

> fun applyToZero (f: 'a -> 'a) = f 0; 
poly: : error: Type error in function application. 
    Function: f : 'a -> 'a 
    Argument: 0 : int 
    Reason: Can't unify int to 'a (Cannot unify with explicit type variable) 
Found near f 0 

다음 작업을 수행합니다. 이것은이 유형의 고차 함수를 생성하는 것이 불가능하지 않다는 것을 보여줍니다.

왜 SML은 내 정의 applyToZero을 허용하지 않습니까? 해당 유형을 ('a -> 'a) -> int되도록 정의 할 수있는 해결 방법이 있습니까?

동기 부여 : this question의 퍼즐을 해결하기 위해 내 시도에, 나는 모든 정수 n에 대한 유형 int -> 'a -> 'a의 함수 tofun 원하는 특성 fromfun (tofun n) = n 또 다른 기능 fromfun을 정의 할 수 있었다. 그러나 내 작업 fromfun의 추론 된 유형은 ('int -> 'int) -> 'int)입니다. SML이 ('a -> 'a) -> int으로 받아 들일 수 있도록 형식 주석을 추가하려는 모든 시도가 실패했습니다. fromfun이라는 내 정의를 보여주고 싶지 않습니다. 그 질문을 한 사람이 여전히 그 퍼즐에서 작업하고있을 수도 있기 때문입니다. 그러나 applyToZero의 정의는 똑같은 오류 메시지를 유발합니다.

Answer 1

SML에서 사용하는 것처럼이 소위 지원하지 않기 때문에 그것은, 일반 힌들리 - 밀너에서 수행 할 수없는을 이상 순위를 또는 일류 다형성. 형식 주석 'a -> 'a 및 유형 ('a -> 'a) -> int은 그들이하는 일을 생각하는 것을 의미하지 않습니다.

유형 변수의 바인더를 명시 적으로 지정하면 명확 해집니다.

fun ignoreF (f: 'a -> 'a) = 1 

는 실제로

fun 'a ignoreF (f: 'a -> 'a) = 1 

가 'a하지 인수 f의 전체 기능에 ignoreF 매개 수단이다. 따라서, 함수의 형태는 I 범용 한정사 등의 종류에 대해 명시 'a 결착을 여기

ignoreF : ∀ 'a. (('a -> 'a) -> int) 

이다. SML은 모든 유형 한정어를 구문에 암시 적으로 유지하는 반면, 타입 이론에서는 이러한 유형을 작성하는 방법입니다. 이제이 있었다 당신이 생각 유형은

ignoreF : (∀ 'a. ('a -> 'a)) -> int 

주에게 차이를 기록 할 것 : 따라서 그것이 무엇이든 될 수있다, 첫 번째 버전에서, ignoreF의 호출자가 인스턴스화하는 방법을 'a 선택하게하고, 기능을 가정 할 수는 int (이 때문에 applyToZero은 유형을 확인하지 않습니다). 두 번째 유형에서는 인수 호출자 (예 : ignoreF)가 선택됩니다.

그러나 이러한 유형은 Hindley-Milner에서 지원하지 않습니다. 이것은 단지 ∀0가 최 외각에있는 소위 prenex 다형성 (또는 순위 0 다형성) 만 지원합니다. 이는이 제한 하에서 모호성이 없으므로 암시 적으로 유지할 수있는 이유입니다. 더 높은 등급의 다형성 문제는 유형 유추가 결정 불가능하다는 것입니다.

applyToZero은 SML에서 원하는 유형을 가질 수 없습니다. 그것이 뭔가를 달성하는 유일한 방법은 모듈 시스템과 펑터를 사용하는 것입니다 :

functor ApplyToZero (val f : 'a -> 'a) = struct val it = f 0 end 

, BTW 당신은 ​​SML/NJ에서 인용 오류 메시지가 아마도 당신이 보여 코드에 의해 발생 될 수 없습니다. 다른 일을 했어야합니다.

Answer 2

fun applyToZero f = f 0에서 Hindley-Milner 유형 추론 알고리즘을 사용하는 경우 f 0이라는 이유로 f : int -> 'a을 얻게됩니다. 명백하게, f은 함수 f : 'b -> 'a이다. 이 함수는 0에 적용되므로 'b = int입니다. 따라서 명시 적 형식 주석 f : 'a -> 'a은 사용자가 관찰 한 오류를 생성합니다.

그건 그렇고, SML/NJ v110.80 내 컴퓨터에서 작동 벌금과 다음과 같은 오류 메시지가 출력 :

stdIn:2.39-2.42 Error: operator and operand don't agree [overload - user bound tyvar] 
    operator domain: 'a 
    operand:   [int ty] 
    in expression: 
    f 0