[Haskell-cafe] Type-Level Programming
ajs at 2piix.com
Sat Jun 26 16:30:07 EDT 2010
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...
More information about the Haskell-Cafe