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.
Nearby terms:
refreshable braille display « refreshable display «
refresh rate « refutable » regex » regexp »
Regina
|
