module GHC.TypeLits
(
Nat, Symbol
, Sing, SingI, SingE, SingRep, sing, fromSing
, unsafeSingNat, unsafeSingSymbol
, Kind
, withSing, singThat
, type (<=), type (<=?), type (+), type (*), type (^)
, 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 GHC.Prim(Any)
import Unsafe.Coerce(unsafeCoerce)
import Data.Bits(testBit,shiftR)
import Data.Maybe(Maybe(..))
import Data.List((++))
type Kind = Any
data Nat
data Symbol
data family Sing (n :: k)
newtype instance Sing (n :: Nat) = SNat Integer
newtype instance Sing (n :: Symbol) = SSym String
unsafeSingNat :: Integer -> Sing (n :: Nat)
unsafeSingNat = SNat
unsafeSingSymbol :: String -> Sing (n :: Symbol)
unsafeSingSymbol = SSym
class SingI a where
sing :: Sing a
class (m :: Nat) <= (n :: Nat)
type family (m :: Nat) <=? (n :: Nat) :: Bool
type family (m :: Nat) + (n :: Nat) :: Nat
type family (m :: Nat) * (n :: Nat) :: Nat
type family (m :: Nat) ^ (n :: Nat) :: Nat
class (kparam ~ Kind) => SingE (kparam :: k) rep | kparam -> rep where
fromSing :: Sing (a :: k) -> rep
instance SingE (Kind :: Nat) Integer where
fromSing (SNat n) = n
instance SingE (Kind :: Symbol) String where
fromSing (SSym s) = s
class (SingI a, SingE (Kind :: k) rep) => SingRep (a :: k) rep | a -> rep
instance (SingI a, SingE (Kind :: k) rep) => SingRep (a :: k) rep
withSing :: SingI a => (Sing a -> b) -> b
withSing f = f sing
singThat :: (SingRep a rep) => (rep -> Bool) -> Maybe (Sing a)
singThat p = withSing $ \x -> if p (fromSing x) then Just x else Nothing
instance (SingE (Kind :: k) rep, Show rep) => Show (Sing (a :: k)) where
showsPrec p = showsPrec p . fromSing
instance (SingRep a rep, Read rep, Eq rep) => 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 (SNat n) | n == 0 = unsafeCoerce IsZero
| otherwise = unsafeCoerce (IsSucc (SNat (n1)))
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 (SNat n) | n == 0 = unsafeCoerce IsEvenZero
| testBit n 0 = unsafeCoerce (IsOdd (SNat (n `shiftR` 1)))
| otherwise = unsafeCoerce (IsEven (SNat (n `shiftR` 1)))
instance Show (IsEven n) where
show IsEvenZero = "0"
show (IsEven x) = "(2 * " ++ show x ++ ")"
show (IsOdd x) = "(2 * " ++ show x ++ " + 1)"
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4