# Notation: mathematics, programming languages

From HaskellWiki

meaning | mathematics | Haskell | Coq |
---|---|---|---|

composition of functions | ∘ | . | |

λ-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 |

construction of a list from elements | ⟨x, y, z⟩ | [x, y, z] | |

empty list | [] | nil | |

construction of 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 | ⇒ | => | => |