module Data.Diverse.Type where
import Data.Diverse.Type.Internal
import Data.Kind
import GHC.TypeLits
type UniqueMember x xs = (Unique x xs, KnownNat (IndexOf x xs))
type MaybeUniqueMember x xs = (Unique x xs, KnownNat (PositionOf x xs))
type MemberAt n x xs = (KnownNat n, x ~ KindAtIndex n xs)
type MaybeMemberAt n x xs = (KnownNat n, KindAtPositionIs n x xs)
type family UniqueIfExists ys x xs :: Constraint where
UniqueIfExists '[] x xs = ()
UniqueIfExists (y ': ys) y xs = Unique y xs
UniqueIfExists (y ': ys) x xs = UniqueIfExists ys x xs
type IsDistinct (xs :: [k]) = IsDistinctImpl xs xs
type family Distinct (xs :: [k]) :: [k] where
Distinct '[] = '[]
Distinct (x ': xs) = DistinctImpl xs x xs
type Unique (x :: k) (xs :: [k]) = UniqueImpl xs x xs
type IndexOf (x :: k) (xs :: [k]) = IndexOfImpl xs x xs
type PositionOf (x :: k) (xs :: [k]) = PositionOfImpl 0 x xs
type KindAtIndex (n :: Nat) (xs :: [k]) = KindAtIndexImpl n xs n xs
type family KindAtPositionIs (n :: Nat) (x :: k) (xs :: [k]) :: Constraint where
KindAtPositionIs 0 x xs = ()
KindAtPositionIs n x xs = (x ~ KindAtIndexImpl (n 1) xs (n 1) xs)
type family KindsAtIndices (ns :: [Nat]) (xs :: [k]) :: [k] where
KindsAtIndices '[] xs = '[]
KindsAtIndices (n ': ns) xs = KindAtIndex n xs ': KindsAtIndices ns xs
type family Without (x :: k) (xs :: [k]) :: [k] where
Without x '[] = '[]
Without x (x ': xs) = Without x xs
Without x (y ': xs) = y ': Without x xs
type WithoutIndex (n :: Nat) (xs :: [k]) = WithoutIndexImpl n xs n xs
type family Length (xs :: [k]) :: Nat where
Length '[] = 0
Length (x ': xs) = 1 + Length xs
type family Tail (xs :: [k]) :: [k] where
Tail '[] = TypeError ('Text "Cannot Tail an empty type list")
Tail (x ': xs) = xs
type family Head (xs :: [k]) :: k where
Head '[] = TypeError ('Text "Cannot Head an empty type list")
Head (x ': xs) = x
type family Last (xs :: [k]) :: k where
Last '[] = TypeError ('Text "Cannot Last an empty type list")
Last (x ': x' ': xs) = Last (x' ': xs)
Last '[x] = x
type SameLength (xs :: [k1]) (ys :: [k2]) = SameLengthImpl xs ys xs ys
type family Complement (xs :: [k]) (ys :: [k]) :: [k] where
Complement xs '[] = xs
Complement xs (y ': ys) = Complement (Without y xs) ys
type family Append (xs :: [k]) (ys :: [k]) :: [k] where
Append '[] ys = ys
Append (x ': xs) ys = x ': Append xs ys
type family Init (xs :: [k]) :: [k] where
Init '[] = TypeError ('Text "Cannot Init an empty type list")
Init '[x] = '[]
Init (x ': xs) = x ': Init xs