Difference between revisions of "Weak head normal form"
(Add a note about strict fields and note (inspired by Stack Overflow question) that the difference between builtin and defined functions is immaterial.) |
|||
| (One intermediate revision by one other user not shown) | |||
| Line 1: | Line 1: | ||
| − | An expression is in weak head normal form, if it is either: |
+ | An expression is in weak head normal form (WHNF), if it is either: |
* a constructor (eventually applied to arguments) like True, Just (square 42) or (:) 1 |
* a constructor (eventually applied to arguments) like True, Just (square 42) or (:) 1 |
||
* a built-in function applied to too few arguments (perhaps none) like (+) 2 or sqrt. |
* a built-in function applied to too few arguments (perhaps none) like (+) 2 or sqrt. |
||
| Line 5: | Line 5: | ||
Note that the arguments do not themselves have to be fully evaluated for an expression to be in weak head normal form; thus, while (square 42) can be reduced to (42 * 42), which can itself be reduced to a normal form of 1764, Just (square 42) is WHNF without further evaluation. Similarly, (+) (2 * 3 * 4) is WHNF, even though (2 * 3 * 4) could be reduced to the normal form 24. |
Note that the arguments do not themselves have to be fully evaluated for an expression to be in weak head normal form; thus, while (square 42) can be reduced to (42 * 42), which can itself be reduced to a normal form of 1764, Just (square 42) is WHNF without further evaluation. Similarly, (+) (2 * 3 * 4) is WHNF, even though (2 * 3 * 4) could be reduced to the normal form 24. |
||
| + | |||
| + | An exception is the case of a fully applied constructor for a data type with some fields declared as strict; the arguments for these fields then also need to be in WHNF. |
||
| + | |||
| + | The above definition might seem to treat built-in functions differently from functions defined via lambda abstraction. However, the distinction does not matter to semantics. If a lambda abstraction is applied to "too few arguments", then evaluating the application just means substituting arguments for some of the lambda abstraction's variables, which always halts with the result a now unapplied lambda abstraction. |
||
== See also == |
== See also == |
||
Revision as of 01:34, 28 June 2014
An expression is in weak head normal form (WHNF), if it is either:
- a constructor (eventually applied to arguments) like True, Just (square 42) or (:) 1
- a built-in function applied to too few arguments (perhaps none) like (+) 2 or sqrt.
- or a lambda abstraction \x -> expression.
Note that the arguments do not themselves have to be fully evaluated for an expression to be in weak head normal form; thus, while (square 42) can be reduced to (42 * 42), which can itself be reduced to a normal form of 1764, Just (square 42) is WHNF without further evaluation. Similarly, (+) (2 * 3 * 4) is WHNF, even though (2 * 3 * 4) could be reduced to the normal form 24.
An exception is the case of a fully applied constructor for a data type with some fields declared as strict; the arguments for these fields then also need to be in WHNF.
The above definition might seem to treat built-in functions differently from functions defined via lambda abstraction. However, the distinction does not matter to semantics. If a lambda abstraction is applied to "too few arguments", then evaluating the application just means substituting arguments for some of the lambda abstraction's variables, which always halts with the result a now unapplied lambda abstraction.