[Haskell-cafe] Type-Level Programming

[Andrew Coppin]

Alexander Solla wrote:
>
> 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.

I have literally no idea what you just said.

It's like, I have C. J. Date on the shelf, and the whole chapter on the 
Relational Calculus just made absolutely no sense to me because I don't 
understand the vocabulary.