{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Data.TypeMap.Internal.List where
import Data.TypeMap.Internal.Unsafe
newtype TypeList d = TypeList [Any]
empty :: TypeList '[]
empty = TypeList []
index
:: forall a d
. KnownNat (Index a d)
=> TypeList d -> Lookup a d
index = unsafeIndex @a (!!)
cons
:: forall a d b
. b -> TypeList d -> TypeList ('(a, b) ': d)
cons = unsafeCons (:)
(<|)
:: forall a d b
. b -> TypeList d -> TypeList ('(a, b) ': d)
(<|) = cons
infixr 5 <|, `cons`
snoc
:: forall a d b
. (Last d ~ '(a, b))
=> TypeList (Init d) -> b -> TypeList d
snoc = unsafeSnoc @a (\xs x -> xs ++ [x])
(|>)
:: forall a d b
. (Last d ~ '(a, b))
=> TypeList (Init d) -> b -> TypeList d
(|>) = snoc
infixr 5 |>, `snoc`