{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Debug.RecoverRTTI.Nat (
Nat(..)
, SNat(..)
, KnownNat(..)
, natVal
, Length
) where
data Nat = Z | S Nat
data SNat (n :: Nat) where
SZ :: SNat 'Z
SS :: SNat n -> SNat ('S n)
class KnownNat (n :: Nat) where
singNat :: SNat n
instance KnownNat 'Z where singNat :: SNat 'Z
singNat = SNat 'Z
SZ
instance KnownNat n => KnownNat ('S n) where singNat :: SNat ('S n)
singNat = SNat n -> SNat ('S n)
forall (n :: Nat). SNat n -> SNat ('S n)
SS SNat n
forall (n :: Nat). KnownNat n => SNat n
singNat
natVal :: forall n proxy. KnownNat n => proxy n -> Int
natVal :: proxy n -> Int
natVal proxy n
_ = SNat n -> Int
forall (m :: Nat). SNat m -> Int
go (SNat n
forall (n :: Nat). KnownNat n => SNat n
singNat :: SNat n)
where
go :: forall m. SNat m -> Int
go :: SNat m -> Int
go SNat m
SZ = Int
0
go (SS SNat n
n) = SNat n -> Int
forall (m :: Nat). SNat m -> Int
go SNat n
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
type family Length (xs :: [k]) :: Nat where
Length '[] = 'Z
Length (_ ': xs) = 'S (Length xs)