module Data.Type.Length where
import Data.Type.Quantifier
import Type.Class.Higher
import Type.Class.Known
import Type.Family.List
data Length :: [k] -> * where
LZ :: Length Ø
LS :: !(Length as) -> Length (a :< as)
deriving instance Eq (Length as)
deriving instance Ord (Length as)
deriving instance Show (Length as)
instance Eq1 Length
instance Ord1 Length
instance Show1 Length
instance Read1 Length where
readsPrec1 d = readParen (d > 10) $ \s0 ->
[ (Some LZ,s1)
| ("LZ",s1) <- lex s0
] ++
[ (l >>- Some . LS,s2)
| ("LS",s1) <- lex s0
, (l,s2) <- readsPrec1 11 s1
]
instance Known Length Ø where
known = LZ
instance Known Length as => Known Length (a :< as) where
type KnownC Length (a :< as) = Known Length as
known = LS known
elimLength :: p Ø
-> (forall x xs. Length xs -> p xs -> p (x :< xs))
-> Length as
-> p as
elimLength z s = \case
LZ -> z
LS l -> s l $ elimLength z s l
lOdd, lEven :: Length as -> Bool
lOdd = \case
LZ -> False
LS l -> lEven l
lEven = \case
LZ -> True
LS l -> lOdd l