[Haskell-cafe] Type-Level Programming

[Alexander Solla]

On Jun 26, 2010, at 11:21 AM, Andrew Coppin wrote:

>> 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.

Let's break it down then.  A language is a set of "terms" or  
"expressions", together with rules for putting terms together  
(resulting in "sentences", in the logic vocabulary).  A "logic" is a  
language with "rules of inference" that let you transform sets of  
sentences into new sentences.

Quantification is a tricky thing to describe.  In short, if a language  
can "quantify over" something, it means that you can have variables  
"of that kind".  So, Haskell can quantify over integers, since we can  
have variables like "x :: Integer".  More generally, Haskell's run- 
time language quantifies over "values".

 From this point of view, Haskell is TWO languages that interact  
nicely (or rather, a second-order language).  First, there is the  
"term-level" run-time language.  This is the stuff that gets evaluated  
when you actually run a program.  It can quantify over values and  
functions.  And we can express function application (a rule of  
inference to combine a function and a value, resulting in a new value).

Second, there is the type language, which relies on specific keywords:

data, class, instance, newtype, type, (::)

Using these keywords, we can quantify over types.  That is, the  
constructs they enable take types as variables.

However, notice that a type is "really" a collection of values.  For  
example, as the Gentle Introduction to Haskell says, we should think  
of the type Integer as being:

data Integer = 0 | 1 | -1 | 2 | -2 | ...

despite the fact that this isn't how it's really implemented.  The  
Integer type is "just" an enumeration of the integers.


Putting this all together and generalizing a bit, a second-order  
language is a language with two distinct, unmixable kinds variables,  
where one kind of variable represents a collection of things that can  
fill in the other kind of variable.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100626/c3a36033/attachment.html