Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Example of promoting a value to a type using higher ranked types, continuation passing and GADTs
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.