Understanding `GHC.TypeLits`

Question

I am trying to wrap my head around the GHC KindSignatures and DataKinds . Looking at the Data.Modular package, I understand roughly what

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

is the equivalent of declaring a C ++ <typename T, int N> template (in this case, the constructor accepts only one argument of type T ). However, looking at the GHC.TypeLits package, I do not understand much of what is happening. Any general explanation for this package would be helpful. Before this question is marked as inactive, here are some specific questions:

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

Answer 1

This question is quite wide - I will consider only a few points.

A proxy type proxy is just a type variable * -> * , i.e. type type contructors. Pragmatically if you have a function

 foo :: proxy a -> ... 

you can pass it type values, for example. Maybe Int by choosing proxy = Maybe and a = Int . You can also pass values ​​like [] Char (also written as [Char] ). Or, most often, a value of type Proxy Int , where proxy is the data type defined as

 data Proxy a = Proxy 

i.e. a data type that does not carry any information about the runtime (there is one value for this!), but which contains compile-time information (a variable like phantom a ).

Suppose N is a type of type Nat — natural compilation time. We can write a function

 bar :: N -> ... 

but the challenge of this requires us to construct a value of type N - which is important. The goal of type N is to pass compile-time information only, and its run-time values ​​are not what we really want to use. In fact, N cannot have any values ​​except the bottom. We could call

 bar (undefined :: N) 

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

 baz :: Proxy N -> ... 

the goal is clear - there is only one runtime value for this: Proxy :: Proxy N It is also clear that the value N present only at compile time.

Sometimes, instead of using a special Proxy N code is slightly generalized to

 foo :: proxy N -> ... 

which achieves the same goal, but also allows various types of proxy . (Personally, I'm not terribly excited about this generalization.)

Back to the question: natVal is a function that turns compilation time only natural into a run-time value. That is, it converts Proxy N to Int , returning only a constant.

You could come close similarly to C ++ templates if you used type template arguments to simulate simulation time. For instance.

 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 that there are no common constructors for S and Z : their run-time values ​​are irrelevant, only compile-time information matters.