Personal tools

Notation: mathematics, programming languages

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
 
(2 intermediate revisions by one user not shown)
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>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>
 
<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 165:
 
<!-- list -->
 
<!-- list -->
 
<tr>
 
<tr>
<td>construction of a list from elements</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 177:
 
</tr>
 
</tr>
 
<tr>
 
<tr>
<td>construction of a list from a head and a tail</td>
+
<td>constructing a list from a head and a tail</td>
 
<td></td>
 
<td></td>
 
<td>x : xs</td>
 
<td>x : xs</td>

Latest revision as of 10:52, 24 May 2010

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