How to read this strange type signature foo :: Sing n -> (KnownNat n => r) -> r

Question

In the singletons package the function withKnownNat has the following strange type signature:

withKnownNat :: Sing n -> (KnownNat n => r) -> r.

The KnownNat n => context is not after the :: (hasType) symbol, but in the second function argument: -> (KnownNat n => r) ->.

How do I read this signature? What does it exactly mean? Where is it documented?

Answer 1

The difference between these two signatures:

withKnownNat :: Sing n -> (KnownNat n => r) -> r
withKnownNat' :: KnownNat n => Sing n -> r -> r

is in who is required to provide evidence that the constraint KnownNat n holds.

The hypothetical version with the constraint up front ("after the :: (hasType) symbol") requires the caller of withKnownNat' to be able to prove KnownNat n in order to invoke the function. That type signature can be read as something like "if you can prove KnownNat n, and give me both a Sing n and an r, I will give you back an r".

That's not particularly useful, as it could be implemented by simply ignoring the KnownNat n constraint and the Sing n argument and just returning the r its given. And without knowing what r is it couldn't really do much else to return an r; it could possibly do some operations with n and raise an error under some conditions, or do some nasty hacking with unsafe functions internally, but that's about it.

In the actual version, it's not the whole withKnownNat function that is under the KnownNat n constraint, but rather one of its arguments has that constraint. This means the caller of withKnownNat doesn't have to be able to prove KnownNat n; instead the caller can pass an argument that needs a proof of KnownNat n. As an argument¹ to a function the type KnownNat n => r can be read as "a value that is of type r under the assumption that KnownNat n holds". So the whole signature can be read as something like "if you give me both (1) a Sing n and (2) a value that is of type r under the assumption that KnownNat n holds, then I will give you a value of type r".

We can see that this is much more useful just from the type. Since it's polymorphic in r, the only way withKnownNat could get an r is from the KnownNat n => r we gave it. It can only actually use the KnownNat n => r value as a value of type r to return to us if it can prove KnownNat n. So basically this type for withKnownNat amounts to a promise that whenever we have a Sing n, we can also use anything that needs KnownNat n for the same n; withKnownNat is just what we have to call to convert one into the other.

---

¹ It means the same thing as a return value of a function as well, but it turns out that getting a return value that needs a constraint works out to exactly the same thing as if the whole function needed the constraint, so GHC always converts types like arg -> (constraints => result) to just constraints => args -> result.

Answer 2

KnownNat n is basically just a way of saying “there's a specific number” associated to n (it “is” the number n). So if you have a constraint KnownNat n => ... to anything, it's equivalent to passing in one specific number.

withKnownNat' :: Sing n -> (Integer -> r) -> r

That in turn is nothing else but a CPS way of writing

natVal :: Sing n -> Integer

...which is essentially a specific instantiation of the actual

natVal :: KnownNat n => proxy n -> Integer

except that the Sing has the typeclass constraint baked-in.