TypeLits or Singletons: Promoting an `Integer` to `KnownNat` (`Nat`) at Runtime

Question

I've found two ways to promote an Integer to a Nat (or KnownNat, I don't get the distintion yet) at runtime, either using TypeLits and Proxy (Data.Proxy and GHC.TypeLits), or Singletons (Data.Singletons). In the code below you can see how each of the two approaches is used:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NoImplicitPrelude #-}

module Main where

import Prelude hiding (replicate)
import Data.Proxy (Proxy(Proxy))
import Data.Monoid ((<>))
import Data.Singletons (SomeSing(..), toSing)
import GHC.TypeLits
import Data.Singletons.TypeLits
import Data.Vector.Sized (Vector, replicate)

main :: IO ()
main = playingWithTypes 8

playingWithTypes :: Integer -> IO ()
playingWithTypes nn = do

  case someNatVal nn of
    Just (SomeNat (proxy :: Proxy n)) -> do
--      let (num :: Integer) = natVal proxy
--      putStrLn $ "Some num: " <> show num
      putStrLn $ "Some vector: " <> show (replicate 5 :: Vector n Int)
    Nothing -> putStrLn "There's no number, the integer was not a natural number"

  case (toSing nn :: SomeSing Nat) of
    SomeSing (SNat :: Sing n) -> do
--      let (num :: Integer) = natVal (Proxy :: Proxy n)
--      putStrLn $ "Some num: " <> show num
      putStrLn $ "Some vector: " <> show (replicate 5 :: Vector n Int)

The documentation for TypeLits indicates that it shouldn't be used by developers, but Singletons don't capture the case in which the given Integer is not a natural number (i.e., running playingWithTypes 8 runs without errors, but playingWithTypes (-2) fails when we try to create a Singleton from the non-natural number).

So, what is the "standard" way to promote an Integer to a Nat? Or what is the best approach to promote, using TypeLits and Proxy, or Singletons?

Answer 1

Nat (or KnownNat, I don't get the distintion yet)

Nat is the kind of type-level natural numbers. It has no term-level inhabitants. The idea is that GHC promotes any natural number into the type-level, and gives it kind Nat.

KnownNat is a constraint, on something of kind Nat, whose implementation witnesses how to convert the thing of kind Nat to a term-level Integer. GHC automagically creates instances of KnownNat for all type-level inhabitants of the kind Nat¹.

That said, even if every n :: Nat (read type n of kind Nat) has a KnownNat instance on it¹, you still need to write out the constraint.

I've found two ways to promote an Integer to a Nat

Have you really? At the end of the day, Nat in today's GHC is simply magical. singletons taps into that same magic. Under the hood, it uses someNatVal.

So, what is the "standard" way to promote an Integer to a Nat? Or what is the best approach to promote, using GHC.TypeLits and Proxy, or singletons?

There is no standard way. My take is: use singletons when you can afford its dependency footprint and GHC.TypeLits otherwise. The advantage of singletons is that the SingI type class makes it convenient to do induction based analysis while still also relying on GHC's special Nat type.

---

¹ As pointed out in the comments, not every inhabitant of the Nat kind has a KnownNat instance. For example, Any Nat :: Nat where Any is the one from GHC.Exts. Only the inhabitants 0, 1, 2, ... have KnownNat instances.