Personal tools

Notation: mathematics, programming languages

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
Line 8: Line 8:
   
 
<!-- combinatory logic and lambda-calculus -->
 
<!-- combinatory logic and lambda-calculus -->
  +
<tr>
  +
<td></td>
  +
<td>C</td>
  +
<td>flip</td>
  +
<td></td>
  +
</tr>
 
<tr>
 
<tr>
 
<td></td>
 
<td></td>

Revision as of 14:57, 15 May 2010

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