{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE GADTs #-} ----------------------------------------------------------------------------- -- | -- Module : Data.Type.Product -- Copyright : Copyright (C) 2015 Kyle Carter -- License : BSD3 -- -- Maintainer : Kyle Carter <kylcarte@indiana.edu> -- Stability : experimental -- Portability : RankNTypes -- -- Type combinators for type-level lists, -- lifting @(f :: k -> *)@ to @(Prod f :: [k] -> *)@, -- as well as its constructions, manipulations, and -- eliminations. -- -- 'Prod' is similar in nature to a few others in the Haskell ecosystem, such as: -- -- Oleg Kiselyov's 'HList', from <http://hackage.haskell.org/package/HList>, and -- -- Kenneth Foner's 'ConicList', from <http://hackage.haskell.org/package/IndexedList-0.1.0.1/docs/Data-List-Indexed-Conic.html>. -- ----------------------------------------------------------------------------- module Data.Type.Product where import Data.Type.Boolean import Data.Type.Combinator import Data.Type.Conjunction import Data.Type.Index import Data.Type.Length -- import Data.Type.Quantifier import Type.Class.Higher import Type.Class.Known import Type.Class.Witness import Type.Family.Constraint import Type.Family.List data Prod (f :: k -> *) :: [k] -> * where Ø :: Prod f Ø (:<) :: !(f a) -> !(Prod f as) -> Prod f (a :< as) infixr 5 :< deriving instance ListC (Eq <$> f <$> as) => Eq (Prod f as) deriving instance ( ListC (Eq <$> f <$> as) , ListC (Ord <$> f <$> as) ) => Ord (Prod f as) deriving instance ListC (Show <$> f <$> as) => Show (Prod f as) instance Eq1 f => Eq1 (Prod f) where eq1 = \case Ø -> \case Ø -> True a :< as -> \case b :< bs -> a =#= b && as =#= bs instance Ord1 f => Ord1 (Prod f) where compare1 = \case Ø -> \case Ø -> EQ a :< as -> \case b :< bs -> compare1 a b `mappend` compare1 as bs instance Show1 f => Show1 (Prod f) where showsPrec1 d = \case Ø -> showString "Ø" a :< as -> showParen (d > 5) $ showsPrec1 6 a . showString " :< " . showsPrec1 6 as instance Read1 f => Read1 (Prod f) where readsPrec1 d s0 = [ (Some Ø,s1) | ("Ø",s1) <- lex s0 ] ++ readParen (d > 5) ( \s1 -> [ (x >>- \a -> xs >>- \as -> Some $ a :< as,s4) | (x,s2) <- readsPrec1 6 s1 , (":<",s3) <- lex s2 , (xs,s4) <- readsPrec1 5 s3 ] ) s0 instance BoolEquality f => BoolEquality (Prod f) where boolEquality = \case Ø -> \case Ø -> True_ (:<){} -> False_ a :< as -> \case b :< bs -> case a .== b of True_ -> case as .== bs of True_ -> True_ False_ -> False_ False_ -> False_ Ø -> False_ instance TestEquality f => TestEquality (Prod f) where testEquality = \case Ø -> \case Ø -> qed _ -> Nothing a :< as -> \case b :< bs -> a =?= b //? as =?= bs //? qed _ -> Nothing -- | Construct a two element Prod. -- Since the precedence of (:>) is higher than (:<), -- we can conveniently write lists like: -- -- >>> a :< b :> c -- -- Which is identical to: -- -- >>> a :< b :< c :< Ø -- pattern (:>) :: (f :: k -> *) (a :: k) -> f (b :: k) -> Prod f '[a,b] pattern a :> b = a :< b :< Ø infix 6 :> -- | Build a singleton Prod. only :: f a -> Prod f '[a] only = (:< Ø) -- | snoc function. insert an element at the end of the list. (>:) :: Prod f as -> f a -> Prod f (as >: a) (>:) = \case Ø -> only b :< as -> (b :<) . (as >:) infixl 6 >: head' :: Prod f (a :< as) -> f a head' (a :< _) = a tail' :: Prod f (a :< as) -> Prod f as tail' (_ :< as) = as -- | Get all but the last element of a non-empty Prod. init' :: Prod f (a :< as) -> Prod f (Init' a as) init' (a :< as) = case as of Ø -> Ø (:<){} -> a :< init' as -- | Get the last element of a non-empty Prod. last' :: Prod f (a :< as) -> f (Last' a as) last' (a :< as) = case as of Ø -> a (:<){} -> last' as reverse' :: Prod f as -> Prod f (Reverse as) reverse' = \case Ø -> Ø a :< as -> reverse' as >: a append' :: Prod f as -> Prod f bs -> Prod f (as ++ bs) append' = \case Ø -> id a :< as -> (a :<) . append' as {- lookup' :: TestEquality f => f a -> Prod (f :&: g) as -> Maybe (g a) lookup' a = \case Ø -> Nothing (b :&: v) :< bs -> witMaybe (a =?= b) (Just v) $ lookup' a bs -} lookupPar :: TestEquality f => f a -> Prod (f :*: g) as -> Maybe (Some g) lookupPar a = \case Ø -> Nothing (b :*: v) :< bs -> witMaybe (a =?= b) (Just $ Some v) $ lookupPar a bs permute :: Known Length bs => (forall x. Index bs x -> Index as x) -> Prod f as -> Prod f bs permute f as = permute' f as known permute' :: (forall x. Index bs x -> Index as x) -> Prod f as -> Length bs -> Prod f bs permute' f as = \case LZ -> Ø LS l -> index (f IZ) as :< permute' (f . IS) as l -- Tuple {{{ -- | A Prod of simple Haskell types. type Tuple = Prod I -- | Singleton Tuple. only_ :: a -> Tuple '[a] only_ = only . I -- | Cons onto a Tuple. pattern (::<) :: a -> Tuple as -> Tuple (a :< as) pattern a ::< as = I a :< as infixr 5 ::< -- | Snoc onto a Tuple. (>::) :: Tuple as -> a -> Tuple (as >: a) (>::) = \case Ø -> only_ b :< as -> (b :<) . (as >::) infixl 6 >:: -- }}} elimProd :: p Ø -> (forall x xs. Index as x -> f x -> p xs -> p (x :< xs)) -> Prod f as -> p as elimProd n c = \case Ø -> n a :< as -> c IZ a $ elimProd n (c . IS) as onHead' :: (f a -> f b) -> Prod f (a :< as) -> Prod f (b :< as) onHead' f (a :< as) = f a :< as onTail' :: (Prod f as -> Prod f bs) -> Prod f (a :< as) -> Prod f (a :< bs) onTail' f (a :< as) = a :< f as uncurry' :: (f a -> Prod f as -> r) -> Prod f (a :< as) -> r uncurry' f (a :< as) = f a as curry' :: (l ~ (a :< as)) => (Prod f l -> r) -> f a -> Prod f as -> r curry' f a as = f $ a :< as index :: Index as a -> Prod f as -> f a index = \case IZ -> head' IS x -> index x . tail' select :: Prod (Index as) bs -> Prod f as -> Prod f bs select = \case Ø -> pure Ø x:<xs -> (:<) <$> index x <*> select xs indices :: forall as. Known Length as => Prod (Index as) as indices = indices' known indices' :: Length as -> Prod (Index as) as indices' = \case LZ -> Ø LS l -> IZ :< map1 IS (indices' l) instance Functor1 Prod where map1 f = \case Ø -> Ø a :< as -> f a :< map1 f as instance IxFunctor1 Index Prod where imap1 f = \case Ø -> Ø a :< as -> f IZ a :< imap1 (f . IS) as instance Foldable1 Prod where foldMap1 f = \case Ø -> mempty a :< as -> f a `mappend` foldMap1 f as instance IxFoldable1 Index Prod where ifoldMap1 f = \case Ø -> mempty a :< as -> f IZ a `mappend` ifoldMap1 (f . IS) as instance Traversable1 Prod where traverse1 f = \case Ø -> pure Ø a :< as -> (:<) <$> f a <*> traverse1 f as instance IxTraversable1 Index Prod where itraverse1 f = \case Ø -> pure Ø a :< as -> (:<) <$> f IZ a <*> itraverse1 (f . IS) as instance (Known Length as, Every (Known f) as) => Known (Prod f) as where type KnownC (Prod f) as = (Known Length as, Every (Known f) as) known = go known where go :: Every (Known f) xs => Length xs -> Prod f xs go = \case LZ -> Ø LS l -> known :< go l {- instance Known (Prod f) Ø where known = Ø instance (Known f a, Known (Prod f) as) => Known (Prod f) (a :< as) where type KnownC (Prod f) (a :< as) = (Known f a, Known (Prod f) as) known = known :< known -} type family Witnesses (ps :: [Constraint]) (qs :: [Constraint]) (f :: k -> *) (as :: [k]) :: Constraint where Witnesses Ø Ø f Ø = ØC Witnesses (p :< ps) (q :< qs) f (a :< as) = (Witness p q (f a), Witnesses ps qs f as) instance Witness ØC ØC (Prod f Ø) where r \\ _ = r instance (Witness p q (f a), Witness s t (Prod f as)) => Witness (p,s) (q,t) (Prod f (a :< as)) where type WitnessC (p,s) (q,t) (Prod f (a :< as)) = (Witness p q (f a), Witness s t (Prod f as)) r \\ (a :< as) = r \\ a \\ as toList :: (forall a. f a -> r) -> Prod f as -> [r] toList f = \case Ø -> [] a :< as -> f a : toList f as