refutable

In lazy functional languages, a refutable pattern is one which

may fail to match. An expression being matched against a

refutable pattern is first evaluated to head normal form

(which may fail to terminate) and then the top-level

constructor of the result is compared with that of the

pattern. If they are the same then any arguments are matched

against the pattern's arguments otherwise the match fails.

An irrefutable pattern is one which always matches. An

attempt to evaluate any variable in the pattern forces the

pattern to be matched as though it were refutable which may

fail to match (resulting in an error) or fail to terminate.

Patterns in Haskell are normally refutable but may be made

irrefutable by prefixing them with a tilde (~). For example,

( (x,y) -@# 1) undefined ==@# undefined

( ~(x,y) -@# 1) undefined ==@# 1

Patterns in Miranda are refutable, except for tuples which are

irrefutable. Thus

g [x] = 2

g undefined ==@# undefined

f (x,y) = 1

f undefined ==@# 1

Pattern bindings in local definitions are irrefutable in both

languages:

h = 1 where [x] = undefined ==@# 1

Irrefutable patterns can be used to simulate unlifted products

because they effectively ignore the top-level constructor of

the expression being matched and consider only its components.