{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module Numeric.TypedList
( TypedList (U, (:*), Empty, TypeList, EvList, Cons, Snoc, Reverse)
, RepresentableList (..)
, Dict1 (..), DictList
, TypeList, types, typeables, inferTypeableList
, 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.stripPrefix
, Numeric.TypedList.stripSuffix
, Numeric.TypedList.sameList
, Numeric.TypedList.concat
, Numeric.TypedList.length
, Numeric.TypedList.map
, module Data.Type.List
, typedListShowsPrecC, typedListShowsPrec
, typedListReadPrec, withTypedListReadPrec
) where
import Control.Arrow (first)
import Data.Constraint hiding ((***))
import Data.Data
import Data.Type.List
import Data.Type.List.Internal
import Data.Type.Lits
import Data.Void
import GHC.Base (Type)
import GHC.Exts
import GHC.Generics hiding (Infix, Prefix)
import qualified Text.ParserCombinators.ReadPrec as Read
import qualified Text.Read as Read
import qualified Text.Read.Lex as Read
import qualified Type.Reflection as R
import Unsafe.Coerce (unsafeCoerce)
import {-# SOURCE #-} Numeric.Dimensions.Dim (Dim, dimVal, minusDimM)
newtype TypedList (f :: (k -> Type)) (xs :: [k]) = TypedList [Any]
deriving (Typeable)
{-# COMPLETE TypeList #-}
{-# COMPLETE EvList #-}
{-# COMPLETE U, (:*) #-}
{-# COMPLETE U, Cons #-}
{-# COMPLETE U, Snoc #-}
{-# COMPLETE Empty, (:*) #-}
{-# COMPLETE Empty, Cons #-}
{-# COMPLETE Empty, Snoc #-}
{-# COMPLETE Reverse #-}
instance (Typeable k, Typeable f, Typeable xs, All Data (Map f xs))
=> Data (TypedList (f :: (k -> Type)) (xs :: [k])) where
gfoldl _ z U = z U
gfoldl k z (x :* xs) = case inferTypeableCons @xs of
Dict -> z (:*) `k` x `k` xs
gunfold k z _ = case typeables @xs of
U -> z U
_ :* _ -> case inferTypeableCons @xs of Dict -> k (k (z (:*)))
toConstr U = typedListConstrEmpty
toConstr (_ :* _) = typedListConstrCons
dataTypeOf _ = typedListDataType
typedListDataType :: DataType
typedListDataType = mkDataType
"Numeric.TypedList.TypedList" [typedListConstrEmpty, typedListConstrCons]
typedListConstrEmpty :: Constr
typedListConstrEmpty = mkConstr typedListDataType "U" [] Prefix
typedListConstrCons :: Constr
typedListConstrCons = mkConstr typedListDataType ":*" [] Infix
type family TypedListRepNil (xs :: [k]) :: (Type -> Type) where
TypedListRepNil '[] = C1 ('MetaCons "U" 'PrefixI 'False) U1
TypedListRepNil (_ ': _) = Rec0 Void
type family TypedListRepCons (f :: (k -> Type)) (xs :: [k]) :: (Type -> Type) where
TypedListRepCons _ '[]
= Rec0 Void
TypedListRepCons f (x ': xs)
= C1 ('MetaCons ":*" ('InfixI 'RightAssociative 5) 'False)
( S1 ('MetaSel 'Nothing 'NoSourceUnpackedness
'NoSourceStrictness 'DecidedLazy)
(Rec0 (f x))
:*:
S1 ('MetaSel 'Nothing 'NoSourceUnpackedness
'NoSourceStrictness 'DecidedLazy)
(Rec0 (TypedList f xs))
)
instance Generic (TypedList (f :: (k -> Type)) (xs :: [k])) where
type Rep (TypedList f xs) = D1
('MetaData "TypedList" "Numeric.TypedList" "dimensions" 'False)
( TypedListRepNil xs :+: TypedListRepCons f xs )
from U = M1 (L1 (M1 U1))
from (x :* xs) = M1 (R1 (M1 (M1 (K1 x) :*: M1 (K1 xs))))
to (M1 (L1 _))
| Dict <- unsafeEqTypes @xs @'[] = U
to (M1 (R1 xxs))
| Dict <- unsafeEqTypes @xs @(Head xs ': Tail xs)
, M1 (M1 (K1 x) :*: M1 (K1 xs)) <- xxs = x :* xs
type TypeList = (TypedList Proxy :: [k] -> Type)
data Dict1 :: (k -> Constraint) -> k -> Type where
Dict1 :: c a => Dict1 c a
deriving Typeable
instance (Typeable k, Typeable p, Typeable a, p a)
=> Data (Dict1 (p :: k -> Constraint) (a :: k)) where
gfoldl _ z Dict1 = z Dict1
toConstr _ = dictConstr
gunfold _ z _ = z Dict1
dataTypeOf _ = dictDataType
dictConstr :: Constr
dictConstr = mkConstr dictDataType "Dict1" [] Prefix
dictDataType :: DataType
dictDataType = mkDataType "Numeric.TypedList.Dict1" [dictConstr]
deriving instance Eq (Dict1 (p :: k -> Constraint) (a :: k))
deriving instance Ord (Dict1 (p :: k -> Constraint) (a :: k))
deriving instance Show (Dict1 (p :: k -> Constraint) (a :: k))
type DictList (c :: k -> Constraint)
= (TypedList (Dict1 c) :: [k] -> Type)
pattern TypeList :: forall xs . () => RepresentableList xs => TypeList xs
pattern TypeList <- (mkRTL -> Dict)
where
TypeList = tList @xs
pattern EvList :: forall c xs
. () => (All c xs, RepresentableList xs) => DictList c xs
pattern EvList <- (mkEVL -> Dict)
where
EvList = _evList (tList @xs)
pattern U :: forall (k :: Type) (f :: k -> Type) (xs :: [k])
. () => (xs ~ '[]) => TypedList f xs
pattern U <- (patTL @k @f @xs -> PatCNil)
where
U = coerce ([] :: [Any])
pattern Empty :: forall (k :: Type) (f :: k -> Type) (xs :: [k])
. () => (xs ~ '[]) => TypedList f xs
pattern Empty = U
pattern (:*) :: forall f xs
. ()
=> forall y ys
. (xs ~ (y ': ys)) => f y -> TypedList f ys -> TypedList f xs
pattern (:*) x xs = Cons x xs
infixr 5 :*
pattern Cons :: forall f xs
. ()
=> forall y ys
. (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 xs . ()
=> forall sy y . SnocList sy y xs
=> 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 xs . ()
=> forall sx . ReverseList xs sx
=> TypedList f sx -> TypedList f xs
pattern Reverse sx <- (unreverseTL @_ @f @xs -> PatReverse sx)
where
Reverse = Numeric.TypedList.reverse
cons :: forall f x xs
. f x -> TypedList f xs -> TypedList f (x :+ xs)
cons x xs = TypedList (unsafeCoerce x : coerce xs)
{-# INLINE cons #-}
snoc :: forall f xs x
. TypedList f xs -> f x -> TypedList f (xs +: x)
snoc xs x = TypedList (coerce xs ++ [unsafeCoerce x])
{-# INLINE snoc #-}
reverse :: forall f xs
. TypedList f xs -> TypedList f (Reverse xs)
reverse = coerce (Prelude.reverse :: [Any] -> [Any])
{-# INLINE reverse #-}
head :: forall f xs
. TypedList f xs -> f (Head xs)
head (TypedList xs) = unsafeCoerce (Prelude.head xs)
{-# INLINE head #-}
tail :: forall f xs
. TypedList f xs -> TypedList f (Tail xs)
tail = coerce (Prelude.tail :: [Any] -> [Any])
{-# INLINE tail #-}
init :: forall f xs
. TypedList f xs -> TypedList f (Init xs)
init = coerce (Prelude.init :: [Any] -> [Any])
{-# INLINE init #-}
last :: forall f xs
. TypedList f xs -> f (Last xs)
last (TypedList xs) = unsafeCoerce (Prelude.last xs)
{-# INLINE last #-}
take :: forall (n :: Nat) f xs
. Dim n -> TypedList f xs -> TypedList f (Take n xs)
take = coerce (Prelude.take . dimValInt :: Dim n -> [Any] -> [Any])
{-# INLINE take #-}
drop :: forall (n :: Nat) f xs
. Dim n -> TypedList f xs -> TypedList f (Drop n xs)
drop = coerce (Prelude.drop . dimValInt :: Dim n -> [Any] -> [Any])
{-# INLINE drop #-}
length :: forall f xs
. TypedList f xs -> Dim (Length xs)
length = order
{-# INLINE length #-}
splitAt :: forall (n :: Nat) f xs
. Dim n
-> TypedList f xs
-> (TypedList f (Take n xs), TypedList f (Drop n xs))
splitAt = coerce (Prelude.splitAt . dimValInt :: Dim n -> [Any] -> ([Any], [Any]))
{-# INLINE splitAt #-}
order' :: forall xs . RepresentableList xs => Dim (Length xs)
order' = order (tList @xs)
{-# INLINE order' #-}
order :: forall f xs
. TypedList f xs -> Dim (Length xs)
order = unsafeCoerce (fromIntegral . Prelude.length :: [Any] -> Word)
{-# INLINE order #-}
concat :: forall f xs ys
. TypedList f xs
-> TypedList f ys
-> TypedList f (xs ++ ys)
concat = coerce ((++) :: [Any] -> [Any] -> [Any])
{-# INLINE concat #-}
stripPrefix :: forall f xs ys
. ( All Typeable xs, All Typeable ys, All Eq (Map f xs))
=> TypedList f xs
-> TypedList f ys
-> Maybe (TypedList f (StripPrefix xs ys))
stripPrefix U ys = Just ys
stripPrefix _ U = Nothing
stripPrefix ((x :: f x) :* xs) ((y :: f y) :* ys)
| Just Refl <- eqT @x @y
, x == y = coerce (stripPrefix xs ys)
| otherwise = Nothing
{-# INLINE stripPrefix #-}
stripSuffix :: forall f xs ys
. ( All Typeable xs, All Typeable ys, All Eq (Map f xs))
=> TypedList f xs
-> TypedList f ys
-> Maybe (TypedList f (StripSuffix xs ys))
stripSuffix U ys = Just ys
stripSuffix _ U = Nothing
stripSuffix xs ys
| Just n <- order ys `minusDimM` order xs
, (zs, xs') <- Numeric.TypedList.splitAt n ys
, EvList <- Numeric.TypedList.drop n $ _evList @_ @Typeable ys
, Just (Refl, True) <- sameList xs xs'
= Just (coerce zs)
| otherwise = Nothing
{-# INLINE stripSuffix #-}
sameList :: forall f xs ys
. ( All Typeable xs, All Typeable ys, All Eq (Map f xs))
=> TypedList f xs
-> TypedList f ys
-> Maybe (xs :~: ys, Bool)
sameList U U = Just (Refl, True)
sameList ((x :: f x) :* xs) ((y :: f y) :* ys)
| Just Refl <- eqT @x @y
, Just (Refl, b) <- sameList xs ys
= Just (Refl, x == y && b)
| otherwise
= Nothing
sameList _ _ = Nothing
map :: forall f g xs
. (forall a . f a -> g a)
-> TypedList f xs
-> TypedList g xs
map k = coerce (Prelude.map k')
where
k' :: Any -> Any
k' = unsafeCoerce k
{-# INLINE map #-}
types :: forall f xs
. TypedList f xs -> TypeList xs
types = Numeric.TypedList.map (const Proxy)
{-# INLINE types #-}
typeables :: forall xs . Typeable xs => TypeList xs
typeables = case R.typeRep @xs of
R.App (R.App _ (_ :: R.TypeRep (n :: k))) (txs :: R.TypeRep (ns :: ks))
| Dict <- unsafeCoerce (Dict @(k ~ k, ks ~ ks))
:: Dict (k ~ KindOfEl xs, ks ~ KindOf xs)
, Dict <- unsafeEqTypes @xs @(n ': ns)
-> Proxy @n :* R.withTypeable txs (typeables @ns)
R.Con _
-> unsafeCoerce U
r -> error ("typeables -- impossible typeRep: " ++ show r)
{-# INLINE typeables #-}
inferTypeableList :: forall f xs
. (Typeable (KindOfEl xs), All Typeable xs)
=> TypedList f xs -> Dict (Typeable xs)
inferTypeableList U = Dict
inferTypeableList (_ :* xs) = case inferTypeableList xs of Dict -> Dict
class RepresentableList xs where
tList :: TypeList xs
instance RepresentableList ('[] :: [k]) where
tList = U
instance RepresentableList xs => RepresentableList (x ': xs :: [k]) where
tList = Proxy @x :* tList @xs
typedListShowsPrecC :: forall c f xs
. All c xs
=> String
-> ( forall x . c x => Int -> f x -> ShowS )
-> Int -> TypedList f xs -> ShowS
typedListShowsPrecC _ _ _ U = showChar 'U'
typedListShowsPrecC consS elShowsPrec p (x :* xs) = showParen (p >= 6)
$ elShowsPrec 6 x
. showChar ' ' . showString consS . showChar ' '
. typedListShowsPrecC @c @f consS elShowsPrec 5 xs
typedListShowsPrec :: forall f xs
. ( forall x . Int -> f x -> ShowS )
-> Int -> TypedList f xs -> ShowS
typedListShowsPrec _ _ U = showChar 'U'
typedListShowsPrec elShowsPrec p (x :* xs) = showParen (p >= 6) $
elShowsPrec 6 x . showString " :* " . typedListShowsPrec @f elShowsPrec 5 xs
typedListReadPrec :: forall c f xs g
. All c xs
=> String
-> ( forall x . c x => Read.ReadPrec (f x) )
-> TypedList g xs
-> Read.ReadPrec (TypedList f xs)
typedListReadPrec _ _ U = Read.parens $ U <$ Read.lift (Read.expect $ Read.Ident "U")
typedListReadPrec consS elReadPrec (_ :* ts) = Read.parens . Read.prec 5 $ do
x <- Read.step elReadPrec
Read.lift . Read.expect $ Read.Symbol consS
xs <- typedListReadPrec @c consS elReadPrec ts
return (x :* xs)
withTypedListReadPrec :: forall f (r :: Type)
. (forall (z :: Type) .
( forall x . f x -> z) -> Read.ReadPrec z )
-> (forall xs . TypedList f xs -> r )
-> Read.ReadPrec r
withTypedListReadPrec withElReadPrec use = Read.parens $
(use U <$ Read.lift (Read.expect $ Read.Ident "U"))
Read.+++
Read.prec 5 (do
WithAnyTL withX <- Read.step $ withElReadPrec (\x -> WithAnyTL $ use . (x :*))
Read.lift . Read.expect $ Read.Symbol ":*"
withTypedListReadPrec @f @r withElReadPrec withX
)
newtype WithAnyTL (f :: k -> Type) (r :: Type)
= WithAnyTL (forall (xs :: [k]) . TypedList f xs -> r)
reifyRepList :: forall (k :: Type) (xs :: [k]) (r :: Type)
. 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 :: k -> Type) (xs :: [k])
= forall (sx :: [k]) . ReverseList xs sx => PatReverse (TypedList f sx)
unreverseTL :: forall (k :: Type) (f :: k -> Type) (xs :: [k])
. TypedList f xs -> PatReverse f xs
unreverseTL xs
= case unsafeEqTypes @xs @(Reverse (Reverse xs)) of
Dict -> PatReverse @k @f @xs @(Reverse xs) (Numeric.TypedList.reverse xs)
{-# INLINE unreverseTL #-}
mkRTL :: forall (k :: Type) (xs :: [k])
. TypeList xs
-> Dict (RepresentableList xs)
mkRTL xs = reifyRepList xs Dict
{-# INLINE mkRTL #-}
data PatSnoc (f :: k -> Type) (xs :: [k]) where
PatSNil :: PatSnoc f '[]
PatSnoc :: SnocList xs s xss => TypedList f xs -> f s -> PatSnoc f xss
unsnocTL :: forall (k :: Type) (f :: k -> Type) (xs :: [k])
. TypedList f xs -> PatSnoc f xs
unsnocTL (TypedList [])
= case unsafeEqTypes @xs @'[] of
Dict -> PatSNil
unsnocTL (TypedList (x:xs))
= case unsafeEqTypes @xs @(Init xs +: Last xs) of
Dict -> PatSnoc (coerce sy) (unsafeCoerce y)
where
(sy, y) = unsnoc x xs
unsnoc :: Any -> [Any] -> ([Any], Any)
unsnoc t [] = ([], t)
unsnoc t (z:zs) = first (t:) (unsnoc z zs)
{-# INLINE unsnocTL #-}
data PatCons (f :: k -> Type) (xs :: [k]) where
PatCNil :: PatCons f '[]
PatCons :: f y -> TypedList f ys -> PatCons f (y ': ys)
patTL :: forall (k :: Type) (f :: k -> Type) (xs :: [k])
. TypedList f xs -> PatCons f xs
patTL (TypedList [])
= case unsafeEqTypes @xs @'[] of
Dict -> PatCNil
patTL (TypedList (x : xs))
= case unsafeEqTypes @xs @(Head xs ': Tail xs) of
Dict -> PatCons (unsafeCoerce x) (coerce xs)
{-# INLINE patTL #-}
mkEVL :: forall (k :: Type) (c :: k -> Constraint) (xs :: [k])
. DictList c xs -> Dict (All c xs, RepresentableList xs)
mkEVL U = Dict
mkEVL (Dict1 :* evs) = case mkEVL evs of Dict -> Dict
_evList :: forall (k :: Type) (c :: k -> Constraint) (xs :: [k]) (f :: (k -> Type))
. All c xs => TypedList f xs -> DictList c xs
_evList U = U
_evList (_ :* xs) = case _evList xs of evs -> Dict1 :* evs
dimValInt :: forall (k :: Type) (x :: k) . Dim x -> Int
dimValInt = fromIntegral . dimVal