유추 유형은 무한 루프를 감지하는 것으로 보이지만 실제로 무슨 일이 일어나고 있습니까?

Question

Andrew Koenig에서 ML 유형 추론에 대한 일화, 저자는 구현을 사용합니다 정렬을 병합하십시오 ML에 대한 학습 운동으로서“잘못된”유형의 추론을 발견하게되어 기쁩니다.

놀랍게도, 컴파일러는

'a list -> int list

다시 말해, 이러한 종류의 함수는 모든 유형 목록을 수락하고 정수 목록을 반환합니다.

그것은 불가능합니다. 출력은 입력의 순열이어야합니다. 어떻게 다른 유형을 가질 수 있습니까? 독자는 반드시 내 첫 임펄스 친숙한 것을 알게 될 것입니다. 컴파일러에서 버그를 발견했는지 궁금했습니다!

그것에 대해 조금 더 생각한 후, 나는 그 기능이 그 주장을 무시할 수있는 또 다른 방법이 있다는 것을 깨달았다. 아마도 그것은 때때로 전혀 돌아 오지 않았을 것이다. 실제로, 내가 그것을 시도했을 때, 그것은 정확히 일어난 일입니다. sort(nil) 돌아 왔습니다 nil, 비어 있지 않은 목록을 정렬하면 무한 재귀 루프가됩니다.

Haskell으로 번역되었을 때

split [] = ([], [])
split [x] = ([x], [])
split (x:y:xs) = (x:s1, y:s2)
  where (s1,s2) = split xs

merge xs [] = xs
merge [] ys = ys
merge xx@(x:xs) yy@(y:ys)
  | x < y     = x : merge xs yy
  | otherwise = y : merge xx ys

mergesort [] = []
mergesort xs = merge (mergesort p) (mergesort q)
  where (p,q) = split xs

GHC는 유사한 유형을 유추합니다.

*Main> :t mergesort
mergesort :: (Ord a) => [t] -> [a]

어떻게 Damas – Hindley – Milner 알고리즘 이 유형을 추론 하시겠습니까?

Answer 1

이것은 실제로 놀라운 예입니다. 무한 루프가 본질적으로 감지됩니다 시간을 컴파일하십시오! 이 예에서는 힌 들리 - 무기 추론에 대해 특별한 것이 없습니다. 평소와 같이 진행됩니다.

GHC는 유형을 얻습니다 split 그리고 merge 바르게:

*Main> :t split
split :: [a] -> ([a], [a])
*Main> :t merge
merge :: (Ord t) => [t] -> [t] -> [t]

지금은 mergesort, 일반적으로 함수 t입니다.₁→ t₂ 일부 유형 t₁ 그리고 t₂. 그런 다음 첫 번째 줄을 봅니다.

mergesort [] = []

그리고 그것을 깨닫습니다₁ 그리고 t₂ 목록 유형이어야합니다₁= [t₃] 및 t₂= [t₄]. 따라서 Mergesort는 함수 여야합니다 [t₃] → [t₄]. 다음 줄

mergesort xs = merge (mergesort p) (mergesort q) 
  where (p,q) = split xs

그것을 말합니다 :

• XS는 일부 A에 대해 [A]의 유형을 분할하는 입력이어야합니다 (이미 a = T입니다.₃).
• 그래서 p 그리고 q 또한 유형입니다 [t₃], 부터 split a] → ([a], [a])입니다.
• mergesort p, 그러므로 (Mergesort가 유형 인 것으로 여겨진다는 것을 상기₃] → [t₄])는 [t₄].
• mergesort q 유형 [t₄] 정확히 같은 이유로.
• 처럼 merge 유형이 있습니다 (Ord t) => [t] -> [t] -> [t], 및 표현식의 입력 merge (mergesort p) (mergesort q) 둘 다 유형입니다 [t₄], 타입 t₄ 들어 있어야합니다 Ord.
• 마지막으로, 유형 merge (mergesort p) (mergesort q) 두 입력, 즉 [t₄]. 이것은 이전에 알려진 유형 [t₃] → [t₄] 을 위한 mergesort, 따라서 더 이상 추론이 수행되지 않으며 Hindley -Milner 알고리즘의 "통일"부분이 완료되었습니다. mergesort 유형 [t₃] → [t₄] t₄ 안에 Ord.

그것이 당신이 얻는 이유입니다.

*Main> :t mergesort 
mergesort :: (Ord a) => [t] -> [a]

(논리적 추론 측면에서 위의 설명은 알고리즘이 수행하는 것과 같지만 알고리즘이 따르는 특정 단계는 예를 들어 Wikipedia 페이지에 주어진 것입니다.)

Answer 2

그 유형은 당신이 결과를 통과하는 것을 볼 수 있기 때문에 추론 될 수 있습니다. mergesort 에게 merge, 목록의 헤드를 다음과 비교합니다. <, 이는 ORD TypeClass의 일부입니다. 따라서 형식 추론은 ORD 인스턴스 목록을 반환해야한다고 추론 할 수 있습니다. 물론, 실제로 무한히 되돌아 가기 때문에 실제로 반환되지 않는 유형에 대해 다른 것을 추론 할 수 없습니다.