In GHC.TypeLits what is someNatVal good for (which we can't accomplish with natVal)?

Question

I'm trying to understand GHC.TypeLits, and specifically someNatVal. I understand the way it's used in this blog post here, but as mentioned the same example could have been implemented using natVal, like:

isLength :: forall len a. KnownNat len => Integer -> List len a -> Bool
isLength n _ = n == natVal (Proxy :: Proxy len)

Are there any uses of someNatVal that can't be rewritten with natVal?

Answer 1

SomeNat is existentially quantified:

data SomeNat = forall n. KnownNat n => SomeNat (Proxy n)

which reads like SomeNat contains, well, "some n :: Nat". Proxy is a singleton that allows to lift that n to the type-level to satisfy the type system — in a dependently typed language we need such construction very rarely. We can define SomeNat in more explicit way using GADTs:

data SomeNat where
    SomeNat :: forall n. KnownNat n => Proxy n -> SomeNat

So SomeNat contains a Nat, which is not known statically.

Then

someNatVal :: Integer -> Maybe SomeNat

reads like "someNatVal receives an Integer and Maybe returns a hiden Nat". We can't return a KnownNat, because Known means "known at the type level", but there is nothing we know about an arbitrary Integer at the type level.

The inverse (modulo SomeNat wrapper and a proxy instead of the Proxy) of someNatVal is

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

Reads like "natVal receives something that have a Nat in its type and returns that Nat converted to Integer".

Existentially quantified data types are usually used for wrapping runtime values. Say you want to read a Vec (a list with statically known length) from STDIN, but how would you statically compute the length of input? There is no way. So you wrap a list, that you've read, in the corresponding existentially quantified data type, thus saying "I don't know the length, but there exists one".

However it's overkill in many cases. To do something with existentially quantified data type you need to be general: e.g. if you need to find the sum of elements of a SomeVec you have to define sumVec for Vecs with arbitrary length. Then you unwrap the SomeVec and apply sumVec, thus saying "I don't know the length of a wrapped Vec, but sumVec doesn't care". But instead of this wrapping-unwrapping you can directly use CPS.

However because of this generality you'll need to enable ImpredicativeTypes to be able to define, say, a list with such continuations. In that case a list with existentially quantified data is a common pattern that allows to get round ImpredicativeTypes.

As to your example, with properly defined Nats, a version that compares Nats is lazier, than a version that compares Integers.

Answer 2

The main use of someNatVal is using a value at run time as if it was a type that wasn't known at compile time.

My answer to Can I have an unknown KnownNat? provides a really dumb example. There are a million better ways to write a program that does the same thing as that one. But it shows what someNatVal does. It's essentially a function from value to type - with an existential limiting the scope of that type to places where it's not statically known.