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.) |
m (Minor changes to formatting and grammar) |
||
| Line 1: | Line 1: | ||
An expression is in weak head normal form (WHNF), 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 <code>True</code>, <code>Just (square 42)</code> or <code>(:) 1</code>. |
| − | * 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 <code>(+) 2</code> or <code>sqrt</code>. |
| − | * or a lambda abstraction \x -> expression. |
+ | * or a lambda abstraction <code>\x -> expression</code>. |
| − | Note that the arguments do not themselves have to be fully evaluated for an expression to be in weak head normal form; thus, while |
+ | Note that the arguments do not themselves have to be fully evaluated for an expression to be in weak head normal form; thus, while <code>square 42</code> can be reduced to <code>42 * 42</code> (which can itself be reduced to a normal form of <code>1764</code>), <code>Just (square 42)</code> is in WHNF without further evaluation. Similarly, <code>(+) (2 * 3 * 4)</code> is in WHNF, even though <code>2 * 3 * 4</code> could be reduced to the normal form <code>24</code>. |
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. |
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 |
+ | 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 == |
||
Latest revision as of 22:16, 5 April 2021
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
(+) 2orsqrt. - 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 in WHNF without further evaluation. Similarly, (+) (2 * 3 * 4) is in 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.