Difference between revisions of "Notation: mathematics, programming languages"
From HaskellWiki
Line 5:  Line 5:  
<th>Haskell</th> 
<th>Haskell</th> 

<th>Coq</th> 
<th>Coq</th> 

+  </tr> 

+  
+  <! combinatory logic and lambdacalculus > 

+  <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>fixpoint combinator</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 159:  
<! list > 
<! list > 

<tr> 
<tr> 

−  <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 171:  
</tr> 
</tr> 

<tr> 
<tr> 

−  <td> 
+  <td>constructing a list from a head and a tail</td> 
<td></td> 
<td></td> 

<td>x : xs</td> 
<td>x : xs</td> 
Revision as of 19:54, 14 May 2010
meaning  mathematics  Haskell  Coq 

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