Type Systems: Sample Polymorphic Type Reconstruction
Claim: ? | (let length := (?x. (if (null? x) then 0 else (+ 1 (length (rest x))))) in (+ (length (cons 1 null)) (length (cons true null)))):int
Tree1: length: ?, x:?1 | null?:?-list?bool, length:?, x: ?1 | x:?1 [?1 = ?-list]
length:?, x:?-list | (null? x):bool
Tree2: length:?, x:?-list | rest: ?2-list??2-list, length:?, x:?-list | x:?-list [?2 = ?]
length:?, x:?-list | (rest x):?-list
length:?-list??2, x:?-list | (length (rest x)):?2 [? = ?-list??2]
length:?-list?int, x:?-list | (+ 1 length(rest x)):int [?2 = int]
Tree3: Tree1, length:?-list? int, x:?-list | 0:int, Tree2
length:?-list?int, x:?-list | if (null? x) then 0 else (+ 1 (length (rest x))))) in (+ (length (cons 1 null)) (length (cons true null)))):int
length:?-list?int | ?x. if (null? x) then 0 else (+ 1 (length (rest x))))) in (+ (length (cons 1 null)) (length (cons true null)))):?-list?int
length:?? .? -list?int | cons:?3??3-list??3-list, length:?? .? -list?int | 1:int, length:?? .? -list?int | null:?4-list [?3 = ?4 = int ]
length:?? .? -list?int | (cons 1 null):int-list
Tree5: length:?? .? -list?int | length: ?5 -list?int, Tree4 [?5 =int]
length:?? .? -list?int | (length (cons 1 null)): int
length:?? .? -list?int | cons:?6??6-list??6-list, length:?? .? -list?int | true:bool, length:?? .? -list?int | null: ?7 -list
length:?? .? -list?int | (cons true null):bool -list [?7 = ?6 = bool ]