Example of promoting a value to a type using higher ranked types, continuation passing and GADTs

value-promotion.hs

{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE ScopedTypeVariables  #-}

module Main where

import Data.Proxy
import Data.Type.Equality

data Nat = Zero | Succ Nat


-- the regular way of promoting values using a continuation that accepts a type witness or proxy

promoteCPS :: forall r . (forall proxy (nat :: Nat) . proxy nat -> r) -> Int -> r
promoteCPS f = go (Proxy :: Proxy 'Zero) where
  go :: forall (nat :: Nat) . Proxy nat -> Int -> r
  go p 0 = f p
  go p i | i > 0 = go (Proxy :: Proxy ('Succ nat)) (i - 1)


-- Equivalent solution using GADTs instead of continuations

data SomeNat where
  SomeNat :: proxy (n :: Nat) -> SomeNat

promoteExistential :: Int -> SomeNat
promoteExistential = go (Proxy :: Proxy 'Zero) where
  go :: forall (nat :: Nat) . Proxy nat -> Int -> SomeNat
  go v 0 = SomeNat v
  go _ i | i > 0 = go (Proxy :: Proxy ('Succ nat)) (i - 1)

  
-- Alternate GADT implementation demonstrating how they are equivalent

promoteExistential' :: Int -> SomeNat
promoteExistential' = promoteCPS SomeNat