[Haskell-cafe] Type-Level Programming

[Alexander Solla]

On Jun 26, 2010, at 4:33 AM, Andrew Coppin wrote:

> It's a bit like trying to learn Prolog from somebody who thinks that  
> the difference between first-order and second-order logic is somehow  
> "common knowledge".


A first order logic quantifies over values, and a second order logic  
quantifies over values and sets of values (i.e., types, predicates,  
etc).  The latter lets you express things like "For every property P,  
P x".  Notice that this expression "is equivalent" to Haskell's bottom  
type "a".  Indeed, Haskell is a weak second-order language.  Haskell's  
language of values, functions, and function application is a first- 
order language.