← back

Polymorphism lecture, in-class exercise C

1 November 2015

Question

I'm trying to understand the types for this function:

let rec msort xs =
 match xs with
 | [] -> []
 | x::xs’ ->
   let ys,zs = split xs in
     merge (msort ys) (msort zs)

Based on the previous two slides, we determined:

split = ('a list) -> ('a list * 'a list) and

merge = ('a list) -> ('a list) -> ('a list).

I understand the types for both split and merge, but I'm confused as to why the type for msort is ('a list) -> ('b list). Why not ('a list) -> ('a list), since both split and merge are known to give us lists of type 'a ?

If someone could try to break down the notes on the slide for me I'd appreciate it.

Answer

Let's look at this line by line:

let rec msort xs =

msort is a function, with type

Tmsort : Txs -> Tbody

 match xs with
 | [] -> []

xs must be a list (of something), and furthermore, msort returns a list. There are no guarantees that msort returns a list of the same type as xs because the empty list inhabits the set of all possible list types (∀a,[]∈alist). So the most general type for Tbody is a list of a fresh parameter. The use of [] as a return value is why OCaml infers 'a list -> 'b list as the most general type of msort.

Txs : 'a list
Tbody : 'b list
Tmsort : 'a list -> 'b list

Recursive case:

| x::xs’ ->
 let ys,zs = split xs in
 merge (msort ys) (msort zs)

we know that

split : 'a list -> ('a list * 'a list)
merge : 'a list -> 'a list -> 'a list

So ys and zs are both 'a lists (by Txs)

merge is called on (msort ys) and (msort zs). By Tmsort we know that

(msort ys) : 'b list
(msort zs) : 'b list

Alpha-rename 'a list to 'b list for the merge equation. The recursive case typechecks with the inferred return type of msort's base case.

Check in Ocaml:

let rec msort xs =
  match xs with
  | [] -> []
  | x::xs' ->
     let ys,zs = split xs in
       merge (msort ys) (msort zs);;
val msort : 'a list -> 'b list = <fun>

Whereas if you defined it like this:

let rec msort xs =
  match xs with
  | [] -> xs
  | x::xs' ->
     let ys,zs = split xs in
       merge (msort ys) (msort zs);;
val msort : 'a list -> 'a list = <fun>

You get the "expected" type of msort.