Example code to implement instances for Singlton types

gistfile1.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}


-- | Example code to implement instances for Singlton types introduced GHC 7.6.1
--   see also: http://hackage.haskell.org/trac/ghc/wiki/TypeNats/Basics

module Main where

import GHC.TypeLits


-- Example 1.

data Nat1 = Zero | Succ Nat1
            deriving (Show)

newtype instance Sing (n :: Nat1) = SNat1 Nat1

instance SingI Zero where
  sing = SNat1 Zero
instance SingI n => SingI (Succ n) where
  sing = let SNat1 m :: Sing n = sing in SNat1 (Succ m)

instance SingE (Kind :: Nat1) Nat1 where
  fromSing (SNat1 n) = n


nat1ToInteger :: Nat1 -> Integer
nat1ToInteger Zero     = 0
nat1ToInteger (Succ m) = 1 + nat1ToInteger m

type family (m :: Nat1) :+ (n :: Nat1) :: Nat1
type instance Zero     :+ n = n
type instance (Succ m) :+ n = Succ (m :+ n)


-- Example 2.

data Result = Fizz | Buzz | FizzBuzz | Other Nat1
              deriving (Show)

newtype instance Sing (r :: Result) = SResult Result

instance SingI Fizz     where sing = SResult Fizz
instance SingI Buzz     where sing = SResult Buzz
instance SingI FizzBuzz where sing = SResult FizzBuzz
instance SingI n => SingI (Other n) where
  sing = let SNat1 nat1 = sing :: Sing n in
         SResult (Other nat1)

instance SingE (Kind :: Result) Result where
  fromSing (SResult s) = s


-- ghci> type One = 'Succ 'Zero
-- ghci> type Two = 'Succ One
-- ghci> type Three = 'Succ Two

-- ghci> sing :: Sing 'Zero
-- Zero
-- ghci> sing :: Sing Three
-- Succ (Succ (Succ Zero))
-- ghci> nat1ToInteger $ fromSing (sing :: Sing Three)
-- 3
-- ghci> :set -XTypeOperators 
-- ghci> nat1ToInteger $ fromSing (sing :: Sing (Three :+ Two))
-- 5

-- ghci> sing :: Sing 'Fizz
-- Fizz
-- ghci> sing :: Sing ('Other Three)
-- Other (Succ (Succ (Succ Zero)))