{-# 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
, List (..), RunList, Snoc', Reverse'
) where
type family Head (xs :: [k]) :: k where
Head (x ': _) = x
type family Tail (xs :: [k]) :: [k] where
Tail (_ ': xs) = xs
type family Last (xs :: [k]) :: k where
Last '[x] = x
Last (_ ': xs) = Last xs
type family Init (xs :: [k]) = (ys :: [k]) | ys -> k where
Init ('[x] :: [k]) = ('[] :: [k])
Init (x ': xs) = x ': Init xs
type Snoc (xs :: [k]) (x :: k) = (RunList (Snoc' xs x :: List k) :: [k])
type Reverse (xs :: [k]) = (RunList (Reverse' xs :: List k) :: [k])
data List k
= Empty
| Single k
| TwoOrMore [k]
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)
type family Concat (as :: [k]) (bs :: [k]) :: [k] where
Concat as '[] = as
Concat '[] bs = bs
Concat (a ': as) bs = a ': Concat as bs
type family StripPrefix (as :: [k]) (asbs :: [k]) :: [k] where
StripPrefix as as = '[]
StripPrefix '[] bs = bs
StripPrefix (a ': as) (a ': asbs) = StripPrefix as asbs
type family StripSuffix (bs :: [k]) (asbs :: [k]) :: [k] where
StripSuffix '[] as = as
StripSuffix bs bs = '[]
StripSuffix bs (a ': asbs) = a ': StripSuffix bs asbs