[Haskell-cafe] Type-Level Programming

Alexander Solla ajs at 2piix.com
Sat Jun 26 13:33:30 EDT 2010

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.

More information about the Haskell-Cafe mailing list