Notation: mathematics, programming languages
Jump to navigation
Jump to search
| meaning | mathematics | Haskell | Coq |
|---|---|---|---|
| C | flip | ||
| K | const | ||
| identity | I | id ($) |
|
| fixed point combinators | 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 | ⇒ | => | => |