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