Suy luận biểu thức đệ quy sử dụng Hindley Milner & chế

Question

Tôi cố gắng để suy ra các loại biểu thức sau đây:

let rec fix f = f (fix f) 

mà phải được cung cấp các loại (a -> a) -> a

Sau khi sử dụng dưới lên thuật toán (được mô tả trong các thuật toán loại Hindley-Milner suy luận khái quát) với sự cai trị thêm bên dưới:

  a1, c1 |-BU e1 : t1  B = fresh var 
--------------------------------------------------------- 
a1\x, c1 U {t' == B | x : t' in A} |-BU let rec x = e1 : t 

tôi đang trái với các loại sau đây: t1 -> t2

và những hạn chế sau:

t0 = fix 
t1 = f 
t2 = f (fix f) 
t3 = f 
t4 = fix f 
t5 = fix 
t6 = f 

t3 = t1 
t3 = t4 -> t2 
t5 = t0 
t5 = t6 -> t4 
t6 = t1 

tôi không thể xem làm thế nào những khó khăn này có thể được giải quyết như thế mà tôi đang trái với kiểu (a -> a) -> a. Tôi hy vọng nó là hiển nhiên đối với một người nào đó để xem là tôi đang đi sai.

full source code here

Answer 1

Nên không có được một t7 cho fix f đầu tiên? Những cung cấp cho những hạn chế:

t7 = t2 
t0 = t1 -> t7 

Từ đó bạn sẽ có thể suy luận rằng t4 = t2 và sau đó t0 = (t2 -> t2) -> t2.