packages feed

type-combinators 0.1.0.1 → 0.1.2.0

raw patch · 14 files changed

+664/−129 lines, 14 filesdep +containersdep +mtldep +template-haskell

Dependencies added: containers, mtl, template-haskell, transformers

Files

src/Data/Type/Combinator.hs view
@@ -34,6 +34,7 @@ import Type.Class.HFunctor import Type.Class.Known import Type.Class.Witness+import Type.Family.Tuple  import Control.Applicative @@ -293,6 +294,66 @@  flipped :: (f a b -> g c d) -> Flip f b a -> Flip g d c flipped f = Flip . f . getFlip++-- }}}++-- Cur {{{++newtype Cur (p :: (k,l) -> *) :: k -> l -> * where+  Cur :: { getCur :: p (a#b) } -> Cur p a b++instance Known p (a#b) => Known (Cur p a) b where+  type KnownC (Cur p a) b = Known p (a#b)+  known = Cur known++instance Witness q r (p (a#b)) => Witness q r (Cur p a b) where+  type WitnessC q r (Cur p a b) = Witness q r (p (a#b))+  r \\ Cur p = r \\ p++-- }}}++-- Uncur {{{++data Uncur (p :: k -> l -> *) :: (k,l) -> * where+  Uncur :: { getUncur :: p a b } -> Uncur p (a#b)++instance (Known (p a) b,q ~ (a#b)) => Known (Uncur p) q where+  type KnownC (Uncur p) q = Known (p (Fst q)) (Snd q)+  known = Uncur known++instance (Witness r s (p a b),q ~ (a#b)) => Witness r s (Uncur p q) where+  type WitnessC r s (Uncur p q) = Witness r s (p (Fst q) (Snd q))+  r \\ Uncur p = r \\ p++-- }}}++-- Cur {{{++newtype Cur3 (p :: (k,l,m) -> *) :: k -> l -> m -> * where+  Cur3 :: { getCur3 :: p '(a,b,c) } -> Cur3 p a b c++instance Known p '(a,b,c) => Known (Cur3 p a b) c where+  type KnownC (Cur3 p a b) c = Known p '(a,b,c)+  known = Cur3 known++instance Witness q r (p '(a,b,c)) => Witness q r (Cur3 p a b c) where+  type WitnessC q r (Cur3 p a b c) = Witness q r (p '(a,b,c))+  r \\ Cur3 p = r \\ p++-- }}}++-- Uncur3 {{{++data Uncur3 (p :: k -> l -> m -> *) :: (k,l,m) -> * where+  Uncur3 :: { getUncur3 :: p a b c } -> Uncur3 p '(a,b,c)++instance (Known (p a b) c,q ~ '(a,b,c)) => Known (Uncur3 p) q where+  type KnownC (Uncur3 p) q = Known (p (Fst3 q) (Snd3 q)) (Thd3 q)+  known = Uncur3 known++instance (Witness r s (p a b c),q ~ '(a,b,c)) => Witness r s (Uncur3 p q) where+  type WitnessC r s (Uncur3 p q) = Witness r s (p (Fst3 q) (Snd3 q) (Thd3 q))+  r \\ Uncur3 p = r \\ p  -- }}}
src/Data/Type/Conjunction.hs view
@@ -35,7 +35,7 @@ import Type.Class.HFunctor import Type.Class.Known import Type.Class.Witness-import Type.Family.Pair+import Type.Family.Tuple  -- (:&:) {{{
src/Data/Type/Index.hs view
@@ -33,8 +33,6 @@ import Type.Family.List import Type.Family.Nat --- | 'IZ' indexes the head of the list,--- and 'IS' indexes into the tail of the list. data Index :: [k] -> k -> * where   IZ :: Index (a :< as) a   IS :: !(Index as a) -> Index (b :< as) a
+ src/Data/Type/Index/Quote.hs view
@@ -0,0 +1,48 @@+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE LambdaCase #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Type.Index.Quote+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- A 'QuasiQuoter' for the 'Index' type.+--+-----------------------------------------------------------------------------++module Data.Type.Index.Quote where++import Data.Type.Index+import Language.Haskell.TH+import Language.Haskell.TH.Lib+import Language.Haskell.TH.Quote+import Text.Read (readMaybe)+import Control.Monad++ix :: QuasiQuoter+ix = QuasiQuoter+  { quoteExp  = parseIxExp+  , quotePat  = error "ix: quotePat not defined"+  , quoteType = error "ix: quoteType not defined"+  , quoteDec  = error "ix: quoteDec not defined"+  }++parseIxExp :: String -> Q Exp+parseIxExp s = maybe (fail $ "ix: couldn't parse Int: " ++ show s)+  (notNeg >=> go)+  $ readMaybe s+  where+  notNeg :: Int -> Q Int+  notNeg n+    | n < 0 = fail $ "ix: negative index: " ++ show n+    | True  = return n+  go :: Int -> Q Exp+  go = \case+    0 -> [| IZ |]+    n -> [| IS $(go $ n-1) |]+
+ src/Data/Type/Nat/Quote.hs view
@@ -0,0 +1,89 @@+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE GADTs #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Type.Index.Quote+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- A 'QuasiQuoter' for the 'N' kind and the 'Nat' type.+--+-----------------------------------------------------------------------------++module Data.Type.Nat.Quote where++import Data.Type.Nat+import Type.Family.Nat+import Language.Haskell.TH+import Language.Haskell.TH.Quote+import Control.Monad+import Text.Read (readMaybe)++n :: QuasiQuoter+n = QuasiQuoter+  { quoteExp  = parseNatExp+  , quotePat  = parseNatPat+  , quoteType = parseNatType+  , quoteDec  = error "n: quoteDec not defined"+  }++parseNatExp :: String -> Q Exp+parseNatExp s = maybe (fail $ "n: couldn't parse Int: " ++ show s)+  (notNeg >=> go)+  $ readMaybe s+  where+  notNeg :: Int -> Q Int+  notNeg n+    | n < 0 = fail $ "n: negative: " ++ show n+    | True  = return n+  go :: Int -> Q Exp+  go = \case+    0 -> [| Z_ |]+    n -> [| S_ $(go $ n-1) |]++parseNatPat :: String -> Q Pat+parseNatPat s = maybe (fail $ "n: couldn't parse Int: " ++ show s)+  (notNeg >=> go)+  $ readMaybe s+  where+  notNeg :: Int -> Q Int+  notNeg n+    | n < 0 = fail $ "n: negative: " ++ show n+    | True  = return n+  go :: Int -> Q Pat+  go = \case+    0 -> [p| Z_ |]+    n -> [p| S_ $(go $ n-1) |]++parseNatType :: String -> Q Type+parseNatType s = maybe (fail $ "n: couldn't parse Int: " ++ show s)+  (notNeg >=> go)+  $ readMaybe s+  where+  notNeg :: Int -> Q Int+  notNeg n+    | n < 0 = fail $ "n: negative: " ++ show n+    | True  = return n+  go :: Int -> Q Type+  go = \case+    0 -> [t| Z |]+    n -> [t| S $(go $ n-1) |]+
src/Data/Type/Product.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ViewPatterns #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE StandaloneDeriving #-}@@ -37,7 +38,7 @@  module Data.Type.Product where -import Data.Type.Combinator ((:.:)(..),IT(..))+import Data.Type.Combinator ((:.:)(..),IT(..),I(..)) import Data.Type.Index import Data.Type.Length import Type.Class.HFunctor@@ -46,49 +47,88 @@ import Type.Family.Constraint import Type.Family.List +import Control.Arrow ((&&&))+ data Prod (f :: k -> *) :: [k] -> * where   Ø    :: Prod f Ø   (:<) :: !(f a) -> !(Prod f as) -> Prod f (a :< as) infixr 5 :< +-- | 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 = (:< Ø) -head' :: Prod f (a :< as) -> f a-head' (a :< _) = a--tail' :: Prod f (a :< as) -> Prod f as-tail' (_ :< as) = as-+-- | 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 >: -reverse' :: Prod f as -> Prod f (Reverse as)-reverse' = \case-  Ø       -> Ø-  a :< as -> reverse' as >: a+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++-- 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 >::++-- }}}  onHead' :: (f a -> f b) -> Prod f (a :< as) -> Prod f (b :< as) onHead' f (a :< as) = f a :< as
+ src/Data/Type/Product/Dual.hs view
@@ -0,0 +1,184 @@+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE GADTs #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Type.Product.Dual+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- Type combinators for type-level lists,+-- where we have many functors with a single index.+--+-----------------------------------------------------------------------------++module Data.Type.Product.Dual where++import Data.Type.Combinator ((:.:)(..),IT(..),I(..))+import Data.Type.Index+import Data.Type.Length+import Type.Class.HFunctor+import Type.Class.Known+import Type.Class.Witness+import Type.Family.Constraint+import Type.Family.List++import Control.Arrow ((&&&))+import Data.Monoid ((<>))++data FProd (fs :: [k -> *]) :: k -> * where+  ØF   :: FProd Ø a+  (:<<) :: !(f a) -> !(FProd fs a) -> FProd (f :< fs) a+infixr 5 :<<++-- | Construct a two element FProd.+--   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) -> (g :: k -> *) a -> FProd '[f,g] a+pattern a :>> b = a :<< b :<< ØF+infix 6 :>>++-- | Build a singleton FProd.+onlyF :: f a -> FProd '[f] a+onlyF = (:<< ØF)++-- | snoc function. insert an element at the end of the FProd.+(>>:) :: FProd fs a -> f a -> FProd (fs >: f) a+(>>:) = \case+  ØF       -> onlyF+  b :<< as -> (b :<<) . (as >>:)+infixl 6 >>:++headF :: FProd (f :< fs) a -> f a+headF (a :<< _) = a++tailF :: FProd (f :< fs) a -> FProd fs a+tailF (_ :<< as) = as++-- | Get all but the last element of a non-empty FProd.+initF :: FProd (f :< fs) a -> FProd (Init' f fs) a+initF (a :<< as) = case as of+  ØF     -> ØF+  (:<<){} -> a :<< initF as++-- | Get the last element of a non-empty FProd.+lastF :: FProd (f :< fs) a -> Last' f fs a+lastF (a :<< as) = case as of+  ØF      -> a+  (:<<){} -> lastF as++-- | Reverse the elements of an FProd.+reverseF :: FProd fs a -> FProd (Reverse fs) a+reverseF = \case+  ØF       -> ØF+  a :<< as -> reverseF as >>: a++-- | Append two FProds.+appendF :: FProd fs a -> FProd gs a -> FProd (fs ++ gs) a+appendF = \case+  ØF       -> id+  a :<< as -> (a :<<) . appendF as++-- | Map over the head of a non-empty FProd.+onHeadF :: (f a -> g a) -> FProd (f :< fs) a -> FProd (g :< fs) a+onHeadF f (a :<< as) = f a :<< as++-- | Map over the tail of a non-empty FProd.+onTailF :: (FProd fs a -> FProd gs a) -> FProd (f :< fs) a -> FProd (f :< gs) a+onTailF f (a :<< as) = a :<< f as++uncurryF :: (f a -> FProd fs a -> r) -> FProd (f :< fs) a -> r+uncurryF f (a :<< as) = f a as++curryF :: (l ~ (f :< fs)) => (FProd l a -> r) -> f a -> FProd fs a -> r+curryF f a as = f $ a :<< as++indexF :: Index fs f -> FProd fs a -> f a+indexF = \case+  IZ -> headF+  IS x -> indexF x . tailF++-- | If all @f@ in @fs@ are @Functor@s, then @FProd fs@ is a @Functor@.+instance ListC (Functor <$> fs) => Functor (FProd fs) where+  fmap f = \case+    ØF       -> ØF+    a :<< as -> fmap f a :<< fmap f as++-- | If all @f@ in @fs@ are @Foldable@s, then @FProd fs@ is a @Foldable@.+instance ListC (Foldable <$> fs) => Foldable (FProd fs) where+  foldMap f = \case+    ØF       -> mempty+    a :<< as -> foldMap f a <> foldMap f as++-- | If all @f@ in @fs@ are @Traversable@s, then @FProd fs@ is a @Traversable@.+instance+  ( ListC (Functor     <$> fs)+  , ListC (Foldable    <$> fs)+  , ListC (Traversable <$> fs)+  ) => Traversable (FProd fs) where+  traverse f = \case+    ØF       -> pure ØF+    a :<< as -> (:<<) <$> traverse f a <*> traverse f as++-- | Map over all elements of an FProd with access to the element's index.+imapF :: (forall f. Index fs f -> f a -> f b)+  -> FProd fs a -> FProd fs b+imapF f = \case+  ØF       -> ØF+  a :<< as -> f IZ a :<< imapF (f . IS) as++-- | Fold over all elements of an FProd with access to the element's index.+ifoldMapF :: Monoid m+  => (forall f. Index fs f -> f a -> m)+  -> FProd fs a -> m+ifoldMapF f = \case+  ØF       -> mempty+  a :<< as -> f IZ a <> ifoldMapF (f . IS) as++-- | Traverse over all elements of an FProd with access to the element's index.+itraverseF :: Applicative g+  => (forall f. Index fs f -> f a -> g (f b))+  -> FProd fs a -> g (FProd fs b)+itraverseF f = \case+  ØF       -> pure ØF+  a :<< as -> (:<<) <$> f IZ a <*> itraverseF (f . IS) as++instance Known (FProd Ø) a where+  known = ØF++instance (Known f a, Known (FProd fs) a) => Known (FProd (f :< fs)) a where+  type KnownC (FProd (f :< fs)) a = (Known f a, Known (FProd fs) a)+  known = known :<< known++-- | An empty FProd is a no-op Witness.+instance Witness ØC ØC (FProd Ø a) where+  r \\ _ = r++-- | A non-empty FProd is a Witness if both its head and tail are Witnesses.+instance (Witness p q (f a), Witness s t (FProd fs a)) => Witness (p,s) (q,t) (FProd (f :< fs) a) where+  type WitnessC (p,s) (q,t) (FProd (f :< fs) a) = (Witness p q (f a), Witness s t (FProd fs a))+  r \\ (a :<< as) = r \\ a \\ as+
src/Data/Type/Quantifier.hs view
@@ -40,14 +40,18 @@  -- | An eliminator for a 'Some' type. ----- NB: the result type of the eliminating function may--- not refer to the universally quantified type index @a@.+-- Consider this function akin to a Monadic bind, except+-- instead of binding into a Monad with a sequent function,+-- we're binding into the existential quantification with+-- a universal eliminator function. ----- This function deserves more documentation. It is a powerful--- basis for working with correct-by-construction data. -- It serves as an explicit delimiter in a program of where -- the type index may be used and depended on, and where it may -- not.+--+-- NB: the result type of the eliminating function may+-- not refer to the universally quantified type index @a@.+-- some :: Some f -> (forall a. f a -> r) -> r some (Some a) f = f a
src/Data/Type/Sum.hs view
@@ -22,10 +22,9 @@ -- Stability   :  experimental -- Portability :  RankNTypes ----- 'Sum' and 'SumF' are type combinators for representing disjoint sums of--- indices @(as :: [k])@ of a single functor @(f :: k -> *), or of--- many functors @(fs :: [k -> *])@ at a single index @(a :: k)@,--- respectively.+-- 'Sum' is a type combinators for representing disjoint sums of+-- indices @(as :: [k])@ of a single functor @(f :: k -> *).+-- Contrast to the many-functors-one-index 'FSum' -- ----------------------------------------------------------------------------- @@ -43,6 +42,10 @@   InL :: !(f a) -> Sum f (a :< as)   InR :: !(Sum f as) -> Sum f (a :< as) +-- | There are no possible values of the type @Sum f Ø@.+nilSum :: Sum f Ø -> Void+nilSum = impossible+ decomp :: Sum f (a :< as) -> Either (f a) (Sum f as) decomp = \case   InL a -> Left  a@@ -113,38 +116,4 @@     InR s -> r \\ s  -- }}}--data SumF :: [k -> *] -> k -> * where-  InLF :: !(f a) -> SumF (f :< fs) a-  InRF :: !(SumF fs a) -> SumF (f :< fs) a--instance ListC (Functor <$> fs) => Functor (SumF fs) where-  fmap f = \case-    InLF a -> InLF $ f <$> a-    InRF s -> InRF $ f <$> s--decompF :: SumF (f :< fs) a -> Either (f a) (SumF fs a)-decompF = \case-  InLF a -> Left  a-  InRF s -> Right s--injF :: (f ∈ fs) => f a -> SumF fs a-injF = injectSumF elemIndex--prjF :: (f ∈ fs) => SumF fs a -> Maybe (f a)-prjF = indexF elemIndex--injectSumF :: Index fs f -> f a -> SumF fs a-injectSumF = \case-  IZ   -> InLF-  IS x -> InRF . injectSumF x--indexF :: Index fs f -> SumF fs a -> Maybe (f a)-indexF = \case-  IZ -> \case-    InLF a -> Just a-    _      -> Nothing-  IS x -> \case-    InRF s -> indexF x s-    _      -> Nothing
+ src/Data/Type/Sum/Dual.hs view
@@ -0,0 +1,125 @@+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE GADTs #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Type.Sum.Dual+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- 'FSum' is a type combinators for representing disjoint sums of+-- many functors @(fs :: [k -> *])@ at a single index @(a :: k)@.+-- As opposed to one-functor-many-indices 'Sum'.+--+-----------------------------------------------------------------------------++module Data.Type.Sum.Dual where++import Data.Type.Index++import Type.Class.HFunctor+import Type.Class.Witness++import Type.Family.Constraint+import Type.Family.List++data FSum :: [k -> *] -> k -> * where+  FInL :: !(f a) -> FSum (f :< fs) a+  FInR :: !(FSum fs a) -> FSum (f :< fs) a++-- | There are no possible values of the type @FSum Ø a@.+nilSumF :: FSum Ø a -> Void+nilSumF = impossible++-- | Decompose a non-empty FSum into either its head or its tail.+decompF :: FSum (f :< fs) a -> Either (f a) (FSum fs a)+decompF = \case+  FInL a -> Left  a+  FInR s -> Right s++-- | Inject an element into an FSum.+injF :: (f ∈ fs) => f a -> FSum fs a+injF = injectFSum elemIndex++-- | Project an implicit index out of an FSum.+prjF :: (f ∈ fs) => FSum fs a -> Maybe (f a)+prjF = indexF elemIndex++-- | Inject an element into an FSum with an explicitly+--   specified Index.+injectFSum :: Index fs f -> f a -> FSum fs a+injectFSum = \case+  IZ   -> FInL+  IS x -> FInR . injectFSum x++-- | Project an explicit index out of an FSum.+indexF :: Index fs f -> FSum fs a -> Maybe (f a)+indexF = \case+  IZ -> \case+    FInL a -> Just a+    _      -> Nothing+  IS x -> \case+    FInR s -> indexF x s+    _      -> Nothing++instance ListC (Functor <$> fs) => Functor (FSum fs) where+  fmap f = \case+    FInL a -> FInL $ f <$> a+    FInR s -> FInR $ f <$> s++instance ListC (Foldable <$> fs) => Foldable (FSum fs) where+  foldMap f = \case+    FInL a -> foldMap f a+    FInR s -> foldMap f s++instance+  ( ListC (Functor     <$> fs)+  , ListC (Foldable    <$> fs)+  , ListC (Traversable <$> fs)+  ) => Traversable (FSum fs) where+  traverse f = \case+    FInL a -> FInL <$> traverse f a+    FInR s -> FInR <$> traverse f s++-- | Map over the single element in an FSum+--   with a function that can handle any possible+--   element, along with the element's index.+imapF :: (forall f. Index fs f -> f a -> f b)+  -> FSum fs a -> FSum fs b+imapF f = \case+  FInL a -> FInL $ f IZ a+  FInR s -> FInR $ imapF (f . IS) s++-- | Fun fact: Since there is exactly one element in+--   an FSum, we don't need the @Monoid@ instance!+ifoldMapF :: (forall f. Index fs f -> f a -> m)+  -> FSum fs a -> m+ifoldMapF f = \case+  FInL a -> f IZ a+  FInR s -> ifoldMapF (f . IS) s++-- | Another fun fact: Since there is exactly one element in+--   an FSum, we require only a @Functor@ instance on @g@, rather+--   than @Applicative@.+itraverseF :: Functor g+  => (forall f. Index fs f -> f a -> g (f b))+  -> FSum fs a -> g (FSum fs b)+itraverseF f = \case+  FInL a -> FInL <$> f IZ a+  FInR s -> FInR <$> itraverseF (f . IS) s+
src/Type/Class/Witness.hs view
@@ -77,6 +77,9 @@   id              = Sub Wit   Sub bc . Sub ab = Sub $ bc \\ ab +type (:-:) = Bij (:-)+infixr 4 :-:+ -- | A general eliminator for entailment. -- -- Given a term of type @t@ with an instance @Witness p q t@@@ -159,6 +162,7 @@   id    = Bij id id   g . f = Bij (fwd g . fwd f) (bwd f . bwd g) +{- class Category c => Monoidal (c :: k -> k -> *) where   type Tensor c :: k -> k -> k   type Unit   c :: k@@ -193,6 +197,7 @@ (***) :: Monoidal p => Bij p a b -> Bij p c d -> Bij p (Tensor p a c) (Tensor p b d) f *** g = (fwd f .*. fwd g) <-> (bwd f .*. bwd g) infixr 3 ***+-}  type (<->) = Bij (->) infixr 5 <->
− src/Type/Family/Pair.hs 
@@ -1,58 +0,0 @@-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE GADTs #-}--------------------------------------------------------------------------------- |--- Module      :  Type.Family.Pair--- Copyright   :  Copyright (C) 2015 Kyle Carter--- License     :  BSD3------ Maintainer  :  Kyle Carter <kylcarte@indiana.edu>--- Stability   :  experimental--- Portability :  RankNTypes------ Type-level pairs, along with some convenient aliases and type families--- over them.-----------------------------------------------------------------------------------module Type.Family.Pair where--import Type.Family.Monoid--type (#) = '(,)-infixr 6 #--type family Fst (p :: (k,l)) :: k where-  Fst '(a,b) = a--type family Snd (p :: (k,l)) :: l where-  Snd '(a,b) = b--type family (f :: k -> l) <$> (a :: (m,k)) :: (m,l) where-  f <$> (a#b) = a # f b-infixr 4 <$>--type family (f :: (m,k -> l)) <&> (a :: k) :: (m,l) where-  (r#f) <&> a = r # f a-infixr 4 <&>--type family (f :: (m,k -> l)) <*> (a :: (m,k)) :: (m,l) where-  (r#f) <*> (s#a) = (r <> s) # f a-infixr 4 <*>---- | A type-level pair is a Monoid over its pairwise components.-type instance Mempty = Mempty # Mempty-type instance (r#a) <> (s#b) = (r <> s) # (a <> b)-
+ src/Type/Family/Tuple.hs view
@@ -0,0 +1,70 @@+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE GADTs #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Type.Family.Tuple+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- Type-level pairs and triples, along with some convenient aliases and type families+-- over them.+--+-----------------------------------------------------------------------------++module Type.Family.Tuple where++import Type.Family.Monoid++type (#) = '(,)+infixr 6 #++type family Fst (p :: (k,l)) :: k where+  Fst '(a,b) = a++type family Snd (p :: (k,l)) :: l where+  Snd '(a,b) = b++type family (f :: k -> l) <$> (a :: (m,k)) :: (m,l) where+  f <$> (a#b) = a # f b+infixr 4 <$>++type family (f :: (m,k -> l)) <&> (a :: k) :: (m,l) where+  (r#f) <&> a = r # f a+infixr 4 <&>++type family (f :: (m,k -> l)) <*> (a :: (m,k)) :: (m,l) where+  (r#f) <*> (s#a) = (r <> s) # f a+infixr 4 <*>++-- | A type-level pair is a Monoid over its pairwise components.+type instance Mempty = Mempty # Mempty+type instance (r#a) <> (s#b) = (r <> s) # (a <> b)++type family Fst3 (p :: (k,l,m)) :: k where+  Fst3 '(a,b,c) = a++type family Snd3 (p :: (k,l,m)) :: l where+  Snd3 '(a,b,c) = b++type family Thd3 (p :: (k,l,m)) :: m where+  Thd3 '(a,b,c) = c++type instance Mempty = '(Mempty,Mempty,Mempty)+type instance '(a,b,c) <> '(d,e,f) = '(a<>d,b<>e,c<>f)+
type-combinators.cabal view
@@ -1,24 +1,16 @@ name: type-combinators+version: 0.1.2.0 category: Data-synopsis: A collection of data types for type-level programming.-description: I put this library together first and foremost so that-             I wouldn't need to constantly rewrite the same code-             that uses these types, but also because I noticed a-             growing trend of writing and rewriting bits and pieces-             of code for these types all over the Haskell community.-             Hopefully, this helps! Contributions, criticisms, and-             thoughts are very welcome.  -kylcarte-homepage:      http://github.com/kylcarte/type-combinators-bug-reports:   http://github.com/type-combinators/issues-version: 0.1.0.1+synopsis: A collection of data types for type-level programming cabal-version: >=1.10 build-type: Simple license: BSD3 license-file: LICENSE maintainer: kylcarte@gmail.com author: Kyle Carter+homepage: https://github.com/kylcarte/type-combinators -source-repository head+Source-Repository head     type: git     location: git://github.com/kylcarte/type-combinators.git @@ -29,12 +21,16 @@         Data.Type.Disjunction         Data.Type.Fin         Data.Type.Index+        Data.Type.Index.Quote         Data.Type.Length         Data.Type.Nat+        Data.Type.Nat.Quote         Data.Type.Option         Data.Type.Product-        Data.Type.Quantifier+        Data.Type.Product.Dual         Data.Type.Sum+        Data.Type.Sum.Dual+        Data.Type.Quantifier         Data.Type.Vector         Type.Class.HFunctor         Type.Class.Known@@ -44,9 +40,13 @@         Type.Family.Maybe         Type.Family.Monoid         Type.Family.Nat-        Type.Family.Pair+        Type.Family.Tuple     build-depends:-        base >=4.8 && <4.9+        base >=4.8 && <4.9,+        containers,+        template-haskell,+        transformers,+        mtl     default-language: Haskell2010     hs-source-dirs: src