Understanding `GHC.TypeLits`

Question

I'm trying to wrap my head around the GHC extensions KindSignatures and DataKinds. Looking at the Data.Modular package, I understand roughly that

newtype i `Mod` (n :: Nat) = Mod i deriving (Eq, Ord)

is sort of equivalent to declaring a c++ template <typename T, int N> (with the constructor taking only one argument of type T). However, looking at the GHC.TypeLits package, I don't understand most of what is happening. Any general explanation about this package would be helpful. Before this question gets flagged as off topic though, here are some specific sub-questions:

• a KnownNat class makes sense, with required function letting you extract the type variable from the type, but what does natVal do, and what is the proxy type variable?
• Where would you use someNatVal?
• Finally, what is SomeNat - how can a type level number be unknown? Isn't the whole point of a type level number that it is known at compile time?

Answer 1

This question is quite broad -- I'll address a few points, only.

The proxy type variable is just a type variable of kind * -> *, i.e. the kind of type contructors. Pragmatically, if you have a function

foo :: proxy a -> ...

you can pass to it values of type e.g. Maybe Int, choosing proxy = Maybe and a = Int. You can pass also values of type [] Char (also written as [Char]). Or, more commonly, a value of type Proxy Int, where Proxy is a data type defined as

data Proxy a = Proxy

i.e. a data type which does not carry any run-time information (there's a single value for it!), but which carries compile-time information (the phantom type variable a).

Assume N is a type of kind Nat -- a compile-time natural. We can write a function

bar :: N -> ...

but calling this would require us to build a value of type N -- which is immaterial. The purpose of type N is to carry compile-time information, only, and its run-time values are not things that we really want to use. In fact, N could have no values at all, except for bottom. We could call

bar (undefined :: N)

but this looks weird. Reading this, we must realize that bar is lazy in its first argument and that it will not cause divergence trying to use it. The problem is that the bar :: N -> ... type signature is misleading: it claims that the result may depend on the value of the argument of type N, when this is not really the case. Instead, if we use

baz :: Proxy N -> ...

the intent is clear -- there's only a single run-time value for that: Proxy :: Proxy N. It is equally clear that the N value is only present at compile time.

Sometimes, instead of using the specific Proxy N, the code is slightly generalized to

foo :: proxy N -> ...

which achieves the same goal, but permits also different Proxy types. (Personally, I'm not terribly thrilled by this generalization.)

Back to the question: natVal is a function which turns a compile-time only natural into a run-time value. I.e. it converts Proxy N into Int, returning just the constant.

You analogy with C++ templates might get closer if you used type template arguments to model compile time naturals. E.g.

template <typename N> struct S { using pred = N; };
struct Z {};

template <typename N> int natVal();
template <typename N> int natVal() { return 1 + natVal<typename N::pred>(); }
template <>           int natVal<Z>() { return 0; }

int main() {
    cout << natVal<S<S<Z>>>() << endl;  // outputs 2
    return 0;
}

Just pretend there are no public constructors for S and Z: their run-time values are unimportant, only their compile-time information matters.