Difference between revisions of "Notation: mathematics, programming languages"
Jump to navigation
Jump to search
| Line 5: | Line 5: | ||
<th>Haskell</th> |
<th>Haskell</th> |
||
<th>Coq</th> |
<th>Coq</th> |
||
| + | </tr> |
||
| + | |||
| + | <!-- combinatory logic and lambda-calculus --> |
||
| + | <tr> |
||
| + | <td></td> |
||
| + | <td>K</td> |
||
| + | <td>const</td> |
||
| + | <td></td> |
||
| + | </tr> |
||
| + | <tr> |
||
| + | <td>identity</td> |
||
| + | <td>I</td> |
||
| + | <td><div>id</div><div>($)</div></td> |
||
| + | <td></td> |
||
| + | </tr> |
||
| + | <tr> |
||
| + | <td>fixpoint combinator</td> |
||
| + | <td>Y</td> |
||
| + | <td>fix</td> |
||
| + | <td>fix</td> |
||
</tr> |
</tr> |
||
<tr> |
<tr> |
||
<td>composition of functions</td> |
<td>composition of functions</td> |
||
| − | <td>∘</td> |
+ | <td><div>∘</div><div>B (combinator)</div></td> |
<td>.</td> |
<td>.</td> |
||
<td></td> |
<td></td> |
||
| Line 139: | Line 159: | ||
<!-- list --> |
<!-- list --> |
||
<tr> |
<tr> |
||
| − | <td> |
+ | <td>constructing a list from elements</td> |
<td>⟨x, y, z⟩</td> |
<td>⟨x, y, z⟩</td> |
||
<td>[x, y, z]</td> |
<td>[x, y, z]</td> |
||
| Line 151: | Line 171: | ||
</tr> |
</tr> |
||
<tr> |
<tr> |
||
| − | <td> |
+ | <td>constructing a list from a head and a tail</td> |
<td></td> |
<td></td> |
||
<td>x : xs</td> |
<td>x : xs</td> |
||
Revision as of 19:54, 14 May 2010
| meaning | mathematics | Haskell | Coq |
|---|---|---|---|
| K | const | ||
| identity | I | id ($) |
|
| fixpoint combinator | Y | fix | fix |
| composition of functions | ∘ B (combinator) |
. | |
| λ-abstraction | λxy (λ-calculus) λx.y (λ-calculus) ↦ |
\ x -> y | fun x => y |
| not equal | ≠ | /= | <> (Prop) |
| equal | = | == | = (Prop) |
| lower or equal | ≤ | <= | <= |
| greater or equal | ≥ | >= | >= |
| is of type | name : type | name :: type | name : type |
| logical negation | ¬ | not | ~ (Prop) |
| material implication | → ⊃ |
-> | |
| function type constructor | → | -> | -> |
| categorical product | a × b | (a, b) | a * b |
| conjunction | ∧ | && | /\ (Prop) |
| categorical sum | + | Either | + (Type) |
| disjunction | ∨ | || | \/ (Prop) |
| verum | ⊤ | True | True (Prop) |
| falsum, absurd, contradiction | ⊥ | False | False (Prop) |
| empty set | ∅ | Empty_set | |
| singleton set | {*} {∙} |
() | unit |
| inhabitant of the singleton set | * ∙ |
() | tt |
| universal quantification | ∀ | forall | forall |
| existential quantification | ∃ | forall (before data constructor) | exists ex sig sigT |
| constructing a list from elements | ⟨x, y, z⟩ | [x, y, z] | |
| empty list | [] | nil | |
| constructing a list from a head and a tail | x : xs | x :: xs | |
| concatenation of lists | ⧺ | ++ | app |
| tuple constructor | ⟨x, y, z⟩ | (x, y, z) | (x, y, z) |
| natural numbers | ℕ | nat | |
| covariant Hom functor | Hom(a,−) | Reader a | |
| contravariant Hom functor | Hom(−,a) | Writer a | |
| functor | Functor | ||
| lax monoidal functor | Applicative | ||
| monad | Monad | ||
| neutral element of a monad | η | return | |
| binary operation of a monad | μ | join | |
| double arrow | ⇒ | => | => |