{-# 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 = forall (n :: Nat). SNat n -> SNat ('S n)
SS forall (n :: Nat). KnownNat n => SNat n
singNat
natVal :: forall n proxy. KnownNat n => proxy n -> Int
natVal :: forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Int
natVal proxy n
_ = forall (m :: Nat). SNat m -> Int
go (forall (n :: Nat). KnownNat n => SNat n
singNat :: SNat n)
where
go :: forall m. SNat m -> Int
go :: forall (m :: Nat). SNat m -> Int
go SNat m
SZ = Int
0
go (SS SNat n
n) = forall (m :: Nat). SNat m -> Int
go SNat n
n forall a. Num a => a -> a -> a
+ Int
1
type family Length (xs :: [k]) :: Nat where
Length '[] = 'Z
Length (_ ': xs) = 'S (Length xs)