Reasoning about type inference

	(*
	f: T1 -> T2 [must be a function; all functions take 1 arg]
	x: T1
	y: T3
	z: T4
	T1 = T3 * T4 [else pattern match does not type-check]
	T3 = int [abs has type int -> int]
	T4 = int [because we added z to an int]
	So T1 = int * int
	So (abs y) + z: int, so let-expression: int, so body: int
	T2 = int
	f: int * int -> int
	*)
	fun f x =
	let val (y,z) = x in
	(abs y) + z
	end

view raw gistfile1.sml hosted with ❤ by GitHub

	(*
	sum: T1 -> T2
	xs: T1
	x: T3
	xs': T3 list [pattern match a T1]
	T1 = T3 list
	T2 = int [because 0 might be returned]
	T3 = int [because x:T3 and we add x to something]
	from T3 = int, we know T1 = int list
	from that and T2=int, we know f: int list -> int
	*)
	fun sum xs =
	case xs of
	[] => 0
	| x::xs' => x + (sum xs')

view raw gistfile1.sml hosted with ❤ by GitHub

	(*
	length: T1 -> T2
	xs: T1
	x: T3
	xs': T3 list
	T1 = T3 list
	T2 = int
	There are no more constraints, therefore
	T3 list -> int
	'a list -> int
	*)
	fun length xs =
	case xs of
	[] => 0
	| x::xs' => 1 + (length xs')

view raw gistfile1.sml hosted with ❤ by GitHub

	(*
	f: T1 * T2 * T3 -> T4
	x: T1
	y: T2
	z: T3
	T4 = T1 * T2 * T3
	T4 = T2 * T1 * T3
	only way those can both be true is if T1 = T2
	put it all together: f: T1 * T1 * T3 -> T1 * T1 * T3
	'a * 'a * 'b -> 'a * 'a * 'b
	*)
	fun f (x,y,z) =
	if true
	then (x,y,z)
	else (y,x,z)

view raw gistfile1.sml hosted with ❤ by GitHub

	(*
	compose: T1 * T2 -> T3
	f: T1
	g: T2
	x: T4
	body being a functoin has type T3 = T4 -> T5
	from g being passed x, T2 = T4 -> T6 for some T6
	from f being passed the result of g, T1 = T6 -> T7 for some T7
	from call to f being the body of anonmymous function T7 = T5
	put it all together: T1 = T6 -> T5, T2 = T4 -> T6, T3 = T4 -> T5
	(T6 -> T5) * (T4 -> T6) -> (T4 -> T5)
	('a -> 'b) * ('c -> 'a) -> ('c -> 'b)
	*)
	fun compose (f,g) = fn x => f (g x)

view raw gistfile1.sml hosted with ❤ by GitHub