module Prelude.Type.Families (
module Prelude,
module Prelude.Type.Families,
module GHC.TypeLits,
module Prelude.Type.Integer,
module Prelude.Type.Value
) where
import Prelude.Type.Value
import Prelude.Type.Integer
import GHC.TypeLits (Symbol, Nat)
import Prelude (
Bool(False, True),
Maybe(Nothing, Just),
Either(Left, Right),
Ordering(LT, GT, EQ)
)
type family If (p :: Bool) (a :: k) (b :: k) :: k
type instance If True a b = a
type instance If False a b = b
type Show a = Shows a '[]
type family Shows (a :: k) (t :: [Symbol]) :: [Symbol]
type family Kind (a :: k) :: *
type family (a :: k) == (b :: k) :: Bool
type a /= b = Not (a == b)
type family Compare (a :: k) (b :: k) :: Ordering
type a < b = FromOrdering True False False (Compare a b)
type a <= b = FromOrdering True True False (Compare a b)
type a >= b = FromOrdering False True True (Compare a b)
type a > b = FromOrdering False False True (Compare a b)
type Max a b = FromOrdering b a a (Compare a b)
type Min a b = FromOrdering a a b (Compare a b)
type family ToEnum (i :: Integer) :: k
type family FromEnum (a :: k) :: Integer
type Succ a = ToEnum (I 1 + FromEnum a)
type Pred a = ToEnum (FromEnum a `Minus` I 1)
type EnumFromTo a b = EnumFromTo_1 (FromEnum a < FromEnum b) a b
type family EnumFromTo_1 (lt :: Bool) (a :: k) (b :: k) :: [k]
type instance EnumFromTo_1 True a b = a ': EnumFromTo (Succ a) b
type instance EnumFromTo_1 False a b = '[]
type family MinBound :: k
type family MaxBound :: k
type instance Shows '() x = "()" ': x
type instance ToEnum Zeros = '()
type instance FromEnum '() = Zeros
type instance Kind (a :: ()) = ()
type instance ((a :: ()) == b) = True
type instance MinBound = '()
type instance MaxBound = '()
type instance Compare '() '() = EQ
type instance Shows Nothing x = "Nothing" ': x
type instance Shows (Just a) x = "Just" ': Shows a x
type instance FromEnum Nothing = Zeros
type instance FromEnum (Just x) = I 1 + FromEnum x
type instance ToEnum Zeros = Nothing
type instance ToEnum (One i) = Just (ToEnum (IntegerCons False i))
type instance ToEnum (Zero i) = Just (ToEnum (Zero i `Minus` I 1))
type instance Compare Nothing Nothing = EQ
type instance Compare Nothing (Just a) = LT
type instance Compare (Just a) Nothing = GT
type instance Compare (Just a) (Just b) = Compare a b
type instance Kind (a :: Maybe k) = Maybe (Kind (Undefined :: k))
type instance Nothing == Nothing = True
type instance Just a == Nothing = False
type instance Nothing == Just b = False
type instance Just a == Just b = a == b
type instance MinBound = Nothing
type instance MaxBound = Just MaxBound
type instance Shows True x = "True" ': x
type instance Shows False x = "False" ': x
type instance FromEnum False = I 0
type instance FromEnum True = I 1
type instance ToEnum Zeros = False
type instance ToEnum (One Zeros) = True
type instance Compare True True = EQ
type instance Compare False False = EQ
type instance Compare True False = GT
type instance Compare False True = LT
type instance Kind (a :: Bool) = Bool
type instance True == True = True
type instance True == False = False
type instance False == True = False
type instance False == False = True
type instance MinBound = False
type instance MaxBound = True
type family Not (a :: Bool) :: Bool
type instance Not True = False
type instance Not False = True
type family ((a :: Bool) || (b :: Bool)) :: Bool
type instance False || a = a
type instance True || a = True
type family ((a :: Bool) && (b :: Bool)) :: Bool
type instance True && a = a
type instance False && a = False
type family FromOrdering (lt :: k) (eq :: k) (gt :: k) (o :: Ordering) :: k
type instance FromOrdering a b c LT = a
type instance FromOrdering a b c EQ = b
type instance FromOrdering a b c GT = c
type instance Shows LT x = "LT" ': x
type instance Shows EQ x = "EQ" ': x
type instance Shows GT x = "GT" ': x
type instance FromEnum LT = I 0
type instance FromEnum EQ = I 1
type instance FromEnum GT = I 2
type instance ToEnum Zeros = LT
type instance ToEnum (One Zeros) = EQ
type instance ToEnum (Zero (One Zeros)) = GT
type instance Compare EQ EQ = EQ
type instance Compare LT LT = EQ
type instance Compare GT GT = EQ
type instance Compare LT EQ = LT
type instance Compare LT GT = LT
type instance Compare EQ GT = LT
type instance Compare GT EQ = GT
type instance Compare GT LT = GT
type instance Compare EQ LT = GT
type instance Kind (a :: Ordering) = Ordering
type instance MinBound = LT
type instance MaxBound = GT
type family CombineOrdering (a :: Ordering) (b :: Ordering) :: Ordering
type instance CombineOrdering LT a = LT
type instance CombineOrdering EQ a = a
type instance CombineOrdering GT a = GT
type instance Shows (Left a) x = "Left" ': Shows a x
type instance Shows (Right a) x = "Right" ': Shows a x
type instance Compare (Left a) (Right b) = LT
type instance Compare (Right a) (Left b) = GT
type instance Compare (Right a) (Right b) = Compare a b
type instance Compare (Left a) (Left b) = Compare a b
type instance Kind (a :: Either k1 k2) = Either (Kind (Undefined :: k1)) (Kind (Undefined :: k2))
type instance Left a == Left b = a == b
type instance Right a == Right b = a == b
type instance Left a == Right b = False
type instance Right a == Left b = False
type instance MinBound = Left MinBound
type instance MaxBound = Right MaxBound
type instance Shows '(a, b) x = "(" ': Shows a ("," ': Shows b (")" ': x))
type instance Shows '(a, b, c) x = "(" ': Shows a ("," ': Shows b ("," ': Shows c (")" ': x)))
type instance Shows '(a, b, c, d) x = "(" ': Shows a ("," ': Shows b ("," ': Shows c ("," ': Shows d (")" ': x))))
type instance Compare '(a, b) '(e, f) = CombineOrdering (Compare a e) (Compare b f)
type instance Compare '(a, b, c) '(e, f, g) = CombineOrdering (Compare a e) (Compare '(b, c) '(f, g))
type instance Compare '(a, b, c, d) '(e, f, g, h) = CombineOrdering (Compare a e) (Compare '(b, c, d) '(f, g, h))
type instance Kind '(a, b) = (Kind a, Kind b)
type instance Kind '(a, b, c) = (Kind a, Kind b, Kind c)
type instance Kind '(a, b, c, d) = (Kind a, Kind b, Kind c, Kind d)
type instance '(a, b) == '(e, f) = (a == e) && (b == f)
type instance '(a, b, c) == '(e, f, g) = (a == e) && (b == f) && (c == g)
type instance '(a, b, c, d) == '(e, f, g, h) = (a == e) && (b == f) && (c == g) && (d == h)
type instance MinBound = '(MinBound, MinBound)
type instance MinBound = '(MinBound, MinBound, MinBound)
type instance MinBound = '(MinBound, MinBound, MinBound, MinBound)
type instance MaxBound = '(MaxBound, MaxBound)
type instance MaxBound = '(MaxBound, MaxBound, MaxBound)
type instance MaxBound = '(MaxBound, MaxBound, MaxBound, MaxBound)
type family Fst (p :: (a, b)) :: a
type instance Fst '(a, b) = a
type family Snd (p :: (a, b)) :: b
type instance Snd '(a, b) = b
type instance Kind (a :: Nat) = Nat
type instance Kind (a :: Symbol) = Symbol
type instance MinBound = 0
data StarKind
type instance Kind (a :: *) = StarKind
type Compose f g a = f (g a)
type family (a :: x) $ (b :: y) :: k
type instance a $ b = a b
type Id a = a
type Flip f a b = f a b
type instance Shows '[] r = "[]" ': r
type instance Shows (x ': xs) r = "(" ': Shows x ("," ': (ShowsTail xs r))
type family ShowsTail (a :: [k]) (x :: [Symbol]) :: [Symbol]
type instance ShowsTail '[] r = "]" ': r
type instance ShowsTail (x ': xs) r = "," ': Shows x (ShowsTail xs r)
type instance Compare '[] '[] = EQ
type instance Compare '[] (x ': xs) = LT
type instance Compare (x ': xs) '[] = GT
type instance Compare (x ': xs) (y ': ys) = CombineOrdering (Compare x y) (Compare xs ys)
type instance Kind (a :: [k]) = [Kind (Undefined :: k)]
type instance '[] == '[] = True
type instance '[] == (x ': xs) = False
type instance (x ': xs) == '[] = False
type instance (x ': xs) == (y ': ys) = (x == y) && (xs == ys)
type instance MinBound = '[]
type family Head (l :: [k]) :: k
type instance Head '[] = Error "Head_: empty list"
type instance Head (x ': xs) = x
type family Tail (l :: [k]) :: [k]
type instance Tail '[] = Error "Tail_: empty list"
type instance Tail (x ': xs) = xs
type family Last (a :: [k]) :: k
type instance Last '[] = Error "Last_: empty list"
type instance Last (x ': y ': xs) = Last (y ': xs)
type instance Last (x ': '[]) = x
type family Init (a :: [k]) :: [k]
type instance Init '[] = Error "Init_: empty list"
type instance Init (x ': y ': xs) = x ': Init (y ': xs)
type instance Init (x ': '[]) = '[]
type family Null (a :: [k]) :: Bool
type instance Null '[] = True
type instance Null (x ': xs) = False
type family Length (a :: [k]) :: Integer
type instance Length '[] = I 0
type instance Length (x ': xs) = I 1 + Length xs
type family (a :: [k]) !! (i :: Integer) :: k
type instance '[] !! i = Error "(!!\\): index too large"
type instance (x ': xs) !! i = At_1 x xs (IsZero i) i
type family At_1 (a :: k) (b :: [k]) (c :: Bool) (d :: Integer) :: k
type instance At_1 x xs True i = x
type instance At_1 x xs False i = xs !! (i `Minus` I 1)
type family Drop (i :: Integer) (a :: [k]) :: [k]
type instance Drop i '[] = '[]
type instance Drop Zeros (x ': xs) = (x ': xs)
type instance Drop Ones (x ': xs) = Error "Drop_: negative count"
type instance Drop (One i) (x ': xs) = Drop i (Drop i xs)
type instance Drop (Zero i) (x ': xs) = Drop i (Drop i (x ': xs))
type family (a :: [k]) ++ (b :: [k]) :: [k]
type instance '[] ++ l = l
type instance (x ': xs) ++ l = x ': (xs ++ l)
type family Concat (a :: [[k]]) :: [k]
type instance Concat '[] = '[]
type instance Concat (x ': xs) = x ++ Concat xs
type Replicate i a = Replicate_1 (IsZero i) i a
type family Replicate_1 (z :: Bool) (i :: Integer) (a :: k) :: [k]
type instance Replicate_1 True i a = '[]
type instance Replicate_1 False i a = a ': Replicate (i `Minus` I 1) a
type family And (a :: [Bool]) :: Bool
type instance And '[] = True
type instance And (x ': xs) = x && And xs
type family Or (a :: [Bool]) :: Bool
type instance Or '[] = False
type instance Or (x ': xs) = x || Or xs
type family Elem (a :: k) (b :: [k]) :: Bool
type instance Elem a '[] = False
type instance Elem a (x ': xs) = Elem_1 (a == x) a xs
type family Elem_1 (p :: Bool) (a :: k) (b :: [k]) :: Bool
type instance Elem_1 True a xs = True
type instance Elem_1 False a xs = Elem a xs
type NotElem a b = Not (Elem a b)
type instance Shows i x = ShowsInteger_2 (IsZero i) i x
type family ShowsInteger_2 (z :: Bool) (i :: Integer) (x :: [Symbol]) :: [Symbol]
type instance ShowsInteger_2 True i x = x
type instance ShowsInteger_2 False i x =
(Shows (Quot i (I 10)) (Digit (Rem i (I 10)) ': x))
type family IsZero (i :: Integer) :: Bool
type instance IsZero Zeros = True
type instance IsZero (Zero i) = IsZero i
type instance IsZero Ones = False
type instance IsZero (One i) = False
type family Digit (i :: Integer) :: Symbol
type instance Digit Zeros = "0"
type instance Digit (One Zeros) = "1"
type instance Digit (Zero (One Zeros)) = "2"
type instance Digit (One (One Zeros)) = "3"
type instance Digit (Zero (Zero (One Zeros))) = "4"
type instance Digit (One (Zero (One Zeros))) = "5"
type instance Digit (Zero (One (One Zeros))) = "6"
type instance Digit (One (One (One Zeros))) = "7"
type instance Digit (Zero (Zero (Zero (One Zeros)))) = "8"
type instance Digit (One (Zero (Zero (One Zeros)))) = "9"
type instance i == j = IntegerEqual (IntegerEnd2 i j) i j
type family IntegerEqual (p :: Bool) (i :: Integer) (j :: Integer) :: Bool
type instance IntegerEqual True i j = IntegerHead i == IntegerHead j
type instance IntegerEqual False i j = (IntegerHead i == IntegerHead j) && (IntegerTail i == IntegerTail j)
type instance FromEnum i = i
type instance ToEnum i = i
type instance Kind (a :: Integer) = Integer
type family IntegerEnd (i :: Integer) :: Bool
type instance IntegerEnd Zeros = True
type instance IntegerEnd Ones = True
type instance IntegerEnd (One i) = False
type instance IntegerEnd (Zero i) = False
type IntegerEnd2 i j = IntegerEnd i && IntegerEnd j
type family ((a :: k) + (b :: k)) :: k
type instance a + b = AddWithCarry False a b
type AddWithCarry c i j = AddWithCarry_2 (IntegerEnd2 i j) c i j
type family AddWithCarry_2 (end :: Bool) (a :: Bool) (b :: Integer) (c :: Integer) :: Integer
type instance AddWithCarry_2 True False Zeros i = i
type instance AddWithCarry_2 True False Ones Ones = Zeros
type instance AddWithCarry_2 True False Ones Zeros = Ones
type instance AddWithCarry_2 True True Zeros Zeros = One Zeros
type instance AddWithCarry_2 True True Zeros Ones = Zeros
type instance AddWithCarry_2 True True Ones Ones = Ones
type instance AddWithCarry_2 True True Ones Zeros = Zeros
type instance AddWithCarry_2 False c i j =
AddWithCarry_3 (Add3 c (IntegerHead i) (IntegerHead j))
(IntegerTail i) (IntegerTail j)
type family AddWithCarry_3 (h :: (Bool, Bool)) (i :: Integer) (j :: Integer) :: Integer
type instance AddWithCarry_3 '(s, c) i j = IntegerCons s (AddWithCarry c i j)
type family Add3 (a :: Bool) (b :: Bool) (c :: Bool) :: (Bool, Bool)
type instance Add3 True True True = '(True, True)
type instance Add3 False True True = '(False, True)
type instance Add3 True False True = '(False, True)
type instance Add3 True True False = '(False, True)
type instance Add3 False False True = '(True, False)
type instance Add3 True False False = '(True, False)
type instance Add3 False True False = '(True, False)
type instance Add3 False False False = '(False, False)
type family (a :: k) `Minus` (b :: k) :: k
type instance a `Minus` b = a + Negate b
type family Negate (a :: k) :: k
type instance Negate a = Complement a + I 1
type family (a :: k) * (b :: k) :: k
type instance Zeros * j = Zeros
type instance Ones * j = Negate j
type instance (Zero i) * j = IntegerCons False (i * j)
type instance (One i) * j = j + IntegerCons False (i * j)
type Signum a = FromOrdering Ones Zeros (One Zeros) (Compare0 a)
type Abs a = FromOrdering (Negate a) a a (Compare0 a)
type Subtract a b = b `Minus` a
type Even i = IntegerHead i
type Odd i = Not (Even i)
type family Gcd_1 (zs :: Bool) (a :: Integer) (b :: Integer) :: Integer
type family Gcd_3 (z :: Bool) (a :: Integer) (b :: Integer) :: Integer
type Gcd a b = Gcd_1 (IsZero a && IsZero b) a b
type instance Gcd_1 True a b = Error "Gcd 0 0 is undefined"
type instance Gcd_1 False a b = Gcd_2 (Abs a) (Abs b)
type Gcd_2 a b = Gcd_3 (IsZero b) a b
type instance Gcd_3 True a b = a
type instance Gcd_3 False a b = Gcd_2 b (Rem a b)
type instance Compare (i :: Integer) j = Compare0 (i `Minus` j)
type family Compare0 (i :: Integer) :: Ordering
type instance Compare0 Zeros = EQ
type instance Compare0 Ones = LT
type instance Compare0 (One i) = FromOrdering LT GT GT (Compare0 i)
type instance Compare0 (Zero i) = Compare0 i
type Undefined = Error "undefined"
type family Error (a :: k1) :: k2
type instance Error (a :: k1) = ERROR a
type family ERROR (a :: k1) :: k2
type family AsKindOf (a :: k) (b :: k) :: k
type instance AsKindOf a b = a
type family Xor (a :: k) (b :: k) :: k
type instance Xor True True = False
type instance Xor True False = True
type instance Xor False True = True
type instance Xor False False = False
type instance Xor i j = Xor_2 (IntegerEnd2 i j) i j
type family Xor_2 (end :: Bool) (a :: k) (b :: k) :: k
type instance Xor_2 True Zeros Zeros = Zeros
type instance Xor_2 True Ones Ones = Zeros
type instance Xor_2 True Zeros Ones = Ones
type instance Xor_2 True Ones Zeros = Ones
type instance Xor_2 False i j =
IntegerCons (Xor (IntegerHead i) (IntegerHead j))
(Xor (IntegerTail i) (IntegerTail j))
type family ((a :: k) .&. (b :: k)) :: k
type instance (True .&. True) = True
type instance (True .&. False) = False
type instance (False .&. True) = False
type instance (False .&. False) = False
type instance i .&. j = BitwiseAnd_2 (IntegerEnd2 i j) i j
type family BitwiseAnd_2 (end :: Bool) (a :: k) (b :: k) :: k
type instance BitwiseAnd_2 True Zeros Zeros = Zeros
type instance BitwiseAnd_2 True Ones Ones = Ones
type instance BitwiseAnd_2 True Zeros Ones = Zeros
type instance BitwiseAnd_2 True Ones Zeros = Zeros
type instance BitwiseAnd_2 False i j =
IntegerCons (IntegerHead i .&. IntegerHead j)
(IntegerTail i .&. IntegerTail j)
type family Complement (a :: k) :: k
type instance Complement True = False
type instance Complement False = True
type instance Complement Zeros = Ones
type instance Complement Ones = Zeros
type instance Complement (One i) = IntegerCons False (Complement i)
type instance Complement (Zero i) = IntegerCons True (Complement i)
type QuotRem a b = '(
(Signum a * Signum b * Fst (QuotRem' (Abs a) (Abs b))),
(Signum a * Snd (QuotRem' (Abs a) (Abs b))))
type family QuotRem'_2 (p :: Bool) (a :: Integer) (b :: Integer) :: (Integer, Integer)
type family QuotRem'_3 (b :: Integer) (qr :: (Integer, Integer)) :: (Integer, Integer)
type family QuotRem'_4 (p :: Bool) (a :: Integer) (b :: Integer) (c :: Integer) :: (Integer, Integer)
type QuotRem' a b = QuotRem'_2 (a < b) a b
type instance QuotRem'_2 True a b = '(I 0, a)
type instance QuotRem'_2 False a b = QuotRem'_3 b (QuotRem' a (IntegerCons False b))
type instance QuotRem'_3 b '(q', r') = QuotRem'_4 (r' >= b) b q' r'
type instance QuotRem'_4 True b q' r' = '(IntegerCons True q', r' `Minus` b)
type instance QuotRem'_4 False b q' r' = '(IntegerCons False q', r')
type Rem a b = Snd (QuotRem a b)
type Quot a b = Fst (QuotRem a b)