{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ViewPatterns #-} ----------------------------------------------------------------------------- -- | -- Module : Numeric.TypedList -- Copyright : (c) Artem Chirkin -- License : BSD3 -- -- -- Provide a type-indexed heterogeneous list type @TypedList@. -- Behind the facade, @TypedList@ is just a plain list of haskell pointers. -- It is used to represent dimension lists, indices, and just flexible tuples. -- -- Most of type-level functionality is implemented using GADT-like pattern synonyms. -- Import this module qualified to use list-like functionality. -- ----------------------------------------------------------------------------- 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 -- * Deriving Show and Read , 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) -- | Type-indexed list newtype TypedList (f :: (k -> Type)) (xs :: [k]) = TypedList [Any] deriving (Typeable) type role TypedList representational representational {-# COMPLETE TypeList #-} {-# COMPLETE EvList #-} {-# COMPLETE U, (:*) #-} {-# COMPLETE U, Cons #-} {-# COMPLETE U, Snoc #-} {-# COMPLETE Empty, (:*) #-} {-# COMPLETE Empty, Cons #-} {-# COMPLETE Empty, Snoc #-} {-# COMPLETE Reverse #-} -- | Term-level structure of a @TypedList f xs@ is fully determined by its -- type @Typeable xs@. -- Thus, @gunfold@ does not use its last argument (@Constr@) at all, -- relying on the structure of the type parameter. instance (Typeable k, Typeable f, Typeable xs, All Data (Map f xs)) => Data (TypedList (f :: (k -> Type)) (xs :: [k])) where gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypedList f xs -> c (TypedList f xs) gfoldl forall d b. Data d => c (d -> b) -> d -> c b _ forall g. g -> c g z TypedList f xs U = TypedList f xs -> c (TypedList f xs) forall g. g -> c g z TypedList f xs forall k (f :: k -> *) (xs :: [k]). (xs ~ '[]) => TypedList f xs U gfoldl forall d b. Data d => c (d -> b) -> d -> c b k forall g. g -> c g z (f y x :* TypedList f ys xs) = case forall (x :: k) (xs :: [k]). (Typeable xs, xs ~ (x : xs)) => Dict (Typeable x, Typeable xs) forall k (ys :: [k]) (x :: k) (xs :: [k]). (Typeable ys, ys ~ (x : xs)) => Dict (Typeable x, Typeable xs) inferTypeableCons @xs of Dict (Typeable y, Typeable ys) Dict -> (f y -> TypedList f ys -> TypedList f xs) -> c (f y -> TypedList f ys -> TypedList f xs) forall g. g -> c g z f y -> TypedList f ys -> TypedList f xs forall k (f :: k -> *) (xs :: [k]) (y :: k) (ys :: [k]). (xs ~ (y : ys)) => f y -> TypedList f ys -> TypedList f xs (:*) c (f y -> TypedList f ys -> TypedList f xs) -> f y -> c (TypedList f ys -> TypedList f xs) forall d b. Data d => c (d -> b) -> d -> c b `k` f y x c (TypedList f ys -> TypedList f xs) -> TypedList f ys -> c (TypedList f xs) forall d b. Data d => c (d -> b) -> d -> c b `k` TypedList f ys xs gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TypedList f xs) gunfold forall b r. Data b => c (b -> r) -> c r k forall r. r -> c r z Constr _ = case Typeable xs => TypeList xs forall k (xs :: [k]). Typeable xs => TypeList xs typeables @xs of TypeList xs U -> TypedList f xs -> c (TypedList f xs) forall r. r -> c r z TypedList f xs forall k (f :: k -> *) (xs :: [k]). (xs ~ '[]) => TypedList f xs U Proxy y _ :* TypedList Proxy ys _ -> case forall (x :: k) (xs :: [k]). (Typeable xs, xs ~ (x : xs)) => Dict (Typeable x, Typeable xs) forall k (ys :: [k]) (x :: k) (xs :: [k]). (Typeable ys, ys ~ (x : xs)) => Dict (Typeable x, Typeable xs) inferTypeableCons @xs of Dict (Typeable y, Typeable ys) Dict -> c (TypedList f ys -> TypedList f xs) -> c (TypedList f xs) forall b r. Data b => c (b -> r) -> c r k (c (f y -> TypedList f ys -> TypedList f xs) -> c (TypedList f ys -> TypedList f xs) forall b r. Data b => c (b -> r) -> c r k ((f y -> TypedList f ys -> TypedList f xs) -> c (f y -> TypedList f ys -> TypedList f xs) forall r. r -> c r z f y -> TypedList f ys -> TypedList f xs forall k (f :: k -> *) (xs :: [k]) (y :: k) (ys :: [k]). (xs ~ (y : ys)) => f y -> TypedList f ys -> TypedList f xs (:*))) toConstr :: TypedList f xs -> Constr toConstr TypedList f xs U = Constr typedListConstrEmpty toConstr (f y _ :* TypedList f ys _) = Constr typedListConstrCons dataTypeOf :: TypedList f xs -> DataType dataTypeOf TypedList f xs _ = DataType typedListDataType typedListDataType :: DataType typedListDataType :: DataType typedListDataType = String -> [Constr] -> DataType mkDataType String "Numeric.TypedList.TypedList" [Constr typedListConstrEmpty, Constr typedListConstrCons] typedListConstrEmpty :: Constr typedListConstrEmpty :: Constr typedListConstrEmpty = DataType -> String -> [String] -> Fixity -> Constr mkConstr DataType typedListDataType String "U" [] Fixity Prefix typedListConstrCons :: Constr typedListConstrCons :: Constr typedListConstrCons = DataType -> String -> [String] -> Fixity -> Constr mkConstr DataType typedListDataType String ":*" [] Fixity 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 :: TypedList f xs -> Rep (TypedList f xs) x from TypedList f xs U = (:+:) (M1 C ('MetaCons "U" 'PrefixI 'False) U1) (Rec0 Void) x -> M1 D ('MetaData "TypedList" "Numeric.TypedList" "dimensions" 'False) (M1 C ('MetaCons "U" 'PrefixI 'False) U1 :+: Rec0 Void) x forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p M1 (M1 C ('MetaCons "U" 'PrefixI 'False) U1 x -> (:+:) (M1 C ('MetaCons "U" 'PrefixI 'False) U1) (Rec0 Void) x forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p L1 (U1 x -> M1 C ('MetaCons "U" 'PrefixI 'False) U1 x forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p M1 U1 x forall k (p :: k). U1 p U1)) from (f y x :* TypedList f ys xs) = (:+:) (Rec0 Void) (M1 C ('MetaCons ":*" ('InfixI 'RightAssociative 5) 'False) (M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (K1 R (f y)) :*: M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (K1 R (TypedList f ys)))) x -> M1 D ('MetaData "TypedList" "Numeric.TypedList" "dimensions" 'False) (Rec0 Void :+: M1 C ('MetaCons ":*" ('InfixI 'RightAssociative 5) 'False) (M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (K1 R (f y)) :*: M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (K1 R (TypedList f ys)))) x forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p M1 (M1 C ('MetaCons ":*" ('InfixI 'RightAssociative 5) 'False) (M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (K1 R (f y)) :*: M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (K1 R (TypedList f ys))) x -> (:+:) (Rec0 Void) (M1 C ('MetaCons ":*" ('InfixI 'RightAssociative 5) 'False) (M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (K1 R (f y)) :*: M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (K1 R (TypedList f ys)))) x forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p R1 ((:*:) (M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (K1 R (f y))) (M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (K1 R (TypedList f ys))) x -> M1 C ('MetaCons ":*" ('InfixI 'RightAssociative 5) 'False) (M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (K1 R (f y)) :*: M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (K1 R (TypedList f ys))) x forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p M1 (K1 R (f y) x -> M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (K1 R (f y)) x forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p M1 (f y -> K1 R (f y) x forall k i c (p :: k). c -> K1 i c p K1 f y x) M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (K1 R (f y)) x -> M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (K1 R (TypedList f ys)) x -> (:*:) (M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (K1 R (f y))) (M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (K1 R (TypedList f ys))) x forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> g p -> (:*:) f g p :*: K1 R (TypedList f ys) x -> M1 S ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (K1 R (TypedList f ys)) x forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p M1 (TypedList f ys -> K1 R (TypedList f ys) x forall k i c (p :: k). c -> K1 i c p K1 TypedList f ys xs)))) to :: Rep (TypedList f xs) x -> TypedList f xs to (M1 (L1 _)) | Dict (xs ~ '[]) Dict <- Dict (xs ~ '[]) forall k (a :: k) (b :: k). Dict (a ~ b) unsafeEqTypes @xs @'[] = TypedList f xs forall k (f :: k -> *) (xs :: [k]). (xs ~ '[]) => TypedList f xs U to (M1 (R1 xxs)) | Dict (xs ~ (Head xs : Tail xs)) Dict <- Dict (xs ~ (Head xs : Tail xs)) forall k (a :: k) (b :: k). Dict (a ~ b) unsafeEqTypes @xs @(Head xs ': Tail xs) , M1 (M1 (K1 x) :*: M1 (K1 xs)) <- TypedListRepCons f xs x xxs = f (Head xs) x f (Head xs) -> TypedList f (Tail xs) -> TypedList f xs forall k (f :: k -> *) (xs :: [k]) (y :: k) (ys :: [k]). (xs ~ (y : ys)) => f y -> TypedList f ys -> TypedList f xs :* TypedList f (Tail xs) xs -- | A list of type proxies type TypeList = (TypedList Proxy :: [k] -> Type) -- | Same as `Dict`, but allows to separate constraint function from -- the type it is applied to. 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 :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Dict1 p a -> c (Dict1 p a) gfoldl forall d b. Data d => c (d -> b) -> d -> c b _ forall g. g -> c g z Dict1 p a Dict1 = Dict1 p a -> c (Dict1 p a) forall g. g -> c g z Dict1 p a forall k (c :: k -> Constraint) (a :: k). c a => Dict1 c a Dict1 toConstr :: Dict1 p a -> Constr toConstr Dict1 p a _ = Constr dictConstr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Dict1 p a) gunfold forall b r. Data b => c (b -> r) -> c r _ forall r. r -> c r z Constr _ = Dict1 p a -> c (Dict1 p a) forall r. r -> c r z Dict1 p a forall k (c :: k -> Constraint) (a :: k). c a => Dict1 c a Dict1 dataTypeOf :: Dict1 p a -> DataType dataTypeOf Dict1 p a _ = DataType dictDataType dictConstr :: Constr dictConstr :: Constr dictConstr = DataType -> String -> [String] -> Fixity -> Constr mkConstr DataType dictDataType String "Dict1" [] Fixity Prefix dictDataType :: DataType dictDataType :: DataType dictDataType = String -> [Constr] -> DataType mkDataType String "Numeric.TypedList.Dict1" [Constr 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)) -- | A list of dicts for the same constraint over several types. type DictList (c :: k -> Constraint) = (TypedList (Dict1 c) :: [k] -> Type) -- | Pattern matching against this causes `RepresentableList` instance -- come into scope. -- Also it allows constructing a term-level list out of a constraint. pattern TypeList :: forall xs . () => RepresentableList xs => TypeList xs pattern $bTypeList :: TypeList xs $mTypeList :: forall r k (xs :: [k]). TypeList xs -> (RepresentableList xs => r) -> (Void# -> r) -> r TypeList <- (mkRTL -> Dict) where TypeList = RepresentableList xs => TypeList xs forall k (xs :: [k]). RepresentableList xs => TypeList xs tList @xs -- | Pattern matching against this allows manipulating lists of constraints. -- Useful when creating functions that change the shape of dimensions. pattern EvList :: forall c xs . () => (All c xs, RepresentableList xs) => DictList c xs pattern $bEvList :: DictList c xs $mEvList :: forall r k (c :: k -> Constraint) (xs :: [k]). DictList c xs -> ((All c xs, RepresentableList xs) => r) -> (Void# -> r) -> r EvList <- (mkEVL -> Dict) where EvList = TypedList Proxy xs -> DictList c xs forall k (c :: k -> Constraint) (xs :: [k]) (f :: k -> *). All c xs => TypedList f xs -> DictList c xs _evList (RepresentableList xs => TypedList Proxy xs forall k (xs :: [k]). RepresentableList xs => TypeList xs tList @xs) -- | Zero-length type list pattern U :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) . () => (xs ~ '[]) => TypedList f xs pattern $bU :: TypedList f xs $mU :: forall r k (f :: k -> *) (xs :: [k]). TypedList f xs -> ((xs ~ '[]) => r) -> (Void# -> r) -> r U <- (patTL @k @f @xs -> PatCNil) where U = [Any] -> TypedList f xs coerce ([] :: [Any]) -- | Zero-length type list; synonym to `U`. pattern Empty :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) . () => (xs ~ '[]) => TypedList f xs pattern $bEmpty :: TypedList f xs $mEmpty :: forall r k (f :: k -> *) (xs :: [k]). TypedList f xs -> ((xs ~ '[]) => r) -> (Void# -> r) -> r Empty = U -- | Constructing a type-indexed list pattern (:*) :: forall f xs . () => forall y ys . (xs ~ (y ': ys)) => f y -> TypedList f ys -> TypedList f xs pattern $b:* :: f y -> TypedList f ys -> TypedList f xs $m:* :: forall r k (f :: k -> *) (xs :: [k]). TypedList f xs -> (forall (y :: k) (ys :: [k]). (xs ~ (y : ys)) => f y -> TypedList f ys -> r) -> (Void# -> r) -> r (:*) x xs = Cons x xs infixr 5 :* -- | Constructing a type-indexed list in the canonical way pattern Cons :: forall f xs . () => forall y ys . (xs ~ (y ': ys)) => f y -> TypedList f ys -> TypedList f xs pattern $bCons :: f y -> TypedList f ys -> TypedList f xs $mCons :: forall r k (f :: k -> *) (xs :: [k]). TypedList f xs -> (forall (y :: k) (ys :: [k]). (xs ~ (y : ys)) => f y -> TypedList f ys -> r) -> (Void# -> r) -> r Cons x xs <- (patTL @_ @f @xs -> PatCons x xs) where Cons = f y -> TypedList f ys -> TypedList f xs forall k (f :: k -> *) (x :: k) (xs :: [k]). f x -> TypedList f xs -> TypedList f (x :+ xs) Numeric.TypedList.cons -- | Constructing a type-indexed list from the other end pattern Snoc :: forall f xs . () => forall sy y . SnocList sy y xs => TypedList f sy -> f y -> TypedList f xs pattern $bSnoc :: TypedList f sy -> f y -> TypedList f xs $mSnoc :: forall r k (f :: k -> *) (xs :: [k]). TypedList f xs -> (forall (sy :: [k]) (y :: k). SnocList sy y xs => TypedList f sy -> f y -> r) -> (Void# -> r) -> r Snoc sx x <- (unsnocTL @_ @f @xs -> PatSnoc sx x) where Snoc = TypedList f sy -> f y -> TypedList f xs forall k (f :: k -> *) (xs :: [k]) (x :: k). TypedList f xs -> f x -> TypedList f (xs +: x) Numeric.TypedList.snoc -- | Reverse a typed list pattern Reverse :: forall f xs . () => forall sx . ReverseList xs sx => TypedList f sx -> TypedList f xs pattern $bReverse :: TypedList f sx -> TypedList f xs $mReverse :: forall r k (f :: k -> *) (xs :: [k]). TypedList f xs -> (forall (sx :: [k]). ReverseList xs sx => TypedList f sx -> r) -> (Void# -> r) -> r Reverse sx <- (unreverseTL @_ @f @xs -> PatReverse sx) where Reverse = TypedList f sx -> TypedList f xs forall k (f :: k -> *) (xs :: [k]). TypedList f xs -> TypedList f (Reverse xs) Numeric.TypedList.reverse -- | /O(1)/ append an element in front of a @TypedList@ (same as `(:)` for lists). cons :: forall f x xs . f x -> TypedList f xs -> TypedList f (x :+ xs) cons :: f x -> TypedList f xs -> TypedList f (x :+ xs) cons f x x TypedList f xs xs = [Any] -> TypedList f (x :+ xs) forall k (f :: k -> *) (xs :: [k]). [Any] -> TypedList f xs TypedList (f x -> Any forall a b. a -> b unsafeCoerce f x x Any -> [Any] -> [Any] forall a. a -> [a] -> [a] : TypedList f xs -> [Any] coerce TypedList f xs xs) {-# INLINE cons #-} -- | /O(n)/ append an element to the end of a @TypedList@. snoc :: forall f xs x . TypedList f xs -> f x -> TypedList f (xs +: x) snoc :: TypedList f xs -> f x -> TypedList f (xs +: x) snoc TypedList f xs xs f x x = [Any] -> TypedList f (xs +: x) forall k (f :: k -> *) (xs :: [k]). [Any] -> TypedList f xs TypedList (TypedList f xs -> [Any] coerce TypedList f xs xs [Any] -> [Any] -> [Any] forall a. [a] -> [a] -> [a] ++ [f x -> Any forall a b. a -> b unsafeCoerce f x x]) {-# INLINE snoc #-} -- | /O(n)/ return elements of a @TypedList@ in reverse order. reverse :: forall f xs . TypedList f xs -> TypedList f (Reverse xs) reverse :: TypedList f xs -> TypedList f (Reverse xs) reverse = ([Any] -> [Any]) -> TypedList f xs -> TypedList f (Reverse xs) coerce ([Any] -> [Any] forall a. [a] -> [a] Prelude.reverse :: [Any] -> [Any]) {-# INLINE reverse #-} -- | /O(1)/ Extract the first element of a @TypedList@, which must be non-empty. head :: forall f xs . TypedList f xs -> f (Head xs) head :: TypedList f xs -> f (Head xs) head (TypedList [Any] xs) = Any -> f (Head xs) forall a b. a -> b unsafeCoerce ([Any] -> Any forall a. [a] -> a Prelude.head [Any] xs) {-# INLINE head #-} -- | /O(1)/ Extract the elements after the head of a @TypedList@, -- which must be non-empty. tail :: forall f xs . TypedList f xs -> TypedList f (Tail xs) tail :: TypedList f xs -> TypedList f (Tail xs) tail = ([Any] -> [Any]) -> TypedList f xs -> TypedList f (Tail xs) coerce ([Any] -> [Any] forall a. [a] -> [a] Prelude.tail :: [Any] -> [Any]) {-# INLINE tail #-} -- | /O(n)/ Return all the elements of a @TypedList@ except the last one -- (the list must be non-empty). init :: forall f xs . TypedList f xs -> TypedList f (Init xs) init :: TypedList f xs -> TypedList f (Init xs) init = ([Any] -> [Any]) -> TypedList f xs -> TypedList f (Init xs) coerce ([Any] -> [Any] forall a. [a] -> [a] Prelude.init :: [Any] -> [Any]) {-# INLINE init #-} -- | /O(n)/ Extract the last element of a @TypedList@, which must be non-empty. last :: forall f xs . TypedList f xs -> f (Last xs) last :: TypedList f xs -> f (Last xs) last (TypedList [Any] xs) = Any -> f (Last xs) forall a b. a -> b unsafeCoerce ([Any] -> Any forall a. [a] -> a Prelude.last [Any] xs) {-# INLINE last #-} -- | /O(min(n,k))/ @take k xs@ returns a prefix of @xs@ of length @min(length xs, k)@. -- It calls `Prelude.take` under the hood, so expect the same behavior. take :: forall (n :: Nat) f xs . Dim n -> TypedList f xs -> TypedList f (Take n xs) take :: Dim n -> TypedList f xs -> TypedList f (Take n xs) take = (Dim n -> [Any] -> [Any]) -> Dim n -> TypedList f xs -> TypedList f (Take n xs) coerce (Int -> [Any] -> [Any] forall a. Int -> [a] -> [a] Prelude.take (Int -> [Any] -> [Any]) -> (Dim n -> Int) -> Dim n -> [Any] -> [Any] forall b c a. (b -> c) -> (a -> b) -> a -> c . Dim n -> Int forall k (x :: k). Dim x -> Int dimValInt :: Dim n -> [Any] -> [Any]) {-# INLINE take #-} -- | /O(min(n,k))/ @drop k xs@ returns a suffix of @xs@ of length @max(0, length xs - k)@. -- It calls `Prelude.drop` under the hood, so expect the same behavior. drop :: forall (n :: Nat) f xs . Dim n -> TypedList f xs -> TypedList f (Drop n xs) drop :: Dim n -> TypedList f xs -> TypedList f (Drop n xs) drop = (Dim n -> [Any] -> [Any]) -> Dim n -> TypedList f xs -> TypedList f (Drop n xs) coerce (Int -> [Any] -> [Any] forall a. Int -> [a] -> [a] Prelude.drop (Int -> [Any] -> [Any]) -> (Dim n -> Int) -> Dim n -> [Any] -> [Any] forall b c a. (b -> c) -> (a -> b) -> a -> c . Dim n -> Int forall k (x :: k). Dim x -> Int dimValInt :: Dim n -> [Any] -> [Any]) {-# INLINE drop #-} -- | Return the number of elements in a @TypedList@ (same as `order`). length :: forall f xs . TypedList f xs -> Dim (Length xs) length :: TypedList f xs -> Dim (Length xs) length = TypedList f xs -> Dim (Length xs) forall k (f :: k -> *) (xs :: [k]). TypedList f xs -> Dim (Length xs) order {-# INLINE length #-} -- | /O(min(n,k))/ @splitAt k xs@ has the same effect as @('take' k xs, 'drop' k xs)@. -- It calls `Prelude.splitAt` under the hood, so expect the same behavior. splitAt :: forall (n :: Nat) f xs . Dim n -> TypedList f xs -> (TypedList f (Take n xs), TypedList f (Drop n xs)) splitAt :: Dim n -> TypedList f xs -> (TypedList f (Take n xs), TypedList f (Drop n xs)) splitAt = (Dim n -> [Any] -> ([Any], [Any])) -> Dim n -> TypedList f xs -> (TypedList f (Take n xs), TypedList f (Drop n xs)) coerce (Int -> [Any] -> ([Any], [Any]) forall a. Int -> [a] -> ([a], [a]) Prelude.splitAt (Int -> [Any] -> ([Any], [Any])) -> (Dim n -> Int) -> Dim n -> [Any] -> ([Any], [Any]) forall b c a. (b -> c) -> (a -> b) -> a -> c . Dim n -> Int forall k (x :: k). Dim x -> Int dimValInt :: Dim n -> [Any] -> ([Any], [Any])) {-# INLINE splitAt #-} -- | Return the number of elements in a type list @xs@ bound by a constraint -- @RepresentableList xs@ (same as `order`, but takes no value arguments). order' :: forall xs . RepresentableList xs => Dim (Length xs) order' :: Dim (Length xs) order' = TypedList Proxy xs -> Dim (Length xs) forall k (f :: k -> *) (xs :: [k]). TypedList f xs -> Dim (Length xs) order (RepresentableList xs => TypedList Proxy xs forall k (xs :: [k]). RepresentableList xs => TypeList xs tList @xs) {-# INLINE order' #-} -- | Return the number of elements in a @TypedList@ (same as `length`). order :: forall f xs . TypedList f xs -> Dim (Length xs) order :: TypedList f xs -> Dim (Length xs) order = ([Any] -> Word) -> TypedList f xs -> Dim (Length xs) forall a b. a -> b unsafeCoerce (Int -> Word forall a b. (Integral a, Num b) => a -> b fromIntegral (Int -> Word) -> ([Any] -> Int) -> [Any] -> Word forall b c a. (b -> c) -> (a -> b) -> a -> c . [Any] -> Int forall (t :: * -> *) a. Foldable t => t a -> Int Prelude.length :: [Any] -> Word) {-# INLINE order #-} -- | Concat two @TypedList@s. -- It calls `Prelude.(++)` under the hood, so expect the same behavior. concat :: forall f xs ys . TypedList f xs -> TypedList f ys -> TypedList f (xs ++ ys) concat :: TypedList f xs -> TypedList f ys -> TypedList f (xs ++ ys) concat = ([Any] -> [Any] -> [Any]) -> TypedList f xs -> TypedList f ys -> TypedList f (xs ++ ys) coerce ([Any] -> [Any] -> [Any] forall a. [a] -> [a] -> [a] (++) :: [Any] -> [Any] -> [Any]) {-# INLINE concat #-} -- | Drops the given prefix from a @TypedList@. -- It returns 'Nothing' if the @TypedList@ does not start with the prefix -- given, or 'Just' the @TypedList@ after the prefix, if it does. -- It calls `Prelude.stripPrefix` under the hood, so expect the same behavior. -- -- This function can be used to find the type-level evidence that one type-level -- list is indeed a prefix of another. 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 :: TypedList f xs -> TypedList f ys -> Maybe (TypedList f (StripPrefix xs ys)) stripPrefix TypedList f xs U TypedList f ys ys = TypedList f ys -> Maybe (TypedList f ys) forall a. a -> Maybe a Just TypedList f ys ys stripPrefix TypedList f xs _ TypedList f ys U = Maybe (TypedList f (StripPrefix xs ys)) forall a. Maybe a Nothing stripPrefix ((f y x :: f x) :* TypedList f ys xs) ((f y y :: f y) :* TypedList f ys ys) | Just y :~: y Refl <- (Typeable y, Typeable y) => Maybe (y :~: y) forall k (a :: k) (b :: k). (Typeable a, Typeable b) => Maybe (a :~: b) eqT @x @y , f y x f y -> f y -> Bool forall a. Eq a => a -> a -> Bool == f y f y y = Maybe (TypedList f (StripPrefix ys ys)) -> Maybe (TypedList f (StripPrefix (y : ys) (y : ys))) coerce (TypedList f ys -> TypedList f ys -> Maybe (TypedList f (StripPrefix ys ys)) forall k (f :: k -> *) (xs :: [k]) (ys :: [k]). (All Typeable xs, All Typeable ys, All Eq (Map f xs)) => TypedList f xs -> TypedList f ys -> Maybe (TypedList f (StripPrefix xs ys)) stripPrefix TypedList f ys xs TypedList f ys ys) | Bool otherwise = Maybe (TypedList f (StripPrefix xs ys)) forall a. Maybe a Nothing {-# INLINE stripPrefix #-} -- | Drops the given suffix from a @TypedList@. -- It returns 'Nothing' if the @TypedList@ does not end with the suffix -- given, or 'Just' the @TypedList@ before the suffix, if it does. -- -- This function can be used to find the type-level evidence that one type-level -- list is indeed a suffix of another. 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 :: TypedList f xs -> TypedList f ys -> Maybe (TypedList f (StripSuffix xs ys)) stripSuffix TypedList f xs U TypedList f ys ys = TypedList f ys -> Maybe (TypedList f ys) forall a. a -> Maybe a Just TypedList f ys ys stripSuffix TypedList f xs _ TypedList f ys U = Maybe (TypedList f (StripSuffix xs ys)) forall a. Maybe a Nothing stripSuffix TypedList f xs xs TypedList f ys ys | Just Dim (Length ys - Length xs) n <- TypedList f ys -> Dim (Length ys) forall k (f :: k -> *) (xs :: [k]). TypedList f xs -> Dim (Length xs) order TypedList f ys ys Dim (Length ys) -> Dim (Length xs) -> Maybe (Dim (Length ys - Length xs)) forall (n :: Nat) (m :: Nat). Dim n -> Dim m -> Maybe (Dim (n - m)) `minusDimM` TypedList f xs -> Dim (Length xs) forall k (f :: k -> *) (xs :: [k]). TypedList f xs -> Dim (Length xs) order TypedList f xs xs , (TypedList f (Take (Length ys - Length xs) ys) zs, TypedList f (Drop (Length ys - Length xs) ys) xs') <- Dim (Length ys - Length xs) -> TypedList f ys -> (TypedList f (Take (Length ys - Length xs) ys), TypedList f (Drop (Length ys - Length xs) ys)) forall k (n :: Nat) (f :: k -> *) (xs :: [k]). Dim n -> TypedList f xs -> (TypedList f (Take n xs), TypedList f (Drop n xs)) Numeric.TypedList.splitAt Dim (Length ys - Length xs) n TypedList f ys ys , TypedList (Dict1 Typeable) (Drop (Length ys - Length xs) ys) EvList <- Dim (Length ys - Length xs) -> TypedList (Dict1 Typeable) ys -> TypedList (Dict1 Typeable) (Drop (Length ys - Length xs) ys) forall k (n :: Nat) (f :: k -> *) (xs :: [k]). Dim n -> TypedList f xs -> TypedList f (Drop n xs) Numeric.TypedList.drop Dim (Length ys - Length xs) n (TypedList (Dict1 Typeable) ys -> TypedList (Dict1 Typeable) (Drop (Length ys - Length xs) ys)) -> TypedList (Dict1 Typeable) ys -> TypedList (Dict1 Typeable) (Drop (Length ys - Length xs) ys) forall a b. (a -> b) -> a -> b $ TypedList f ys -> TypedList (Dict1 Typeable) ys forall k (c :: k -> Constraint) (xs :: [k]) (f :: k -> *). All c xs => TypedList f xs -> DictList c xs _evList @_ @Typeable TypedList f ys ys , Just (xs :~: Drop (Length ys - Length xs) ys Refl, Bool True) <- TypedList f xs -> TypedList f (Drop (Length ys - Length xs) ys) -> Maybe (xs :~: Drop (Length ys - Length xs) ys, Bool) forall k (f :: k -> *) (xs :: [k]) (ys :: [k]). (All Typeable xs, All Typeable ys, All Eq (Map f xs)) => TypedList f xs -> TypedList f ys -> Maybe (xs :~: ys, Bool) sameList TypedList f xs xs TypedList f (Drop (Length ys - Length xs) ys) xs' = TypedList f (StripSuffix xs ys) -> Maybe (TypedList f (StripSuffix xs ys)) forall a. a -> Maybe a Just (TypedList f (Take (Length ys - Length xs) ys) -> TypedList f (StripSuffix xs ys) coerce TypedList f (Take (Length ys - Length xs) ys) zs) | Bool otherwise = Maybe (TypedList f (StripSuffix xs ys)) forall a. Maybe a Nothing {-# INLINE stripSuffix #-} -- | Returns two things at once: -- (Evidence that types of lists match, value-level equality). 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 :: TypedList f xs -> TypedList f ys -> Maybe (xs :~: ys, Bool) sameList TypedList f xs U TypedList f ys U = (xs :~: xs, Bool) -> Maybe (xs :~: xs, Bool) forall a. a -> Maybe a Just (xs :~: xs forall k (a :: k). a :~: a Refl, Bool True) sameList ((f y x :: f x) :* TypedList f ys xs) ((f y y :: f y) :* TypedList f ys ys) | Just y :~: y Refl <- (Typeable y, Typeable y) => Maybe (y :~: y) forall k (a :: k) (b :: k). (Typeable a, Typeable b) => Maybe (a :~: b) eqT @x @y , Just (ys :~: ys Refl, Bool b) <- TypedList f ys -> TypedList f ys -> Maybe (ys :~: ys, Bool) forall k (f :: k -> *) (xs :: [k]) (ys :: [k]). (All Typeable xs, All Typeable ys, All Eq (Map f xs)) => TypedList f xs -> TypedList f ys -> Maybe (xs :~: ys, Bool) sameList TypedList f ys xs TypedList f ys ys = (xs :~: xs, Bool) -> Maybe (xs :~: xs, Bool) forall a. a -> Maybe a Just (xs :~: xs forall k (a :: k). a :~: a Refl, f y x f y -> f y -> Bool forall a. Eq a => a -> a -> Bool == f y f y y Bool -> Bool -> Bool && Bool b) | Bool otherwise = Maybe (xs :~: ys, Bool) forall a. Maybe a Nothing sameList TypedList f xs _ TypedList f ys _ = Maybe (xs :~: ys, Bool) forall a. Maybe a Nothing -- | Map a function over contents of a typed list map :: forall f g xs . (forall a . f a -> g a) -> TypedList f xs -> TypedList g xs map :: (forall (a :: k). f a -> g a) -> TypedList f xs -> TypedList g xs map forall (a :: k). f a -> g a k = ([Any] -> [Any]) -> TypedList f xs -> TypedList g xs coerce ((Any -> Any) -> [Any] -> [Any] forall a b. (a -> b) -> [a] -> [b] Prelude.map Any -> Any k') where k' :: Any -> Any k' :: Any -> Any k' = (f Any -> g Any) -> Any -> Any forall a b. a -> b unsafeCoerce f Any -> g Any forall (a :: k). f a -> g a k {-# INLINE map #-} -- | Get a constructible `TypeList` from any other `TypedList`; -- Pattern matching agains the result brings `RepresentableList` constraint -- into the scope: -- -- > case types ts of TypeList -> ... -- types :: forall f xs . TypedList f xs -> TypeList xs types :: TypedList f xs -> TypeList xs types = (forall (a :: k). f a -> Proxy a) -> TypedList f xs -> TypeList xs forall k (f :: k -> *) (g :: k -> *) (xs :: [k]). (forall (a :: k). f a -> g a) -> TypedList f xs -> TypedList g xs Numeric.TypedList.map (Proxy a -> f a -> Proxy a forall a b. a -> b -> a const Proxy a forall k (t :: k). Proxy t Proxy) {-# INLINE types #-} -- | Construct a @TypeList xs@ if there is an instance of @Typeable xs@ around. -- -- This way, you can always bring `RepresentableList` instance into the scope -- if you have a `Typeable` instance. -- typeables :: forall xs . Typeable xs => TypeList xs typeables :: TypeList xs typeables = case Typeable xs => TypeRep xs forall k (a :: k). Typeable a => TypeRep a R.typeRep @xs of R.App (R.App TypeRep a _ (TypeRep b _ :: R.TypeRep (n :: k))) (TypeRep b txs :: R.TypeRep (ns :: ks)) | Dict (k1 ~ k, k1 ~ [k]) Dict <- Dict (k1 ~ k1, k1 ~ k1) -> Dict (k1 ~ k, k1 ~ [k]) forall a b. a -> b unsafeCoerce ((k1 ~ k1, k1 ~ k1) => Dict (k1 ~ k1, k1 ~ k1) forall (a :: Constraint). a => Dict a Dict @(k ~ k, ks ~ ks)) :: Dict (k ~ KindOfEl xs, ks ~ KindOf xs) , Dict (xs ~ (b : b)) Dict <- Dict (xs ~ (b : b)) forall k (a :: k) (b :: k). Dict (a ~ b) unsafeEqTypes @xs @(n ': ns) -> Proxy b forall k (t :: k). Proxy t Proxy @n Proxy b -> TypedList Proxy b -> TypedList Proxy (b : b) forall k (f :: k -> *) (xs :: [k]) (y :: k) (ys :: [k]). (xs ~ (y : ys)) => f y -> TypedList f ys -> TypedList f xs :* TypeRep b -> (Typeable b => TypedList Proxy b) -> TypedList Proxy b forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r R.withTypeable TypeRep b txs (Typeable b => TypeList b forall k (xs :: [k]). Typeable xs => TypeList xs typeables @ns) R.Con TyCon _ -> TypedList Any '[] -> TypeList xs forall a b. a -> b unsafeCoerce TypedList Any '[] forall k (f :: k -> *) (xs :: [k]). (xs ~ '[]) => TypedList f xs U TypeRep xs r -> String -> TypeList xs forall a. HasCallStack => String -> a error (String "typeables -- impossible typeRep: " String -> ShowS forall a. [a] -> [a] -> [a] ++ TypeRep xs -> String forall a. Show a => a -> String show TypeRep xs r) {-# INLINE typeables #-} -- | If all elements of a @TypedList@ are @Typeable@, -- then the list of these elements is also @Typeable@. inferTypeableList :: forall f xs . (Typeable (KindOfEl xs), All Typeable xs) => TypedList f xs -> Dict (Typeable xs) inferTypeableList :: TypedList f xs -> Dict (Typeable xs) inferTypeableList TypedList f xs U = Dict (Typeable xs) forall (a :: Constraint). a => Dict a Dict inferTypeableList (f y _ :* TypedList f ys xs) = case TypedList f ys -> Dict (Typeable ys) forall k (f :: k -> *) (xs :: [k]). (Typeable k, All Typeable xs) => TypedList f xs -> Dict (Typeable xs) inferTypeableList TypedList f ys xs of Dict (Typeable ys) Dict -> Dict (Typeable xs) forall (a :: Constraint). a => Dict a Dict -- | Representable type lists. -- Allows getting type information about list structure at runtime. class RepresentableList xs where -- | Get type-level constructed list tList :: TypeList xs instance RepresentableList ('[] :: [k]) where tList :: TypeList '[] tList = TypeList '[] forall k (f :: k -> *) (xs :: [k]). (xs ~ '[]) => TypedList f xs U instance RepresentableList xs => RepresentableList (x ': xs :: [k]) where tList :: TypeList (x : xs) tList = Proxy x forall k (t :: k). Proxy t Proxy @x Proxy x -> TypedList Proxy xs -> TypeList (x : xs) forall k (f :: k -> *) (xs :: [k]) (y :: k) (ys :: [k]). (xs ~ (y : ys)) => f y -> TypedList f ys -> TypedList f xs :* RepresentableList xs => TypedList Proxy xs forall k (xs :: [k]). RepresentableList xs => TypeList xs tList @xs -- | Generic show function for a @TypedList@. typedListShowsPrecC :: forall c f xs . All c xs => String -- ^ Override cons symbol -> ( forall x . c x => Int -> f x -> ShowS ) -- ^ How to show a single element -> Int -> TypedList f xs -> ShowS typedListShowsPrecC :: String -> (forall (x :: k). c x => Int -> f x -> ShowS) -> Int -> TypedList f xs -> ShowS typedListShowsPrecC String _ forall (x :: k). c x => Int -> f x -> ShowS _ Int _ TypedList f xs U = Char -> ShowS showChar Char 'U' typedListShowsPrecC String consS forall (x :: k). c x => Int -> f x -> ShowS elShowsPrec Int p (f y x :* TypedList f ys xs) = Bool -> ShowS -> ShowS showParen (Int p Int -> Int -> Bool forall a. Ord a => a -> a -> Bool >= Int 6) (ShowS -> ShowS) -> ShowS -> ShowS forall a b. (a -> b) -> a -> b $ Int -> f y -> ShowS forall (x :: k). c x => Int -> f x -> ShowS elShowsPrec Int 6 f y x ShowS -> ShowS -> ShowS forall b c a. (b -> c) -> (a -> b) -> a -> c . Char -> ShowS showChar Char ' ' ShowS -> ShowS -> ShowS forall b c a. (b -> c) -> (a -> b) -> a -> c . String -> ShowS showString String consS ShowS -> ShowS -> ShowS forall b c a. (b -> c) -> (a -> b) -> a -> c . Char -> ShowS showChar Char ' ' ShowS -> ShowS -> ShowS forall b c a. (b -> c) -> (a -> b) -> a -> c . String -> (forall (x :: k). c x => Int -> f x -> ShowS) -> Int -> TypedList f ys -> ShowS forall k (c :: k -> Constraint) (f :: k -> *) (xs :: [k]). All c xs => String -> (forall (x :: k). c x => Int -> f x -> ShowS) -> Int -> TypedList f xs -> ShowS typedListShowsPrecC @c @f String consS forall (x :: k). c x => Int -> f x -> ShowS elShowsPrec Int 5 TypedList f ys xs -- | Generic show function for a @TypedList@. typedListShowsPrec :: forall f xs . ( forall x . Int -> f x -> ShowS ) -- ^ How to show a single element -> Int -> TypedList f xs -> ShowS typedListShowsPrec :: (forall (x :: k). Int -> f x -> ShowS) -> Int -> TypedList f xs -> ShowS typedListShowsPrec forall (x :: k). Int -> f x -> ShowS _ Int _ TypedList f xs U = Char -> ShowS showChar Char 'U' typedListShowsPrec forall (x :: k). Int -> f x -> ShowS elShowsPrec Int p (f y x :* TypedList f ys xs) = Bool -> ShowS -> ShowS showParen (Int p Int -> Int -> Bool forall a. Ord a => a -> a -> Bool >= Int 6) (ShowS -> ShowS) -> ShowS -> ShowS forall a b. (a -> b) -> a -> b $ Int -> f y -> ShowS forall (x :: k). Int -> f x -> ShowS elShowsPrec Int 6 f y x ShowS -> ShowS -> ShowS forall b c a. (b -> c) -> (a -> b) -> a -> c . String -> ShowS showString String " :* " ShowS -> ShowS -> ShowS forall b c a. (b -> c) -> (a -> b) -> a -> c . (forall (x :: k). Int -> f x -> ShowS) -> Int -> TypedList f ys -> ShowS forall k (f :: k -> *) (xs :: [k]). (forall (x :: k). Int -> f x -> ShowS) -> Int -> TypedList f xs -> ShowS typedListShowsPrec @f forall (x :: k). Int -> f x -> ShowS elShowsPrec Int 5 TypedList f ys xs -- | Generic read function for a @TypedList@. -- Requires a "template" to enforce the structure of the type list. typedListReadPrec :: forall c f xs g . All c xs => String -- ^ Override cons symbol -> ( forall x . c x => Read.ReadPrec (f x) ) -- ^ How to read a single element -> TypedList g xs -- ^ Enforce the type structure of the result -> Read.ReadPrec (TypedList f xs) typedListReadPrec :: String -> (forall (x :: k). c x => ReadPrec (f x)) -> TypedList g xs -> ReadPrec (TypedList f xs) typedListReadPrec String _ forall (x :: k). c x => ReadPrec (f x) _ TypedList g xs U = ReadPrec (TypedList f xs) -> ReadPrec (TypedList f xs) forall a. ReadPrec a -> ReadPrec a Read.parens (ReadPrec (TypedList f xs) -> ReadPrec (TypedList f xs)) -> ReadPrec (TypedList f xs) -> ReadPrec (TypedList f xs) forall a b. (a -> b) -> a -> b $ TypedList f xs forall k (f :: k -> *) (xs :: [k]). (xs ~ '[]) => TypedList f xs U TypedList f xs -> ReadPrec () -> ReadPrec (TypedList f xs) forall (f :: * -> *) a b. Functor f => a -> f b -> f a <$ ReadP () -> ReadPrec () forall a. ReadP a -> ReadPrec a Read.lift (Lexeme -> ReadP () Read.expect (Lexeme -> ReadP ()) -> Lexeme -> ReadP () forall a b. (a -> b) -> a -> b $ String -> Lexeme Read.Ident String "U") typedListReadPrec String consS forall (x :: k). c x => ReadPrec (f x) elReadPrec (g y _ :* TypedList g ys ts) = ReadPrec (TypedList f xs) -> ReadPrec (TypedList f xs) forall a. ReadPrec a -> ReadPrec a Read.parens (ReadPrec (TypedList f xs) -> ReadPrec (TypedList f xs)) -> (ReadPrec (TypedList f xs) -> ReadPrec (TypedList f xs)) -> ReadPrec (TypedList f xs) -> ReadPrec (TypedList f xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . Int -> ReadPrec (TypedList f xs) -> ReadPrec (TypedList f xs) forall a. Int -> ReadPrec a -> ReadPrec a Read.prec Int 5 (ReadPrec (TypedList f xs) -> ReadPrec (TypedList f xs)) -> ReadPrec (TypedList f xs) -> ReadPrec (TypedList f xs) forall a b. (a -> b) -> a -> b $ do f y x <- ReadPrec (f y) -> ReadPrec (f y) forall a. ReadPrec a -> ReadPrec a Read.step ReadPrec (f y) forall (x :: k). c x => ReadPrec (f x) elReadPrec ReadP () -> ReadPrec () forall a. ReadP a -> ReadPrec a Read.lift (ReadP () -> ReadPrec ()) -> (Lexeme -> ReadP ()) -> Lexeme -> ReadPrec () forall b c a. (b -> c) -> (a -> b) -> a -> c . Lexeme -> ReadP () Read.expect (Lexeme -> ReadPrec ()) -> Lexeme -> ReadPrec () forall a b. (a -> b) -> a -> b $ String -> Lexeme Read.Symbol String consS TypedList f ys xs <- String -> (forall (x :: k). c x => ReadPrec (f x)) -> TypedList g ys -> ReadPrec (TypedList f ys) forall k (c :: k -> Constraint) (f :: k -> *) (xs :: [k]) (g :: k -> *). All c xs => String -> (forall (x :: k). c x => ReadPrec (f x)) -> TypedList g xs -> ReadPrec (TypedList f xs) typedListReadPrec @c String consS forall (x :: k). c x => ReadPrec (f x) elReadPrec TypedList g ys ts TypedList f xs -> ReadPrec (TypedList f xs) forall (m :: * -> *) a. Monad m => a -> m a return (f y x f y -> TypedList f ys -> TypedList f xs forall k (f :: k -> *) (xs :: [k]) (y :: k) (ys :: [k]). (xs ~ (y : ys)) => f y -> TypedList f ys -> TypedList f xs :* TypedList f ys xs) -- | Generic read function for a @TypedList@ of unknown length. withTypedListReadPrec :: forall f (r :: Type) . (forall (z :: Type) . ( forall x . f x -> z) -> Read.ReadPrec z ) -- ^ How to read a single element -> (forall xs . TypedList f xs -> r ) -- ^ Consume the result -> Read.ReadPrec r withTypedListReadPrec :: (forall z. (forall (x :: k). f x -> z) -> ReadPrec z) -> (forall (xs :: [k]). TypedList f xs -> r) -> ReadPrec r withTypedListReadPrec forall z. (forall (x :: k). f x -> z) -> ReadPrec z withElReadPrec forall (xs :: [k]). TypedList f xs -> r use = ReadPrec r -> ReadPrec r forall a. ReadPrec a -> ReadPrec a Read.parens (ReadPrec r -> ReadPrec r) -> ReadPrec r -> ReadPrec r forall a b. (a -> b) -> a -> b $ (TypedList f '[] -> r forall (xs :: [k]). TypedList f xs -> r use TypedList f '[] forall k (f :: k -> *) (xs :: [k]). (xs ~ '[]) => TypedList f xs U r -> ReadPrec () -> ReadPrec r forall (f :: * -> *) a b. Functor f => a -> f b -> f a <$ ReadP () -> ReadPrec () forall a. ReadP a -> ReadPrec a Read.lift (Lexeme -> ReadP () Read.expect (Lexeme -> ReadP ()) -> Lexeme -> ReadP () forall a b. (a -> b) -> a -> b $ String -> Lexeme Read.Ident String "U")) ReadPrec r -> ReadPrec r -> ReadPrec r forall a. ReadPrec a -> ReadPrec a -> ReadPrec a Read.+++ Int -> ReadPrec r -> ReadPrec r forall a. Int -> ReadPrec a -> ReadPrec a Read.prec Int 5 (do WithAnyTL forall (xs :: [k]). TypedList f xs -> r withX <- ReadPrec (WithAnyTL f r) -> ReadPrec (WithAnyTL f r) forall a. ReadPrec a -> ReadPrec a Read.step (ReadPrec (WithAnyTL f r) -> ReadPrec (WithAnyTL f r)) -> ReadPrec (WithAnyTL f r) -> ReadPrec (WithAnyTL f r) forall a b. (a -> b) -> a -> b $ (forall (x :: k). f x -> WithAnyTL f r) -> ReadPrec (WithAnyTL f r) forall z. (forall (x :: k). f x -> z) -> ReadPrec z withElReadPrec (\f x x -> (forall (xs :: [k]). TypedList f xs -> r) -> WithAnyTL f r forall k (f :: k -> *) r. (forall (xs :: [k]). TypedList f xs -> r) -> WithAnyTL f r WithAnyTL ((forall (xs :: [k]). TypedList f xs -> r) -> WithAnyTL f r) -> (forall (xs :: [k]). TypedList f xs -> r) -> WithAnyTL f r forall a b. (a -> b) -> a -> b $ TypedList f (x : xs) -> r forall (xs :: [k]). TypedList f xs -> r use (TypedList f (x : xs) -> r) -> (TypedList f xs -> TypedList f (x : xs)) -> TypedList f xs -> r forall b c a. (b -> c) -> (a -> b) -> a -> c . (f x x f x -> TypedList f xs -> TypedList f (x : xs) forall k (f :: k -> *) (xs :: [k]) (y :: k) (ys :: [k]). (xs ~ (y : ys)) => f y -> TypedList f ys -> TypedList f xs :*)) ReadP () -> ReadPrec () forall a. ReadP a -> ReadPrec a Read.lift (ReadP () -> ReadPrec ()) -> (Lexeme -> ReadP ()) -> Lexeme -> ReadPrec () forall b c a. (b -> c) -> (a -> b) -> a -> c . Lexeme -> ReadP () Read.expect (Lexeme -> ReadPrec ()) -> Lexeme -> ReadPrec () forall a b. (a -> b) -> a -> b $ String -> Lexeme Read.Symbol String ":*" (forall z. (forall (x :: k). f x -> z) -> ReadPrec z) -> (forall (xs :: [k]). TypedList f xs -> r) -> ReadPrec r forall k (f :: k -> *) r. (forall z. (forall (x :: k). f x -> z) -> ReadPrec z) -> (forall (xs :: [k]). TypedList f xs -> r) -> ReadPrec r withTypedListReadPrec @f @r forall z. (forall (x :: k). f x -> z) -> ReadPrec z withElReadPrec forall (xs :: [k]). TypedList f xs -> r withX ) -- Workaround impredicative polymorphism newtype WithAnyTL (f :: k -> Type) (r :: Type) = WithAnyTL (forall (xs :: [k]) . TypedList f xs -> r) -------------------------------------------------------------------------------- -- internal -------------------------------------------------------------------------------- -- | This function does GHC's magic to convert user-supplied `tList` function -- to create an instance of `RepresentableList` typeclass at runtime. -- The trick is taken from Edward Kmett's reflection library explained -- in https://www.schoolofhaskell.com/user/thoughtpolice/using-reflection reifyRepList :: forall (k :: Type) (xs :: [k]) (r :: Type) . TypeList xs -> (RepresentableList xs => r) -> r reifyRepList :: TypeList xs -> (RepresentableList xs => r) -> r reifyRepList TypeList xs tl RepresentableList xs => r k = MagicRepList xs r -> TypeList xs -> r forall a b. a -> b unsafeCoerce ((RepresentableList xs => r) -> MagicRepList xs r forall k (xs :: [k]) r. (RepresentableList xs => r) -> MagicRepList xs r MagicRepList RepresentableList xs => r k :: MagicRepList xs r) TypeList xs 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 :: TypedList f xs -> PatReverse f xs unreverseTL TypedList f xs xs = case Dict (xs ~ Reverse (Reverse xs)) forall k (a :: k) (b :: k). Dict (a ~ b) unsafeEqTypes @xs @(Reverse (Reverse xs)) of Dict (xs ~ Reverse (Reverse xs)) Dict -> TypedList f (Reverse xs) -> PatReverse f xs forall k (f :: k -> *) (xs :: [k]) (sx :: [k]). ReverseList xs sx => TypedList f sx -> PatReverse f xs PatReverse @k @f @xs @(Reverse xs) (TypedList f xs -> TypedList f (Reverse xs) forall k (f :: k -> *) (xs :: [k]). TypedList f xs -> TypedList f (Reverse xs) Numeric.TypedList.reverse TypedList f xs xs) {-# INLINE unreverseTL #-} mkRTL :: forall (k :: Type) (xs :: [k]) . TypeList xs -> Dict (RepresentableList xs) mkRTL :: TypeList xs -> Dict (RepresentableList xs) mkRTL TypeList xs xs = TypeList xs -> (RepresentableList xs => Dict (RepresentableList xs)) -> Dict (RepresentableList xs) forall k (xs :: [k]) r. TypeList xs -> (RepresentableList xs => r) -> r reifyRepList TypeList xs xs RepresentableList xs => Dict (RepresentableList xs) forall (a :: Constraint). a => Dict a 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 f xs -> PatSnoc f xs unsnocTL (TypedList []) = case Dict (xs ~ '[]) forall k (a :: k) (b :: k). Dict (a ~ b) unsafeEqTypes @xs @'[] of Dict (xs ~ '[]) Dict -> PatSnoc f xs forall k (f :: k -> *). PatSnoc f '[] PatSNil unsnocTL (TypedList (Any x:[Any] xs)) = case Dict (xs ~ (Init xs +: Last xs)) forall k (a :: k) (b :: k). Dict (a ~ b) unsafeEqTypes @xs @(Init xs +: Last xs) of Dict (xs ~ (Init xs +: Last xs)) Dict -> TypedList f (Init xs) -> f (Last xs) -> PatSnoc f xs forall k (xs :: [k]) (s :: k) (xss :: [k]) (f :: k -> *). SnocList xs s xss => TypedList f xs -> f s -> PatSnoc f xss PatSnoc ([Any] -> TypedList f (Init xs) coerce [Any] sy) (Any -> f (Last xs) forall a b. a -> b unsafeCoerce Any y) where ([Any] sy, Any y) = Any -> [Any] -> ([Any], Any) unsnoc Any x [Any] xs unsnoc :: Any -> [Any] -> ([Any], Any) unsnoc :: Any -> [Any] -> ([Any], Any) unsnoc Any t [] = ([], Any t) unsnoc Any t (Any z:[Any] zs) = ([Any] -> [Any]) -> ([Any], Any) -> ([Any], Any) forall (a :: * -> * -> *) b c d. Arrow a => a b c -> a (b, d) (c, d) first (Any tAny -> [Any] -> [Any] forall a. a -> [a] -> [a] :) (Any -> [Any] -> ([Any], Any) unsnoc Any z [Any] 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 f xs -> PatCons f xs patTL (TypedList []) = case Dict (xs ~ '[]) forall k (a :: k) (b :: k). Dict (a ~ b) unsafeEqTypes @xs @'[] of Dict (xs ~ '[]) Dict -> PatCons f xs forall k (f :: k -> *). PatCons f '[] PatCNil patTL (TypedList (Any x : [Any] xs)) = case Dict (xs ~ (Head xs : Tail xs)) forall k (a :: k) (b :: k). Dict (a ~ b) unsafeEqTypes @xs @(Head xs ': Tail xs) of Dict (xs ~ (Head xs : Tail xs)) Dict -> f (Head xs) -> TypedList f (Tail xs) -> PatCons f (Head xs : Tail xs) forall a (f :: a -> *) (y :: a) (ys :: [a]). f y -> TypedList f ys -> PatCons f (y : ys) PatCons (Any -> f (Head xs) forall a b. a -> b unsafeCoerce Any x) ([Any] -> TypedList f (Tail xs) coerce [Any] xs) {-# INLINE patTL #-} mkEVL :: forall (k :: Type) (c :: k -> Constraint) (xs :: [k]) . DictList c xs -> Dict (All c xs, RepresentableList xs) mkEVL :: DictList c xs -> Dict (All c xs, RepresentableList xs) mkEVL DictList c xs U = Dict (All c xs, RepresentableList xs) forall (a :: Constraint). a => Dict a Dict mkEVL (Dict1 c y Dict1 :* TypedList (Dict1 c) ys evs) = case TypedList (Dict1 c) ys -> Dict (All c ys, RepresentableList ys) forall k (c :: k -> Constraint) (xs :: [k]). DictList c xs -> Dict (All c xs, RepresentableList xs) mkEVL TypedList (Dict1 c) ys evs of Dict (All c ys, RepresentableList ys) Dict -> Dict (All c xs, RepresentableList xs) forall (a :: Constraint). a => Dict a Dict _evList :: forall (k :: Type) (c :: k -> Constraint) (xs :: [k]) (f :: (k -> Type)) . All c xs => TypedList f xs -> DictList c xs _evList :: TypedList f xs -> DictList c xs _evList TypedList f xs U = DictList c xs forall k (f :: k -> *) (xs :: [k]). (xs ~ '[]) => TypedList f xs U _evList (f y _ :* TypedList f ys xs) = case TypedList f ys -> DictList c ys forall k (c :: k -> Constraint) (xs :: [k]) (f :: k -> *). All c xs => TypedList f xs -> DictList c xs _evList TypedList f ys xs of DictList c ys evs -> Dict1 c y forall k (c :: k -> Constraint) (a :: k). c a => Dict1 c a Dict1 Dict1 c y -> DictList c ys -> DictList c xs forall k (f :: k -> *) (xs :: [k]) (y :: k) (ys :: [k]). (xs ~ (y : ys)) => f y -> TypedList f ys -> TypedList f xs :* DictList c ys evs dimValInt :: forall (k :: Type) (x :: k) . Dim x -> Int dimValInt :: Dim x -> Int dimValInt = Word -> Int forall a b. (Integral a, Num b) => a -> b fromIntegral (Word -> Int) -> (Dim x -> Word) -> Dim x -> Int forall b c a. (b -> c) -> (a -> b) -> a -> c . Dim x -> Word forall k (x :: k). Dim x -> Word dimVal