Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Iavor S. Diatchki April 08, 2012
file 144 lines (99 sloc) 4.375 kb
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143
{-# LANGUAGE DataKinds #-} -- to declare the kinds
{-# LANGUAGE KindSignatures #-} -- (used all over)
{-# LANGUAGE MultiParamTypeClasses #-} -- for <=
{-# LANGUAGE TypeFamilies #-} -- for declaring operators + sing family
{-# LANGUAGE TypeOperators #-} -- for declaring operator
{-# LANGUAGE EmptyDataDecls #-} -- for declaring the kinds
{-# LANGUAGE GADTs #-} -- for examining type nats
{-# LANGUAGE PolyKinds #-} -- for Sing family
{-# LANGUAGE UndecidableInstances #-} -- for Read and Show instances
{-# OPTIONS_GHC -XNoImplicitPrelude #-}
{-| This module is an internal GHC module. It declares the constants used
in the implementation of type-level natural numbers. The programmer interface
for workin with type-level naturals should be defined in a separate library. -}

module GHC.TypeLits
  ( -- * Kinds
    Nat, Symbol

    -- * Linking type and value level
  , Sing, SingI, sing, SingRep, fromSing

    -- * Working with singletons
  , withSing, singThat

    -- * Functions on type nats
  , type (<=), type (+), type (*), type (^)

    -- * Destructing type-nats.
  , isZero, IsZero(..)
  , isEven, IsEven(..)
  ) where

import GHC.Base(Eq((==)), Bool(..), ($), otherwise, (.))
import GHC.Num(Integer, (-))
import GHC.Base(String)
import GHC.Read(Read(..))
import GHC.Show(Show(..))
import Unsafe.Coerce(unsafeCoerce)
import Data.Bits(testBit,shiftR)
import Data.Maybe(Maybe(..))
import Data.List((++))

-- | This is the *kind* of type-level natural numbers.
data Nat

-- | This is the *kind* of type-level symbols.
data Symbol


--------------------------------------------------------------------------------

-- | A family of singleton types, used to link the type-level literals
-- to run-time values.
type family SingRep a

-- | Type-level natural numbers are linked to (positive) integers.
type instance SingRep (n :: Nat) = Integer

-- | Type-level symbols are linked to strings.
type instance SingRep (n :: Symbol) = String

newtype Sing n = Sing (SingRep n)

--------------------------------------------------------------------------------

-- | The class 'SingI' provides a \"smart\" constructor for singleton types.
-- There are built-in instances for the singleton types corresponding
-- to type literals.

class SingI a where

  -- | The only value of type @Sing a@
  sing :: Sing a


-- | Comparsion of type-level naturals.
class (m :: Nat) <= (n :: Nat)

-- | Addition of type-level naturals.
type family (m :: Nat) + (n :: Nat) :: Nat

-- | Multiplication of type-level naturals.
type family (m :: Nat) * (n :: Nat) :: Nat

-- | Exponentiation of type-level naturals.
type family (m :: Nat) ^ (n :: Nat) :: Nat


--------------------------------------------------------------------------------

fromSing :: Sing a -> SingRep a
fromSing (Sing n) = n

withSing :: SingI a => (Sing a -> b) -> b
withSing f = f sing

singThat :: SingI a => (SingRep a -> Bool) -> Maybe (Sing a)
singThat p = withSing $ \x -> if p (fromSing x) then Just x else Nothing

instance Show (SingRep a) => Show (Sing a) where
  showsPrec p = showsPrec p . fromSing

instance (SingI a, Read (SingRep a), Eq (SingRep a)) => Read (Sing a) where
  readsPrec p cs = do (x,ys) <- readsPrec p cs
                      case singThat (== x) of
                        Just y -> [(y,ys)]
                        Nothing -> []





--------------------------------------------------------------------------------

data IsZero :: Nat -> * where
  IsZero :: IsZero 0
  IsSucc :: !(Sing n) -> IsZero (n + 1)

isZero :: Sing n -> IsZero n
isZero (Sing n) | n == 0 = unsafeCoerce IsZero
                | otherwise = unsafeCoerce (IsSucc (Sing (n-1)))

instance Show (IsZero n) where
  show IsZero = "0"
  show (IsSucc n) = "(" ++ show n ++ " + 1)"

data IsEven :: Nat -> * where
  IsEvenZero :: IsEven 0
  IsEven :: !(Sing (n+1)) -> IsEven (2 * n + 2)
  IsOdd :: !(Sing n) -> IsEven (2 * n + 1)

isEven :: Sing n -> IsEven n
isEven (Sing n) | n == 0 = unsafeCoerce IsEvenZero
                | testBit n 0 = unsafeCoerce (IsOdd (Sing (n `shiftR` 1)))
                | otherwise = unsafeCoerce (IsEven (Sing (n `shiftR` 1)))

instance Show (IsEven n) where
  show IsEvenZero = "0"
  show (IsEven x) = "(2 * " ++ show x ++ ")"
  show (IsOdd x) = "(2 * " ++ show x ++ " + 1)"



Something went wrong with that request. Please try again.