View source for Notation: mathematics, programming languages

<table border="1">
<tr>
	<th>meaning</th>
	<th>mathematics</th>
	<th>Haskell</th>
	<th>Coq</th>
</tr>

<!-- combinatory logic and lambda-calculus -->
<tr>
	<td></td>
	<td>C</td>
	<td>flip</td>
	<td></td>
</tr>
<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>fixed point combinators</td>
	<td>Y</td>
	<td>fix</td>
	<td>fix</td>
</tr>
<tr>
	<td>composition of functions</td>
	<td><div>∘</div><div>B (combinator)</div></td>
	<td>.</td>
	<td></td>
</tr>
<tr>
	<td>λ-abstraction</td>
	<td><div>λxy (λ-calculus)</div><div>λx.y (λ-calculus)</div><div>↦</div></td>
	<td>\ x -> y</td>
	<td>fun x => y</td>
</tr>

<!-- predicate -->
<tr>
	<td>not equal</td>
	<td>≠</td>
	<td>/=</td>
	<td>&lt;&gt; (Prop)</td>
</tr>
<tr>
	<td>equal</td>
	<td>=</td>
	<td>==</td>
	<td>= (Prop)</td>
</tr>
<tr>
	<td>lower or equal</td>
	<td>≤</td>
	<td>&lt;=</td>
	<td>&lt;=</td>
</tr>
<tr>
	<td>greater or equal</td>
	<td>≥</td>
	<td>>=</td>
	<td>>=</td>
</tr>

<!-- type -->
<tr>
	<td>is of type</td>
	<td>name : type</td>
	<td>name :: type</td>
	<td>name : type</td>
</tr>
<tr>
	<td>logical negation</td>
	<td>¬</td>
	<td>not</td>
	<td>~ (Prop)</td>
</tr>
<tr>
	<td>material implication</td>
	<td><div>→</div><div>⊃</div></td>
	<td></td>
	<td>-&gt;</td>
</tr>
<tr>
	<td>function type constructor</td>
	<td>→</td>
	<td>-&gt;</td>
	<td>-&gt;</td>
</tr>
<tr>
	<td>categorical product</td>
	<td>a × b</td>
	<td>(a, b)</td>
	<td>a * b</td>
</tr>
<tr>
	<td>conjunction</td>
	<td>∧</td>
	<td>&amp;&amp;</td>
	<td>/\ (Prop)</td>
</tr>
<tr>
	<td>categorical sum</td>
	<td>+</td>
	<td>Either</td>
	<td>+ (Type)</td>
</tr>
<tr>
	<td>disjunction</td>
	<td>∨</td>
	<td>||</td>
	<td>\/ (Prop)</td>
</tr>
<tr>
	<td>verum</td>
	<td>⊤</td>
	<td>True</td>
	<td>True (Prop)</td>
</tr>
<tr>
	<td>falsum, absurd, contradiction</td>
	<td>⊥</td>
	<td>False</td>
	<td>False (Prop)</td>
</tr>
<tr>
	<td>empty set</td>
	<td>∅</td>
	<td></td>
	<td>Empty_set</td>
</tr>
<tr>
	<td>singleton set</td>
	<td><div>{*}</div><div>{∙}</div></td>
	<td>()</td>
	<td>unit</td>
</tr>
<tr>
	<td>inhabitant of the singleton set</td>
	<td><div>*</div><div>∙</div></td>
	<td>()</td>
	<td>tt</td>
</tr>
<tr>
	<td>universal quantification</td>
	<td>∀</td>
	<td>forall</td>
	<td>forall</td>
</tr>
<tr>
	<td>existential quantification</td>
	<td>∃</td>
	<td>forall (before data constructor)</td>
	<td><div>exists</div><div>ex</div><div>sig</div><div>sigT</div></td>
</tr>

<!-- list -->
<tr>
	<td>constructing a list from elements</td>
	<td>⟨x, y, z⟩</td>
	<td>[x, y, z]</td>
	<td></td>
</tr>
<tr>
	<td>empty list</td>
	<td></td>
	<td>[]</td>
	<td>nil</td>
</tr>
<tr>
	<td>constructing a list from a head and a tail</td>
	<td></td>
	<td>x : xs</td>
	<td>x :: xs</td>
</tr>
<tr>
	<td>concatenation of lists</td>
	<td>⧺</td>
	<td>++</td>
	<td>app</td>
</tr>

<!-- algebraic data type -->
<tr>
	<td>tuple constructor</td>
	<td>⟨x, y, z⟩</td>
	<td>(x, y, z)</td>
	<td>(x, y, z)</td>
</tr>
<tr>
	<td>natural numbers</td>
	<td>ℕ</td>
	<td></td>
	<td>nat</td>
</tr>

<!-- category theory -->
<tr>
	<td>covariant Hom functor</td>
	<td>Hom(a,−)</td>
	<td>Reader a</td>
	<td></td>
</tr>
<tr>
	<td>contravariant Hom functor</td>
	<td>Hom(−,a)</td>
	<td>Writer a</td>
	<td></td>
</tr>
<tr>
	<td>functor</td>
	<td></td>
	<td>Functor</td>
	<td></td>
</tr>
<tr>
	<td>lax monoidal functor</td>
	<td></td>
	<td>Applicative</td>
	<td></td>
</tr>
<tr>
	<td>monad</td>
	<td></td>
	<td>Monad</td>
	<td></td>
</tr>
<tr>
	<td>neutral element of a monad</td>
	<td>η</td>
	<td>return</td>
	<td></td>
</tr>
<tr>
	<td>binary operation of a monad</td>
	<td>μ</td>
	<td>join</td>
	<td></td>
</tr>

<!-- notation -->
<tr>
	<td>double arrow</td>
	<td>⇒</td>
	<td>=&gt;</td>
	<td>=&gt;</td>
</tr>
</table>

[[Category:Mathematics]]