Difference between revisions of "Notation: mathematics, programming languages"
From HaskellWiki
Line 8:  Line 8:  
<! combinatory logic and lambdacalculus > 
<! combinatory logic and lambdacalculus > 

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