Notation: mathematics, programming languages
Jump to navigation
Jump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
| meaning | mathematics | Haskell | Coq |
|---|---|---|---|
| C | flip | ||
| 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 | ⇒ | => | => |