From Nat to SNat (singleton Nat)

fromNat.hs

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs          #-}
{-# LANGUAGE RankNTypes     #-}
module SNat where

-- Disclaimer: my knowledge in Haskell is very limited and this may not be 100% accurate.
--
-- **All credit to** https://github.com/i-am-tom/haskell-exercises from Tom Harding.
-- Also, shoutout to the book "Thinking with Types" from Sandy Maguire which explains this in detail.

data Nat = Z | S Nat
  deriving Eq

instance Show Nat where
  show = show . go 0
    where
      go acc Z = acc
      go acc (S n) = go (acc + 1) n

data SNat (n :: Nat) where
  SZ :: SNat 'Z
  SS :: SNat n -> SNat ('S n)

toNat :: SNat n -> Nat
toNat SZ = Z
toNat (SS sn) = S (toNat sn)

-- This direction is tricky. Because we don't know n (it can be a runtime value)
fromNat :: (forall n. SNat n -> r) -> Nat -> r
fromNat f nat = f (fromNat' nat)
  where
    fromNat' :: Nat -> SNat n
    fromNat' Z = SZ
    fromNat' (S nat) = SS (fromNat' nat)
-- ^^^^^^^^^^^^^^ Compilation error

-- It will fail because n is "existential" (from the compiler POV).
-- n can never be defined outisde the rank-2 scope.

fromNat :: (forall n. SNat n -> r) -> Nat -> r
fromNat f Z = f SZ
fromNat f (S n) = fromNat (\some -> f (SS some)) n== x@!

testIso x = fromNat ((== x) . toNat) x
-- >>> let nat = S (S ( S( S Z)))
-- >>> testIso nat

-- A more compeling example

data Vector (n :: Nat) (a :: Type) where
  VNil  :: Vector 'Z a
  VCons :: a -> Vector n a -> Vector ('S n) a

vlength :: forall n. Vector n a -> SNat n
vlength VNil = SZ
vlength (VCons _ v) = SS (vlength v)

-- This is similar to fromNat, we don't know the length of the vector
-- when we filter it because the compiler can't statically know which
-- elements are going to pass the predicate*
filterV :: (forall n. Vector n a -> r) -> (a -> Bool) -> Vector n a -> r
filterV f p VNil = f VNil
filterV f p (VCons a v) = filterV (\v' -> if p a then f (VCons a v') else f v') p v

-- >>> let v = VCons 1 (VCons 2 ( VCons 3 VNil))

-- Although we are running it forall n, the following fails:
--
-- >>> filterV (vlength) (< 2) v
--
--    • Couldn't match type ‘r’ with ‘SNat n1’
--        because type variable ‘n1’ would escape its scope
--
-- As I mentioned before, n can't scape the rank2 scope because it has been "existentialized"
-- from the compiler POV.

-- toNat removes the dependency on the forall n.
-- So we can finally know the length of the vector as it was a regular list.
--
-- >>> filterV (toNat . vlength) (< 2) v
-- 1