{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Type.List
(
type (++), type (+:), type (:+)
, Empty, Cons, Snoc, Head
, Tail, Last, Init, Concat
, StripPrefix, StripSuffix
, Reverse, Take, Drop, Length
, All, Map, Elem
, ConcatList, evStripSuffix, evStripPrefix, evConcat
, inferTypeableCons
) where
import Data.Constraint ((:-) (..), Constraint, Dict (..))
import Data.Type.List.Internal (Snoc)
import Data.Type.Lits
import GHC.Base (Type)
import Type.Reflection
import Unsafe.Coerce (unsafeCoerce)
type Empty = '[]
type Cons (a :: k) (as :: [k])
= a ': as
type family Head (xs :: [k]) :: k where
Head ('[] :: [k]) = TypeError ( ListError k "Head: empty type-level list." )
Head (x ': _) = x
type family Tail (xs :: [k]) :: [k] where
Tail ('[] :: [k]) = TypeError ( ListError k "Tail: empty type-level list." )
Tail (_ ': xs) = xs
type family Last (xs :: [k]) :: k where
Last ('[] :: [k]) = TypeError ( ListError k "Last: empty type-level list." )
Last '[x] = x
Last (_ ': xs) = Last xs
type family Init (xs :: [k]) :: [k] where
Init ('[] :: [k]) = TypeError ( ListError k "Init: empty type-level list." )
Init '[x] = '[]
Init (x ': xs) = x ': Init xs
type family Take (n :: Nat) (xs :: [k]) :: [k] where
Take 0 _ = '[]
Take n (x ': xs) = x ': Take (n - 1) xs
Take _ '[] = '[]
type family Drop (n :: Nat) (xs :: [k]) :: [k] where
Drop 0 xs = xs
Drop n (_ ': xs) = Drop (n - 1) xs
Drop _ '[] = '[]
type family Concat (as :: [k]) (bs :: [k]) :: [k] where
Concat '[] bs = bs
Concat as '[] = as
Concat (a ': as) bs = a ': Concat as bs
type family StripPrefix (as :: [k]) (asbs :: [k]) :: [k] where
StripPrefix as as = '[]
StripPrefix '[] asbs = asbs
StripPrefix (a ': as) (a ': asbs) = StripPrefix as asbs
StripPrefix (a ': as) (b ': asbs)
= TypeError
( 'Text "StripPrefix: the first argument is not a prefix of the second."
':$$:
'Text "Failed prefix: " ':<>: 'ShowType (a ': as)
':$$:
'Text "Second argument: " ':<>: 'ShowType (b ': asbs)
)
StripPrefix (a ': as) '[]
= TypeError
( 'Text "StripPrefix: the first argument is longer than the second."
':$$:
'Text "Failed prefix: " ':<>: 'ShowType (a ': as)
':$$:
'Text "The reduced second argument is empty."
)
type family StripSuffix (bs :: [k]) (asbs :: [k]) :: [k] where
StripSuffix bs bs = '[]
StripSuffix '[] asbs = asbs
StripSuffix (a ': bs) (b ': bs)
= TypeError
( 'Text "StripSuffix: the first argument is not a suffix of the second."
':$$:
'Text "Failed match: "
':<>: 'ShowType ((a ': bs) ~ (b ': bs))
)
StripSuffix (b ': bs) '[]
= TypeError
( 'Text "StripSuffix: the first argument is longer than the second."
':$$:
'Text "Failed suffix: " ':<>: 'ShowType (b ': bs)
':$$:
'Text "The reduced second argument is empty."
)
StripSuffix bs (a ': asbs) = a ': StripSuffix bs asbs
type family Reverse (xs :: [k]) :: [k] where
Reverse '[] = '[]
Reverse (x ': xs) = Snoc (Reverse xs) x
type family Length (xs :: [k]) :: Nat where
Length '[] = 0
Length (x ': xs) = Length xs + 1
type (a :: k) :+ (as :: [k]) = a ': as
infixr 5 :+
type (ns :: [k]) +: (n :: k) = Snoc ns n
infixl 6 +:
type (as :: [k]) ++ (bs :: [k]) = Concat as bs
infixr 5 ++
type family All (f :: k -> Constraint) (xs :: [k]) :: Constraint where
All _ '[] = ()
All f (x ': xs) = (f x, All f xs)
type family Map (f :: a -> b) (xs :: [a]) :: [b] where
Map f '[] = '[]
Map f (x ': xs) = f x ': Map f xs
type family Elem (x :: k) (xs :: [k]) :: Constraint where
Elem x (x ': xs) = ()
Elem x (_ ': xs) = Elem x xs
type ListError k t
= 'Text t ':$$:
( 'Text "Type-level error occured when operating on a list of kind "
':<>: 'ShowType [k] ':<>: 'Text "."
)
type ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k]) =
( asbs ~ Concat as bs
, as ~ StripSuffix bs asbs
, bs ~ StripPrefix as asbs
)
evConcat :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k])
. (asbs ~ Concat as bs) :- ConcatList as bs asbs
evConcat = Sub $ unsafeCoerce
( Dict :: Dict
( asbs ~ Concat as bs
, as ~ as
, bs ~ bs
)
)
evStripSuffix :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k])
. (as ~ StripSuffix bs asbs) :- ConcatList as bs asbs
evStripSuffix = Sub $ unsafeCoerce
( Dict :: Dict
( asbs ~ asbs
, as ~ StripSuffix bs asbs
, bs ~ bs
)
)
evStripPrefix :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k])
. (bs ~ StripPrefix as asbs) :- ConcatList as bs asbs
evStripPrefix = Sub $ unsafeCoerce
( Dict :: Dict
( asbs ~ asbs
, as ~ as
, bs ~ StripPrefix as asbs
)
)
inferTypeableCons :: forall (k :: Type) (ys :: [k]) (x :: k) (xs :: [k])
. (Typeable ys, ys ~ (x ': xs))
=> Dict (Typeable x, Typeable xs)
inferTypeableCons = case typeRep @ys of
App _ xRep `App` xsRep
-> case ( withTypeable xRep (Dict @(Typeable x))
, withTypeable xsRep (Dict @(Typeable xs))
) of
(Dict, Dict) -> Dict