{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module Numeric.TypedList
( TypedList (U, (:*), Empty, TypeList, EvList, Cons, Snoc, Reverse)
, RepresentableList (..)
, TypeList, types, order, order'
, cons, snoc
, Numeric.TypedList.reverse
, Numeric.TypedList.take
, Numeric.TypedList.drop
, Numeric.TypedList.head
, Numeric.TypedList.tail
, Numeric.TypedList.last
, Numeric.TypedList.init
, Numeric.TypedList.splitAt
, Numeric.TypedList.concat
, Numeric.TypedList.length
, Numeric.TypedList.map
, module Numeric.Type.List
) where
import Control.Arrow (first)
import Data.Proxy
import GHC.Base (Type)
import GHC.Exts
import Numeric.Dim
import Numeric.Type.Evidence
import Numeric.Type.List
newtype TypedList (f :: (k -> Type)) (xs :: [k]) = TypedList [Any]
#if __GLASGOW_HASKELL__ >= 802
{-# COMPLETE TypeList #-}
{-# COMPLETE EvList #-}
{-# COMPLETE U, (:*) #-}
{-# COMPLETE U, Cons #-}
{-# COMPLETE U, Snoc #-}
{-# COMPLETE Empty, (:*) #-}
{-# COMPLETE Empty, Cons #-}
{-# COMPLETE Empty, Snoc #-}
{-# COMPLETE Reverse #-}
#endif
type TypeList (xs :: [k]) = TypedList Proxy xs
type EvidenceList (c :: k -> Constraint) (xs :: [k])
= TypedList (Evidence' c) xs
pattern TypeList :: forall (xs :: [k])
. () => RepresentableList xs => TypeList xs
pattern TypeList <- (mkRTL -> E)
where
TypeList = tList @k @xs
pattern EvList :: forall (c :: k -> Constraint) (xs :: [k])
. () => (All c xs, RepresentableList xs) => EvidenceList c xs
pattern EvList <- (mkEVL -> E)
where
EvList = _evList (tList @k @xs)
pattern U :: forall (f :: k -> Type) (xs :: [k])
. () => (xs ~ '[]) => TypedList f xs
pattern U <- (patTL @f @xs -> PatCNil)
where
U = unsafeCoerce# []
pattern Empty :: forall (f :: k -> Type) (xs :: [k])
. () => (xs ~ '[]) => TypedList f xs
pattern Empty = U
pattern (:*) :: forall (f :: k -> Type) (xs :: [k])
. ()
=> forall (y :: k) (ys :: [k])
. (xs ~ (y ': ys)) => f y -> TypedList f ys -> TypedList f xs
pattern (:*) x xs = Cons x xs
infixr 5 :*
pattern Cons :: forall (f :: k -> Type) (xs :: [k])
. ()
=> forall (y :: k) (ys :: [k])
. (xs ~ (y ': ys)) => f y -> TypedList f ys -> TypedList f xs
pattern Cons x xs <- (patTL @f @xs -> PatCons x xs)
where
Cons = Numeric.TypedList.cons
pattern Snoc :: forall (f :: k -> Type) (xs :: [k])
. ()
=> forall (sy :: [k]) (y :: k)
. (xs ~ (sy +: y)) => TypedList f sy -> f y -> TypedList f xs
pattern Snoc sx x <- (unsnocTL @f @xs -> PatSnoc sx x)
where
Snoc = Numeric.TypedList.snoc
pattern Reverse :: forall (f :: k -> Type) (xs :: [k])
. ()
=> forall (sx :: [k])
. (xs ~ Reverse sx, sx ~ Reverse xs)
=> TypedList f sx -> TypedList f xs
pattern Reverse sx <- (unreverseTL @f @xs -> PatReverse sx)
where
Reverse = Numeric.TypedList.reverse
cons :: f x -> TypedList f xs -> TypedList f (x :+ xs)
cons x xs = TypedList (unsafeCoerce# x : unsafeCoerce# xs)
{-# INLINE cons #-}
snoc :: TypedList f xs -> f x -> TypedList f (xs +: x)
snoc xs x = TypedList (unsafeCoerce# xs ++ [unsafeCoerce# x])
{-# INLINE snoc #-}
reverse :: TypedList f xs -> TypedList f (Reverse xs)
reverse (TypedList sx) = unsafeCoerce# (Prelude.reverse sx)
{-# INLINE reverse #-}
take :: Dim n -> TypedList f xs -> TypedList f (Take n xs)
take d (TypedList xs) = unsafeCoerce# (Prelude.take (intD d) xs)
{-# INLINE take #-}
drop :: Dim n -> TypedList f xs -> TypedList f (Drop n xs)
drop d (TypedList xs) = unsafeCoerce# (Prelude.drop (intD d) xs)
{-# INLINE drop #-}
head :: TypedList f xs -> f (Head xs)
head (TypedList xs) = unsafeCoerce# (Prelude.head xs)
{-# INLINE head #-}
tail :: TypedList f xs -> TypedList f (Tail xs)
tail (TypedList xs) = unsafeCoerce# (Prelude.tail xs)
{-# INLINE tail #-}
init :: TypedList f xs -> TypedList f (Init xs)
init (TypedList xs) = unsafeCoerce# (Prelude.init xs)
{-# INLINE init #-}
last :: TypedList f xs -> f (Last xs)
last (TypedList xs) = unsafeCoerce# (Prelude.last xs)
{-# INLINE last #-}
length :: TypedList f xs -> Dim (Length xs)
length = order
{-# INLINE length #-}
splitAt :: Dim n
-> TypedList f xs
-> (TypedList f (Take n xs), TypedList f (Drop n xs))
splitAt d (TypedList xs) = unsafeCoerce# (Prelude.splitAt (intD d) xs)
{-# INLINE splitAt #-}
concat :: TypedList f xs
-> TypedList f ys
-> TypedList f (xs ++ ys)
concat (TypedList xs) (TypedList ys) = unsafeCoerce# (xs ++ ys)
{-# INLINE concat #-}
map :: (forall a . f a -> g a)
-> TypedList f xs
-> TypedList g xs
map k (TypedList xs) = unsafeCoerce# (Prelude.map k' xs)
where
k' :: Any -> Any
k' = unsafeCoerce# . k . unsafeCoerce#
{-# INLINE map #-}
types :: TypedList f xs -> TypeList xs
types (TypedList xs) = unsafeCoerce# (Prelude.map (const Proxy) xs)
{-# INLINE types #-}
class RepresentableList (xs :: [k]) where
tList :: TypeList xs
instance RepresentableList ('[] :: [k]) where
tList = U
instance RepresentableList xs => RepresentableList (x ': xs :: [k]) where
tList = Proxy @x :* tList @k @xs
order' :: forall xs . RepresentableList xs => Dim (Length xs)
order' = order (tList @_ @xs)
{-# INLINE order' #-}
order :: TypedList f xs -> Dim (Length xs)
order (TypedList xs) = unsafeCoerce# (fromIntegral (Prelude.length xs) :: Word)
{-# INLINE order #-}
reifyRepList :: forall xs r
. TypeList xs
-> (RepresentableList xs => r)
-> r
reifyRepList tl k = unsafeCoerce# (MagicRepList k :: MagicRepList xs r) tl
{-# INLINE reifyRepList #-}
newtype MagicRepList xs r = MagicRepList (RepresentableList xs => r)
data PatReverse f xs
= forall (sx :: [k]) . (xs ~ Reverse sx, sx ~ Reverse xs)
=> PatReverse (TypedList f sx)
unreverseTL :: forall f xs . TypedList f xs -> PatReverse f xs
unreverseTL (TypedList xs)
= case (unsafeCoerce# (E @(xs ~ xs, xs ~ xs))
:: Evidence (xs ~ Reverse sx, sx ~ Reverse xs)
) of
E -> PatReverse (unsafeCoerce# (Prelude.reverse xs))
{-# INLINE unreverseTL #-}
mkRTL :: forall (xs :: [k])
. TypeList xs
-> Evidence (RepresentableList xs)
mkRTL xs = reifyRepList xs E
{-# INLINE mkRTL #-}
data PatSnoc f xs where
PatSNil :: PatSnoc f '[]
PatSnoc :: TypedList f ys -> f y -> PatSnoc f (ys +: y)
unsnocTL :: forall f xs . TypedList f xs -> PatSnoc f xs
unsnocTL (TypedList [])
= case (unsafeCoerce# (E @(xs ~ xs)) :: Evidence (xs ~ '[])) of
E -> PatSNil
unsnocTL (TypedList (x:xs))
= case (unsafeCoerce# (E @(xs ~ xs)) :: Evidence (xs ~ (Init xs +: Last xs))) of
E -> PatSnoc (unsafeCoerce# sy) (unsafeCoerce# y)
where
(sy, y) = unsnoc x xs
unsnoc t [] = ([], t)
unsnoc t (z:zs) = first (t:) (unsnoc z zs)
{-# INLINE unsnocTL #-}
data PatCons f xs where
PatCNil :: PatCons f '[]
PatCons :: f y -> TypedList f ys -> PatCons f (y ': ys)
patTL :: forall f xs . TypedList f xs -> PatCons f xs
patTL (TypedList [])
= case (unsafeCoerce# (E @(xs ~ xs)) :: Evidence (xs ~ '[])) of
E -> PatCNil
patTL (TypedList (x : xs))
= case (unsafeCoerce# (E @(xs ~ xs)) :: Evidence (xs ~ (Head xs ': Tail xs))) of
E -> PatCons (unsafeCoerce# x) (unsafeCoerce# xs)
{-# INLINE patTL #-}
intD :: Dim n -> Int
intD = (fromIntegral :: Word -> Int) . unsafeCoerce#
mkEVL :: forall (c :: k -> Constraint) (xs :: [k])
. EvidenceList c xs -> Evidence (All c xs, RepresentableList xs)
mkEVL U = E
mkEVL (E' :* evs) = case mkEVL evs of E -> E
#if __GLASGOW_HASKELL__ >= 802
#else
mkEVL _ = error "EvList/mkEVL: impossible argument"
#endif
_evList :: forall (c :: k -> Constraint) (xs :: [k])
. All c xs => TypeList xs -> EvidenceList c xs
_evList U = U
_evList (_ :* xs) = case _evList xs of evs -> E' :* evs
#if __GLASGOW_HASKELL__ >= 802
#else
_evList _ = error "EvList/_evList: impossible argument"
#endif