CSC448: Type Checking Revisited: Hindley-Milner Type Inference: Implementation I [119/133]

Not a full implementation because it generates constraints but does not solve them.

See the file:hm directory.

Expressions (file:Exp.java) and types (file:Type.java) are represented in the usual way.

A type scheme (file:TypeScheme.java) is a list of bound type variables and a type.

A constraint (file:Constraint.java) represents equality between a pair of types.

The work is performed by file:Infer.java.

The test file (file:Test.java) infers a type for the take function.

Compile and run with:

C:\l\csc448\examples\hm>javac -classpath . *.java
C:\l\csc448\examples\hm>java -classpath . Test
        

Output is:

(fun f i => (fun g xs => (if (is_zero i) then [] else ((head xs)::((f ((add i) -1)) (tail xs))))))

Inferred type is: ('A0 -> 'A1)

Constraints:
('A2 -> 'A3) = 'A1
('A6 list) = 'A3
('A6 list) = 'A20
'A5 = boolean
('A9 list) = 'A20
'A18 = 'A19
'A15 = ('A19 -> 'A20)
'A2 = 'A17
('A16 list) = 'A18
('A16 list) = 'A17
'A13 = 'A14
'A1 = 'A15
'A0 = 'A14
'A12 = int
'A11 = ('A12 -> 'A13)
'A0 = 'A10
(int -> int) = 'A11
'A10 = int
'A2 = 'A8
'A7 = 'A9
('A7 list) = 'A8
'A0 = 'A4
'A5 = boolean
'A4 = int