Version 6 (modified by 5 years ago) (diff) | ,
---|

The only "magic" thing about `GHC.TypeLits`

are the instances of `SingI`

. The rest is implemented like this:

newtype Sing n = Sing (SingRep n) type family SingRep a type instance SingRep (n :: Nat) = Integer type instance SingRep (n :: Symbol) = String fromSing :: Sing n -> SingRep n fromSing (Sing n) = n

So, now we just need instances like these:

instance SingI 0 where sing = Sing 0 instance SingI 1 where sing = Sing 1 instance SingI "hello" where sing = Sing "hello" ...

Because we cannot generate this infinite family of instances, we have
some code in GHC which can solve `SingI`

predicates on the fly.

The "proof" (aka "dictionary") for `SingI n`

is just the number (or string) `n`

. This is OK because:

- GHC uses a
`newtype`

to represent the dictionaries for classes that have just a single method and no super-classes.`SingI`

is just such a class. `Sing`

is already a`newtype`

for`Integer`

or`String`

, depending on the kind of its parameter.

Therefore, the dictionaries for class `SingI`

are just integers or strings, depending on the kind of the parameter.