module Data.Type.Row (
Row (..), (:++),
Length, KnownLength,
IndexOf, Member,
Inclusive,
Is, InstanceOf
) where
import Data.Type.Nat
import Data.Type.Bool (If)
infixr 5 :+, :-, :++
data Row a
= Nil
| a :+ Row a
| a :- Row a
type family l :++ m where
Nil :++ l = l
(e :+ l) :++ m = e :+ l :++ m
(e :- l) :++ m = e :- l :++ m
type family Length l where
Length Nil = Zero
Length (h :+ t) = Succ (Length t)
Length (h :- t) = Succ (Length t)
class KnownNat (Length l) => KnownLength l
instance KnownNat (Length l) => KnownLength l
type IndexOf e l = NthIndexOf Zero e l
type family NthIndexOf n e l where
NthIndexOf Zero e (e :+ l) = Zero
NthIndexOf (Succ n) e (e :+ l) = Succ (NthIndexOf n e l)
NthIndexOf n e (f :+ l) = Succ (NthIndexOf n e l)
NthIndexOf n e (e :- l) = Succ (NthIndexOf (Succ n) e l)
NthIndexOf n e (f :- l) = Succ (NthIndexOf n e l)
class KnownNat (IndexOf e l) => Member e l
instance KnownNat (IndexOf e l) => Member e l
class KnownLength l => Inclusive l
instance Inclusive Nil
instance Inclusive l => Inclusive (e :+ l)
type family Is (name :: k) (f :: * -> *) :: Bool
type InstanceOf name l = InstanceOfNone name '[] l
type family InstanceOfNone name ex l where
InstanceOfNone name ex (f :- l) = InstanceOfNone name (f ': ex) l
InstanceOfNone name ex (f :+ l) =
If (Is name f)
(If (Elem f ex) (InstanceOfNone name (Remove f ex) l) f)
(InstanceOfNone name ex l)
type family Elem e l where
Elem e '[] = False
Elem e (e ': l) = True
Elem e (f ': l) = Elem e l
type family Remove e l where
Remove e (e ': l) = l
Remove e (f ': l) = f ': Remove e l