{-# OPTIONS_HADDOCK hide, prune #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Type.List.Families
( Head, Tail
, Snoc, Init, Last, Reverse
, StripSuffix, StripPrefix, Concat
-- * Internals
, List (..), RunList, Snoc', Reverse'
) where
-- | Extract the first element of a list, which must be non-empty.
type family Head (xs :: [k]) :: k where
Head (x ': _) = x
-- | Extract the elements after the head of a list, which must be non-empty.
type family Tail (xs :: [k]) :: [k] where
Tail (_ ': xs) = xs
-- | Extract the last element of a list, which must be non-empty.
type family Last (xs :: [k]) :: k where
Last '[x] = x
Last (_ ': xs) = Last xs
-- | Extract all but last elements of a list, which must be non-empty.
type family Init (xs :: [k]) = (ys :: [k]) | ys -> k where
Init ('[x] :: [k]) = ('[] :: [k])
Init (x ': xs) = x ': Init xs
-- | Appending a list on the other side (injective).
type Snoc (xs :: [k]) (x :: k) = (RunList (Snoc' xs x :: List k) :: [k])
-- | Reverse elements of a list (injective).
type Reverse (xs :: [k]) = (RunList (Reverse' xs :: List k) :: [k])
-- | A helper data type that makes possible injective `Snoc` and `Reverse` families.
--
-- It assures GHC type checker that the `Snoc` operation on a non-empty list
-- yields a list that contains at least two elements.
data List k
= Empty
| Single k
| TwoOrMore [k]
-- ^ An important invariant: the argument list contains at least two elements.
type family RunList (xs :: List k) = (ys :: [k]) | ys -> k xs where
RunList ('Empty :: List k) = ('[] :: [k])
RunList ('Single x) = '[x]
RunList ('TwoOrMore (x ': y ': xs)) = x ': y ': xs
type family Snoc' (xs :: [k]) (x :: k) = (ys :: List k) | ys -> k xs x where
Snoc' '[] y = 'Single y
Snoc' (x ': xs) y = 'TwoOrMore (x ': RunList (Snoc' xs y))
type family Reverse' (xs :: [k]) = (ys :: List k) | ys -> k xs where
Reverse' ('[] :: [k]) = ('Empty :: List k)
Reverse' '[x] = 'Single x
Reverse' (y ': x ': xs) = 'TwoOrMore (Snoc (RunList (Reverse' (x ': xs))) y)
-- | Append two lists.
type family Concat (as :: [k]) (bs :: [k]) :: [k] where
Concat as '[] = as -- "incoherent instance"
Concat '[] bs = bs
Concat (a ': as) bs = a ': Concat as bs
-- | Remove prefix @as@ from a list @asbs@ if @as@ is a prefix; fail otherwise.
type family StripPrefix (as :: [k]) (asbs :: [k]) :: [k] where
StripPrefix as as = '[] -- "incoherent instance"
StripPrefix '[] bs = bs
StripPrefix (a ': as) (a ': asbs) = StripPrefix as asbs
-- | Remove suffix @bs@ from a list @asbs@ if @bs@ is a suffix; fail otherwise.
type family StripSuffix (bs :: [k]) (asbs :: [k]) :: [k] where
StripSuffix '[] as = as -- "incoherent instance"
StripSuffix bs bs = '[]
StripSuffix bs (a ': asbs) = a ': StripSuffix bs asbs