Skip to content

Instantly share code, notes, and snippets.

@hyone
Created November 1, 2012 16:10
Show Gist options
  • Save hyone/3994646 to your computer and use it in GitHub Desktop.
Save hyone/3994646 to your computer and use it in GitHub Desktop.
Example code to implement instances for Singlton types
{-# 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)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment