Each element of a list pattern matches the corresponding element of a list value.
When a list pattern [
P0
,
… ,
Pn
]
is matched against a list type List[
T
]
,
each Pi
is matched against the type T
,
producing typing contexts Γi. The typing context
produced by the whole match is the union of the contexts Γi.
{- Insertion Sort -} def insert(x, []) = [x] def insert(x, y:ys) = if (x <: y) then x:y:ys else y:insert(x,ys) def sort([]) = [] def sort([x]) = [x] def sort([x,y]) = if (x <: y) then [x,y] else [y,x] def sort(x:xs) = insert(x, sort(xs)) sort([3, 1, 4, 1, 5, 9]) {- OUTPUT: [1, 1, 3, 4, 5, 9] -}