{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module Util.Peano
(
Peano
, ToPeano
, Length
, KnownPeano (..)
, peanoVal'
, Sing (SZ, SS)
, At
, IsLongerThan
, LongerThan
, RequireLongerThan
, requiredLongerThan
) where
import Prelude hiding (Nat)
import Data.Singletons (Sing, SingI(..))
import qualified GHC.TypeNats as GHC (Nat)
import Unsafe.Coerce (unsafeCoerce)
import Data.Constraint (Dict (..))
import GHC.TypeLits (TypeError, ErrorMessage (..))
import Data.Type.Bool (If)
import Data.Vinyl.TypeLevel (Nat(..), RLength)
import GHC.TypeNats (type (-), type (+))
type Peano = Nat
type family ToPeano (n :: GHC.Nat) :: Nat where
ToPeano 0 = 'Z
ToPeano a = 'S (ToPeano (a - 1))
type family FromPeano (n :: Nat) :: GHC.Nat where
FromPeano 'Z = 0
FromPeano ('S a) = 1 + FromPeano a
type family Length l where
Length l = RLength l
class KnownPeano (n :: Nat) where
peanoVal :: proxy n -> Natural
instance KnownPeano 'Z where
peanoVal _ = 0
instance KnownPeano a => KnownPeano ('S a) where
peanoVal _ = peanoVal' @a + 1
peanoVal' :: forall n. KnownPeano n => Natural
peanoVal' = peanoVal (Proxy @n)
data instance Sing (_ :: Nat) where
SZ :: Sing 'Z
SS :: Sing n -> Sing ('S n)
deriving instance Eq (Sing (n :: Nat))
instance SingI 'Z where
sing = SZ
instance SingI n => SingI ('S n) where
sing = SS (sing @n)
type family At (n :: Peano) s where
At 'Z (x ': _) = x
At ('S n) (_ ': xs) = At n xs
At a '[] =
TypeError
('Text "You try to access to non-existing element of the stack, n = " ':<>:
'ShowType (FromPeano a))
type family IsLongerThan (l :: [k]) (a :: Nat) :: Bool where
IsLongerThan (_ ': _) 'Z = 'True
IsLongerThan (_ ': xs) ('S a) = IsLongerThan xs a
IsLongerThan '[] _ = 'False
type LongerThan l a = IsLongerThan l a ~ 'True
type family OfLengthWithTail (acc :: GHC.Nat) (l :: [k]) :: GHC.Nat where
OfLengthWithTail a '[] = a
OfLengthWithTail a (_ ': xs) = OfLengthWithTail (a + 1) xs
type LengthWithTail l = OfLengthWithTail 0 l
type family RequireLongerThan (l :: [k]) (a :: Nat) :: Constraint where
RequireLongerThan l a =
If (IsLongerThan l a)
(() :: Constraint)
(TypeError
('Text "Stack element #" ':<>: 'ShowType (FromPeano a) ':<>:
'Text " is not accessible" ':$$:
'Text "Current stack has size of only " ':<>:
'ShowType (LengthWithTail l) ':<>:
'Text ":" ':$$: 'ShowType l
))
requiredLongerThan
:: forall l a r. (RequireLongerThan l a)
=> (LongerThan l a => r) -> r
requiredLongerThan r = do
case unsafeCoerce @(Dict (LongerThan '[Int] 'Z)) @(Dict (LongerThan l a)) Dict of
Dict -> r