Type Systems: Sample Type Reconstruction
Is ((? f :? . (? x:? . (f (f x)))) (? x:? . x)) typable? What is its principal type?
Tree1: f : ?, x:? |- f :?, f :?, x:? |- x:? [? = ?1 ? ?2 , ? =?1 ]
f :?1 ? ?2, x:?1 |- (f x): ?2
Tree2: f : ?1 ? ?2, x: ?1 |- f : ?1 ? ?2, Tree1 [?2 = ?1 ]
f : ?1 ? ?1, x: ?1 |- (f (f x)): ?1
f : ?1 ? ?1 |- (? x:?1 . (f (f x))) : ?1 ? ?1
? |- ((? f :?1 ? ?1. (? x:?1 . (f (f x)))) : (?1 ? ?1) ? (?1 ? ?1)
? |- (? x: ?. x)) : ? ? ?
Tree4: Tree2, Tree3 [? = ?1]
? |- ((? f : ?1 ? ?1. (? x: ?1 . (f (f x)))) (? x: ?1 . x)) : ?1 ? ?1