parameterized (empty) → 0.1.0.0
raw patch · 11 files changed
+637/−0 lines, 11 filesdep +basedep +data-diversedep +transformerssetup-changed
Dependencies added: base, data-diverse, transformers
Files
- LICENSE +30/−0
- README.md +10/−0
- Setup.hs +2/−0
- parameterized.cabal +35/−0
- src/Parameterized/Control/Applicative.hs +88/−0
- src/Parameterized/Control/Monad.hs +53/−0
- src/Parameterized/Control/Monad/Trans/Reader.hs +153/−0
- src/Parameterized/Control/Monad/Trans/State/Strict.hs +128/−0
- src/Parameterized/Data/Monoid.hs +24/−0
- src/Parameterized/Data/Semigroup.hs +21/−0
- src/Parameterized/TypeLevel.hs +93/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Louis Pan (c) 2017++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Louis Pan nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,10 @@+[](https://hackage.haskell.org/package/parameterized)+[](http://travis-ci.org/louispan/parameterized)++Parameterized/indexed monoids and monads using only a single parameter type variable.++# Changelog++* 0.1.0.0+ - Initial version with parameterized Semigroup, Monoid, Applicative, Alternative, Monad+ - Added instances for OverlappingWhichReader, DistinctWhichReader, ManyReader, ManyState, and ChangingState
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ parameterized.cabal view
@@ -0,0 +1,35 @@+name: parameterized+version: 0.1.0.0+synopsis: Extensible records and polymorphic variants.+description: Parameterized/indexed monoids and monads using only a single parameter type variable.++homepage: https://github.com/louispan/parameterized#readme+license: BSD3+license-file: LICENSE+author: Louis Pan+maintainer: louis@pan.me+copyright: 2017 Louis Pan+category: Control+build-type: Simple+extra-source-files: README.md+cabal-version: >=1.10+tested-with: GHC == 8.0.2, GHC == 8.2.1++library+ hs-source-dirs: src+ exposed-modules: Parameterized.TypeLevel+ Parameterized.Data.Semigroup+ Parameterized.Data.Monoid+ Parameterized.Control.Applicative+ Parameterized.Control.Monad+ Parameterized.Control.Monad.Trans.Reader+ Parameterized.Control.Monad.Trans.State.Strict+ build-depends: base >= 4.7 && < 5+ , data-diverse >= 1.2.0.2+ , transformers >= 0.5.2.0+ ghc-options: -Wall+ default-language: Haskell2010++source-repository head+ type: git+ location: https://github.com/louispan/parameterized
+ src/Parameterized/Control/Applicative.hs view
@@ -0,0 +1,88 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}++module Parameterized.Control.Applicative+ ( module Parameterized.TypeLevel+ , PPointed(..)+ , PApplicative(..)+ , (&<*>)+ , (&*>)+ , (&<*)+ , pliftA+ , pliftA2+ , pliftA3+ , PEmpty(..)+ , PAlternative(..)+ , (&<|>)+ ) where++import Data.Kind+import Parameterized.TypeLevel++-- | Parameterized version of 'pure' in 'Applicative'+-- An instance of this should create a parameterized unary type+-- where the parameter is an identity in respect to 'papply'+class PPointed (m :: k -> Type -> Type) (id :: k) where+ -- | lift a value.+ ppure :: a -> m id a++-- | Parameterized version of 'ap' in 'Applicative'+-- NB. 'PPointed' cannot be made a superclass because type variable @id@ is not in scope.+class (Functor (m t), Functor (m u), Functor (m v)) =>+ PApplicative (m :: k -> Type -> Type) (t :: k) (u :: k) (v :: k) | t u -> v where+ -- | Sequential application.+ papply :: m t (a -> b) -> m u a -> m v b+++-- | Sequential application.+(&<*>) :: (PApplicative m t u v) => m t (a -> b) -> m u a -> m v b+(&<*>) = papply+infixl 4 &<*>++-- | Sequence actions, discarding the value of the first argument.+(&*>) :: (PApplicative m t u v) => m t a -> m u b -> m v b+a1 &*> a2 = (id <$ a1) &<*> a2+infixl 4 &<*++-- | Sequence actions, discarding the value of the second argument.+(&<*) :: (PApplicative m t u v) => m t a -> m u b -> m v a+(&<*) = pliftA2 const+infixl 4 &*> -- , &<**>++-- | Lift a function to actions.+pliftA :: (Functor (m t)) => (a -> b) -> m t a -> m t b+pliftA f x = f <$> x++-- | Lift a binary function to actions.+pliftA2 :: (PApplicative m t u v) => (a -> b -> c) -> m t a -> m u b -> m v c+pliftA2 f x y = (f <$> x) `papply` y++-- | Lift a ternary function to actions.+pliftA3+ :: ( PApplicative m t u v+ , PApplicative m v w x+ )+ => (a -> b -> c -> d) -> m t a -> m u b -> m w c -> m x d+pliftA3 f a b c = pliftA2 f a b &<*> c++-- | Parameterized version of empty in 'Alternative'.+-- An instance of this should create a parameterized unary type+-- where the parameter is an identity in respect to 'pappend'+class PEmpty (m :: k -> Type -> Type) (id :: k) where+ -- | The identity of '&<|>'+ pempty :: m id a++-- | Parameterized version of 'Alternative'+-- NB. 'PEmpty' cannot be made a superclass because type variable @id@ will be ambiguous.+-- NB. PAlternative doensn't require 'PApplicative' as a superclass, because+-- Some things can be made instances of 'PAlternative' but not 'PApplicative'.+class PAlternative (m :: k -> Type -> Type) (t :: k) (u :: k) (v :: k) | t u -> v where+ -- | An associative binary operation+ pappend :: m t a -> m u a -> m v a++(&<|>) :: (PAlternative m t u v) => m t a -> m u a -> m v a+(&<|>) = pappend+infixl 3 &<|>
+ src/Parameterized/Control/Monad.hs view
@@ -0,0 +1,53 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}++module Parameterized.Control.Monad+ ( module Parameterized.Control.Applicative+ , PMonad(..)+ , (&>>=)+ , (&>>)+ , (&=<<)+ , (&>=>)+ , (&<=<)+ ) where++import Data.Kind+import Parameterized.TypeLevel+import Parameterized.Control.Applicative++-- | Parameterized version of Monad.+class PApplicative m t u v => PMonad (m :: k -> Type -> Type) (t :: k) (u :: k) (v :: k) where+ -- | Sequentially compose two actions, passing any value produced by the first as an argument to the second.+ pbind :: m t a -> (a -> m u b) -> m v b++-- | Sequentially compose two actions, passing any value produced by the first as an argument to the second.+(&>>=) :: PMonad m t u v => m t a -> (a -> m u b) -> m v b+(&>>=) = pbind+infixl 1 &>>=++(&>>) :: PMonad m t u v => m t a -> m u b -> m v b+m &>> k = m &>>= \_ -> k+infixl 1 &>>++-- | Same as '&>>=', but with the arguments interchanged.+(&=<<) :: PMonad m t u v => (a -> m u b) -> m t a -> m v b+f &=<< x = x &>>= f+infixr 1 &=<<++-- | Left-to-right Kleisli composition of monads.+(&>=>) :: (PMonad m t u v) => (a -> m t b) -> (b -> m u c) -> (a -> m v c)+f &>=> g = \x -> f x &>>= g+infixr 1 &>=>++-- | Right-to-left Kleisli composition of monads. @('>=>')@, with the arguments flipped.+(&<=<) :: (PMonad m t u v) => (b -> m u c) -> (a -> m t b) -> (a -> m v c)+(&<=<) = flip (&>=>)+infixr 1 &<=<++-- class (PAlternative m t u v, PMonad m t u v) => PMonadPlus m t u v++-- class PMZero (m :: k -> Type -> Type) where+-- pmezero :: m (PId m) a
+ src/Parameterized/Control/Monad/Trans/Reader.hs view
@@ -0,0 +1,153 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++module Parameterized.Control.Monad.Trans.Reader where++import Control.Applicative+import Control.Monad+import qualified Control.Monad.Fail as Fail+import Control.Monad.Fix+import Control.Monad.IO.Class+import Control.Monad.Trans.Reader+import Control.Monad.Zip+import Data.Diverse+import qualified GHC.Generics as G+import Parameterized.Control.Monad++-- | Given a Reader that accepts @Which a@, and another Reader that accepts @Which b@+-- make a reader that accepts @Which (AppendUnique a b)@ and runs both readers if possible,+-- where the types in @Which a@ and @Which b@ may overlap,+-- but with the compile time constraint that all the types in (AppendUnique a b) are distinct.+newtype OverlappingWhichReader m r a = OverlappingWhichReader+ { runOverlappingWhichReader :: ReaderT r m a+ } deriving ( G.Generic+ , Functor+ , Applicative+ , Monad+ , Alternative+ , MonadPlus+ , MonadZip+ , MonadFix+ , Fail.MonadFail+ , MonadIO+ )++instance Applicative m => PPointed (OverlappingWhichReader m) (Which '[]) where+ ppure = OverlappingWhichReader . pure++instance Alternative m => PEmpty (OverlappingWhichReader m) (Which '[]) where+ pempty = OverlappingWhichReader $ empty++instance ( Alternative m+ , Reinterpret b c+ , Reinterpret a c+ , c ~ AppendUnique a b+ ) =>+ PAlternative (OverlappingWhichReader m) (Which a) (Which b) (Which c) where+ (OverlappingWhichReader (ReaderT f)) `pappend` (OverlappingWhichReader (ReaderT g)) =+ OverlappingWhichReader $ ReaderT $ \c -> case (reinterpret c, reinterpret c) of+ (Left _, Left _) -> empty+ (Left _, Right b) -> g b+ (Right a, Left _) -> f a+ (Right a, Right b) -> f a <|> g b++-------------------------------++-- | Given a Reader that accepts @Which a@, and another Reader that accepts @Which b@+-- make a reader that accepts @Which (Append a b)@ and only run one of the readers for the correct Which type,+-- with a compile-time contraint that the types in @Which a@ are distinct from the type in @Which b@+newtype DistinctWhichReader m r a = DistinctWhichReader+ { runDistinctWhichReader :: ReaderT r m a+ } deriving ( G.Generic+ , Functor+ , Applicative+ , Monad+ , Alternative+ , MonadPlus+ , MonadZip+ , MonadFix+ , Fail.MonadFail+ , MonadIO+ )++instance Applicative m => PPointed (DistinctWhichReader m) (Which '[]) where+ ppure = DistinctWhichReader . pure++instance Alternative m => PEmpty (DistinctWhichReader m) (Which '[]) where+ pempty = DistinctWhichReader $ empty++instance ( Reinterpret b c+ , Complement c b ~ a+ , Complement c a ~ b+ , c ~ Append a b+ ) =>+ PAlternative (DistinctWhichReader m) (Which a) (Which b) (Which c) where+ pappend (DistinctWhichReader (ReaderT f)) (DistinctWhichReader (ReaderT g)) =+ DistinctWhichReader . ReaderT $ \c -> case reinterpret c of+ Left a -> f a+ Right b -> g b++-------------------------------++-- | Given a Reader that accepts @Many a@, and another Reader that accepts @Many b@+-- make a reader that accepts @Many (AppendUnique a b)@+-- with the compile time constraint that all the types in (AppendUnique a b) are distinct.+newtype ManyReader m r a = ManyReader+ { runManyReader :: ReaderT r m a+ } deriving ( G.Generic+ , Functor+ , Applicative+ , Monad+ , Alternative+ , MonadPlus+ , MonadZip+ , MonadFix+ , Fail.MonadFail+ , MonadIO+ )++instance Applicative m => PPointed (ManyReader m) (Many '[]) where+ ppure = ManyReader . pure++instance Alternative m => PEmpty (ManyReader m) (Many '[]) where+ pempty = ManyReader $ empty++instance ( Functor (ManyReader m (Many c))+ , Applicative m+ , Select a c+ , Select b c+ , c ~ AppendUnique a b+ ) =>+ PApplicative (ManyReader m) (Many a) (Many b) (Many c) where+ papply (ManyReader (ReaderT f)) (ManyReader (ReaderT g)) =+ ManyReader . ReaderT $ \c -> f (select c) <*> g (select c)++instance ( Functor (ManyReader m (Many c))+ , Alternative m+ , Select a c+ , Select b c+ , c ~ AppendUnique a b+ ) =>+ PAlternative (ManyReader m) (Many a) (Many b) (Many c) where+ pappend (ManyReader (ReaderT f)) (ManyReader (ReaderT g)) =+ ManyReader . ReaderT $ \c -> f (select c) <|> g (select c)++instance ( Functor (ManyReader m (Many c))+ , Monad m+ , Select a c+ , Select b c+ , c ~ AppendUnique a b+ ) =>+ PMonad (ManyReader m) (Many a) (Many b) (Many c) where+ pbind (ManyReader (ReaderT f)) k =+ ManyReader . ReaderT $ \c ->+ f (select c) >>= (k' (select c))+ where+ k' b a = let ManyReader (ReaderT g) = k a in g b
+ src/Parameterized/Control/Monad/Trans/State/Strict.hs view
@@ -0,0 +1,128 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++module Parameterized.Control.Monad.Trans.State.Strict where++import Control.Applicative+import Control.Monad+import qualified Control.Monad.Fail as Fail+import Control.Monad.Fix+import Control.Monad.IO.Class+import Control.Monad.Trans.State.Strict+import Data.Diverse+import qualified GHC.Generics as G+import Parameterized.Control.Monad++-- | Given a ManyState that modifies @Many a@, and another ManyState that modifes @Many b@+-- make a State that accepts @Many (AppendUnique a b)@+-- with the compile time constraint that all the types in (AppendUnique a b) are distinct.+newtype ManyState m s a = ManyState+ { runManyState :: StateT s m a+ } deriving ( G.Generic+ , Functor+ , Applicative+ , Monad+ , Alternative+ , MonadPlus+ , MonadFix+ , Fail.MonadFail+ , MonadIO+ )++instance Monad m => PPointed (ManyState m) (Many '[]) where+ ppure = ManyState . pure++instance Alternative m => PEmpty (ManyState m) (Many '[]) where+ pempty = ManyState $ StateT $ \_ -> empty++instance ( Monad m+ , Select a c+ , Select b c+ , Amend a c+ , Amend b c+ , c ~ AppendUnique a b+ ) =>+ PApplicative (ManyState m) (Many a) (Many b) (Many c) where+ papply (ManyState (StateT x)) (ManyState (StateT y)) =+ ManyState . StateT $ \c -> do+ (f, a) <- x (select c)+ let c' = amend c a+ (r, b) <- y (select c')+ let c'' = amend c' b+ pure (f r, c'')++instance ( Monad m+ , Alternative m+ , Select a c+ , Select b c+ , Amend a c+ , Amend b c+ , c ~ AppendUnique a b+ ) =>+ PAlternative (ManyState m) (Many a) (Many b) (Many c) where+ pappend (ManyState (StateT x)) (ManyState (StateT y)) =+ ManyState . StateT $ \c -> x' c <|> y' c+ where+ x' c = do+ (r, a) <- x (select c)+ pure (r, amend c a)+ y' c = do+ (r, b) <- y (select c)+ pure (r, amend c b)++instance ( Monad m+ , Select a c+ , Select b c+ , Amend a c+ , Amend b c+ , c ~ AppendUnique a b+ ) =>+ PMonad (ManyState m) (Many a) (Many b) (Many c) where+ pbind (ManyState (StateT x)) k =+ ManyState . StateT $ \c -> do+ (r, a) <- x (select c)+ let c' = amend c a+ ManyState (StateT y) = k r+ (r', b) <- y (select c')+ let c'' = amend c' b+ pure (r', c'')++--------------------------------------------++-- | Given a ChangingState that changes state from @s@ to @t@,+-- and another ChangingState that changes state from @t@ to @u@+-- make a State that changes from @s@ to @u@+-- with the compile time constraint that all the types in (AppendUnique a b) are distinct.+newtype ChangingState m st a = ChangingState+ { runChangingState :: At0 st -> m (a, At1 st)+ } deriving ( G.Generic)++instance Functor m => Functor (ChangingState m st) where+ fmap f m = ChangingState $ \s ->+ fmap (\(a, s') -> (f a, s')) $ runChangingState m s++instance Applicative m => PPointed (ChangingState m) (s, s) where+ ppure a = ChangingState $ \s -> pure (a, s)++instance Monad m => PApplicative (ChangingState m) (s, t) (t, u) (s, u) where+ papply (ChangingState x) (ChangingState y) =+ ChangingState $ \s -> do+ (f, t) <- x s+ (r, u) <- y t+ pure (f r, u)++instance Monad m => PMonad (ChangingState m) (s, t) (t, u) (s, u) where+ pbind (ChangingState x) k =+ ChangingState $ \s -> do+ (r, t) <- x s+ let ChangingState y = k r+ (r', u) <- y t+ pure (r', u)
+ src/Parameterized/Data/Monoid.hs view
@@ -0,0 +1,24 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}++module Parameterized.Data.Monoid+ ( module Parameterized.TypeLevel+ , module Parameterized.Data.Semigroup+ , PMempty(..)+ , PMonoid+ ) where++import Data.Kind+import Parameterized.TypeLevel+import Parameterized.Data.Semigroup++-- | Parameterized version of mempty in Monoid.+class PMempty (n :: k -> Type) (id :: k) where+ pmempty :: n id++-- | Parameterized version of Monoid.+type PMonoid n id t u v = (PMempty n id, PSemigroup n t u v)
+ src/Parameterized/Data/Semigroup.hs view
@@ -0,0 +1,21 @@+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}++module Parameterized.Data.Semigroup where++import Data.Kind++-- | Parameterized version of (<>) in Semigroup+-- If used in conjunction with 'Parameterized.Data.Empty', ie as a parameterized Monoid,+-- then the instance should follow the following laws:+-- * @pmempty' `pmappend'` x = x@+-- * @x `pmappend'` pempty' = x@+-- * @x `pmappend'` (y `pmappend'` z) = (x `pmappend'` y) `pmappend'` z@+class PSemigroup (n :: k -> Type) (t :: k) (u :: k) (v :: k) | t u -> v where+ pmappend :: n t -> n u -> n v++(&<>) :: (PSemigroup n t u v) => n t -> n u -> n v+(&<>) = pmappend+infixr 6 &<>
+ src/Parameterized/TypeLevel.hs view
@@ -0,0 +1,93 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}++module Parameterized.TypeLevel where++-- | Get the first type of a type level tuple+-- This is useful for defining a newtype wrapper with a single "parameterized" type,+-- around a type with many "parameterized" type variables.+type family At0 t where+ At0 (x, _) = x+ At0 (x, _, _) = x+ At0 (x, _, _, _) = x+ At0 (x, _, _, _, _) = x+ At0 (x, _, _, _, _, _) = x+ At0 (x, _, _, _, _, _, _) = x+ At0 (x, _, _, _, _, _, _, _) = x+ At0 (x, _, _, _, _, _, _, _, _) = x+ At0 (x, _, _, _, _, _, _, _, _, _) = x++-- | Get the second type of a type level tuple+type family At1 t where+ At1 (_, x) = x+ At1 (_, x, _) = x+ At1 (_, x, _, _) = x+ At1 (_, x, _, _, _) = x+ At1 (_, x, _, _, _, _) = x+ At1 (_, x, _, _, _, _, _) = x+ At1 (_, x, _, _, _, _, _, _) = x+ At1 (_, x, _, _, _, _, _, _, _) = x+ At1 (_, x, _, _, _, _, _, _, _, _) = x++-- | Get the third type of a type level tuple+type family At2 t where+ At2 (_, _, x) = x+ At2 (_, _, x, _) = x+ At2 (_, _, x, _, _) = x+ At2 (_, _, x, _, _, _) = x+ At2 (_, _, x, _, _, _, _) = x+ At2 (_, _, x, _, _, _, _, _) = x+ At2 (_, _, x, _, _, _, _, _, _) = x+ At2 (_, _, x, _, _, _, _, _, _, _) = x++-- | Get the fourth type of a type level tuple+type family At3 t where+ At3 (_, _, _, x) = x+ At3 (_, _, _, x, _) = x+ At3 (_, _, _, x, _, _) = x+ At3 (_, _, _, x, _, _, _) = x+ At3 (_, _, _, x, _, _, _, _) = x+ At3 (_, _, _, x, _, _, _, _, _) = x+ At3 (_, _, _, x, _, _, _, _, _, _) = x++-- | Get the fifth type of a type level tuple+type family At4 t where+ At4 (_, _, _, _, x) = x+ At4 (_, _, _, _, x, _) = x+ At4 (_, _, _, _, x, _, _) = x+ At4 (_, _, _, _, x, _, _, _) = x+ At4 (_, _, _, _, x, _, _, _, _) = x+ At4 (_, _, _, _, x, _, _, _, _, _) = x++-- | Get the sixth type of a type level tuple+type family At5 t where+ At5 (_, _, _, _, _, x) = x+ At5 (_, _, _, _, _, x, _) = x+ At5 (_, _, _, _, _, x, _, _) = x+ At5 (_, _, _, _, _, x, _, _, _) = x+ At5 (_, _, _, _, _, x, _, _, _, _) = x++-- | Get the seventh type of a type level tuple+type family At6 t where+ At6 (_, _, _, _, _, _, x) = x+ At6 (_, _, _, _, _, _, x, _) = x+ At6 (_, _, _, _, _, _, x, _, _) = x+ At6 (_, _, _, _, _, _, x, _, _, _) = x++-- | Get the eigth type of a type level tuple+type family At7 t where+ At7 (_, _, _, _, _, _, _, x) = x+ At7 (_, _, _, _, _, _, _, x, _) = x+ At7 (_, _, _, _, _, _, _, x, _, _) = x++-- | Get the nineth type of a type level tuple+type family At8 t where+ At8 (_, _, _, _, _, _, _, _, x) = x+ At8 (_, _, _, _, _, _, _, _, x, _) = x++-- | Get the tenth type of a type level tuple+type family At9 t where+ At9 (_, _, _, _, _, _, _, _, _, x) = x