packages feed

type-combinators (empty) → 0.1.0.0

raw patch · 24 files changed

+2592/−0 lines, 24 filesdep +basesetup-changed

Dependencies added: base

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2015, Kyle Carter++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 Kyle Carter 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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ src/Data/Type/Combinator.hs view
@@ -0,0 +1,298 @@+{-# 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.Combinator+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- A collection of simple type combinators,+-- such as @Identity@ 'I', @Constant@ 'C', @Compose@ '(:.:)',+-- left unnest 'LL', right unnest 'RR', the @S Combinator@ 'SS',+-- etc.+--+-----------------------------------------------------------------------------++module Data.Type.Combinator where++import Type.Class.HFunctor+import Type.Class.Known+import Type.Class.Witness++import Control.Applicative++-- (:.:) {{{++data ((f :: l -> *) :.: (g :: k -> l)) :: k -> * where+  Comp :: { getComp :: f (g a) } -> (f :.: g) a+infixr 6 :.:++deriving instance Eq   (f (g a)) => Eq   ((f :.: g) a)+deriving instance Ord  (f (g a)) => Ord  ((f :.: g) a)+deriving instance Show (f (g a)) => Show ((f :.: g) a)++instance Witness p q (f (g a)) => Witness p q ((f :.: g) a) where+  type WitnessC p q ((f :.: g) a) = Witness p q (f (g a))+  r \\ Comp a = r \\ a++data ((f :: m -> *) :..: (g :: k -> l -> m)) :: k -> l -> * where+  Comp2 :: f (g a b) -> (f :..: g) a b+infixr 6 :..:++deriving instance Eq   (f (g a b)) => Eq   ((f :..: g) a b)+deriving instance Ord  (f (g a b)) => Ord  ((f :..: g) a b)+deriving instance Show (f (g a b)) => Show ((f :..: g) a b)++instance Witness p q (f (g a b)) => Witness p q ((f :..: g) a b) where+  type WitnessC p q ((f :..: g) a b) = Witness p q (f (g a b))+  r \\ Comp2 a = r \\ a++-- }}}++-- IT {{{++data IT :: (k -> *) -> k -> * where+  IT :: { getIT :: f a } -> IT f a++deriving instance Eq   (f a) => Eq   (IT f a)+deriving instance Ord  (f a) => Ord  (IT f a)+deriving instance Show (f a) => Show (IT f a)++instance HFunctor IT where+  map' f = IT . f . getIT++instance HFoldable IT where+  foldMap' f = f . getIT++instance HTraversable IT where+  traverse' f = fmap IT . f . getIT++instance Witness p q (f a) => Witness p q (IT f a) where+  type WitnessC p q (IT f a) = Witness p q (f a)+  r \\ IT a = r \\ a++instance Num (f a) => Num (IT f a) where+  IT a * IT b   = IT $ a * b+  IT a + IT b   = IT $ a + b+  IT a - IT b   = IT $ a - b+  abs    (IT a) = IT $ abs a+  signum (IT a) = IT $ signum a+  fromInteger   = IT . fromInteger++-- }}}++-- I {{{++data I :: * -> * where+  I :: { getI :: a } -> I a++deriving instance Eq   a => Eq   (I a)+deriving instance Ord  a => Ord  (I a)+deriving instance Show a => Show (I a)++instance Functor I where+  fmap f (I a) = I $ f a++instance Applicative I where+  pure = I+  I f <*> I a = I $ f a++instance Monad I where+  I a >>= f = f a++instance Foldable I where+  foldMap f (I a) = f a++instance Traversable I where+  traverse f (I a) = I <$> f a++instance Witness p q a => Witness p q (I a) where+  type WitnessC p q (I a) = Witness p q a+  r \\ I a = r \\ a++instance Num a => Num (I a) where+  (*)         = liftA2 (*)+  (+)         = liftA2 (+)+  (-)         = liftA2 (-)+  abs         = fmap abs+  signum      = fmap signum+  fromInteger = pure . fromInteger++-- }}}++-- LL {{{++newtype LL (a :: k) (f :: l -> *) (g :: k -> l) = LL+  { getLL :: f (g a)+  }++deriving instance Eq   (f (g a)) => Eq   (LL a f g)+deriving instance Ord  (f (g a)) => Ord  (LL a f g)+deriving instance Show (f (g a)) => Show (LL a f g)++instance HFunctor (LL a) where+  map' f = LL . f . getLL++instance HFoldable (LL a) where+  foldMap' f = f . getLL++instance HTraversable (LL a) where+  traverse' f = fmap LL . f . getLL++instance Witness p q (f (g a)) => Witness p q (LL a f g) where+  type WitnessC p q (LL a f g) = Witness p q (f (g a))+  r \\ LL a = r \\ a++-- }}}++-- RR {{{++newtype RR (g :: k -> l) (f :: l -> *) (a :: k) = RR+  { getRR :: f (g a)+  }++deriving instance Eq   (f (g a)) => Eq   (RR g f a)+deriving instance Ord  (f (g a)) => Ord  (RR g f a)+deriving instance Show (f (g a)) => Show (RR g f a)++instance HFunctor (RR g) where+  map' f = RR . f . getRR++instance HFoldable (RR g) where+  foldMap' f = f . getRR++instance HTraversable (RR g) where+  traverse' f = fmap RR . f . getRR++instance Witness p q (f (g a)) => Witness p q (RR g f a) where+  type WitnessC p q (RR g f a) = Witness p q (f (g a))+  r \\ RR a = r \\ a++-- }}}++-- SS {{{++newtype SS (f :: k -> l -> *) (g :: k -> l) :: k -> * where+  SS :: { getSS :: f a (g a) } -> SS f g a++deriving instance Eq   (f a (g a)) => Eq   (SS f g a)+deriving instance Ord  (f a (g a)) => Ord  (SS f g a)+deriving instance Show (f a (g a)) => Show (SS f g a)++instance Witness p q (f a (g a)) => Witness p q (SS f g a) where+  type WitnessC p q (SS f g a) = Witness p q (f a (g a))+  r \\ SS a = r \\ a++-- }}}++-- CT {{{++data CT :: * -> (k -> *) -> l -> * where+  CT :: { getCT :: r } -> CT r f a++deriving instance Eq   r => Eq   (CT r f a)+deriving instance Ord  r => Ord  (CT r f a)+deriving instance Show r => Show (CT r f a)++instance HFunctor (CT r) where+  map' _ (CT r) = CT r++instance HFoldable (CT r) where+  foldMap' _ _ = mempty++instance HTraversable (CT r) where+  traverse' _ (CT r) = pure $ CT r++instance Witness p q r => Witness p q (CT r f a) where+  type WitnessC p q (CT r f a) = Witness p q r+  r \\ CT a = r \\ a++instance Num r => Num (CT r f a) where+  CT a * CT b   = CT $ a * b+  CT a + CT b   = CT $ a + b+  CT a - CT b   = CT $ a - b+  abs    (CT a) = CT $ abs a+  signum (CT a) = CT $ signum a+  fromInteger   = CT . fromInteger++-- }}}++-- C {{{++data C :: * -> k -> * where+  C :: { getC :: r } -> C r a++deriving instance Eq   r => Eq   (C r a)+deriving instance Ord  r => Ord  (C r a)+deriving instance Show r => Show (C r a)++instance Witness p q r => Witness p q (C r a) where+  type WitnessC p q (C r a) = Witness p q r+  r \\ C a = r \\ a++instance Num r => Num (C r a) where+  C a * C b    = C $ a * b+  C a + C b    = C $ a + b+  C a - C b    = C $ a - b+  abs    (C a) = C $ abs a+  signum (C a) = C $ signum a+  fromInteger  = C . fromInteger++-- }}}++-- Join {{{++newtype Join f a = Join+  { getJoin :: f a a+  }++deriving instance Eq   (f a a) => Eq   (Join f a)+deriving instance Ord  (f a a) => Ord  (Join f a)+deriving instance Show (f a a) => Show (Join f a)++instance Known (f a) a => Known (Join f) a where+  type KnownC (Join f) a = Known (f a) a+  known = Join known++instance Witness p q (f a a) => Witness p q (Join f a) where+  type WitnessC p q (Join f a) = Witness p q (f a a)+  r \\ Join a = r \\ a+  ++-- }}}++-- Flip {{{++newtype Flip p b a = Flip+  { getFlip :: p a b+  } deriving (Eq,Ord,Show)++instance Known (p a) b => Known (Flip p b) a where+  type KnownC (Flip p b) a = Known (p a) b+  known = Flip known++instance Witness p q (f a b) => Witness p q (Flip f b a) where+  type WitnessC p q (Flip f b a) = Witness p q (f a b)+  r \\ Flip a = r \\ a++flipped :: (f a b -> g c d) -> Flip f b a -> Flip g d c+flipped f = Flip . f . getFlip++-- }}}+
+ src/Data/Type/Conjunction.hs view
@@ -0,0 +1,149 @@+{-# 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.Conjunction+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- Two type combinators for working with conjunctions:+-- A /fanout/ combinator '(:&:)', and a /par/ combinator '(:*:)'.+--+-- These are analogous to '(&&&)' and '(***)' from 'Control.Arrow',+-- respectively.+--+-----------------------------------------------------------------------------++module Data.Type.Conjunction where++import Type.Class.HFunctor+import Type.Class.Known+import Type.Class.Witness+import Type.Family.Pair++-- (:&:) {{{++data ((f :: k -> *) :&: (g :: k -> *)) :: k -> * where+  (:&:) :: !(f a) -> !(g a) -> (f :&: g) a+infixr 5 :&:++deriving instance (Eq   (f a), Eq   (g a)) => Eq   ((f :&: g) a)+deriving instance (Ord  (f a), Ord  (g a)) => Ord  ((f :&: g) a)+deriving instance (Show (f a), Show (g a)) => Show ((f :&: g) a)++fanFst :: (f :&: g) a -> f a+fanFst (a :&: _) = a++fanSnd :: (f :&: g) a -> g a+fanSnd (_ :&: b) = b++uncurryFan :: (f a -> g a -> r) -> (f :&: g) a -> r+uncurryFan f (a :&: b) = f a b++curryFan :: ((f :&: g) a -> r) -> f a -> g a -> r+curryFan f a b = f (a :&: b)++instance DecEquality f => DecEquality (f :&: g) where+  decideEquality (a :&: _) (c :&: _) = decideEquality a c++instance (Known f a, Known g a) => Known (f :&: g) a where+  known = known :&: known++instance HFunctor ((:&:) f) where+  map' f (a :&: b) = a :&: f b++instance HFoldable ((:&:) f) where+  foldMap' f (_ :&: b) = f b++instance HTraversable ((:&:) f) where+  traverse' f (a :&: b) = (:&:) a <$> f b++instance HBifunctor (:&:) where+  bimap' f g (a :&: b) = f a :&: g b++instance (Witness p q (f a), Witness s t (g a)) => Witness (p,s) (q,t) ((f :&: g) a) where+  type WitnessC (p,s) (q,t) ((f :&: g) a) = (Witness p q (f a), Witness s t (g a))+  r \\ a :&: b = r \\ a \\ b++{-+instance Witness p q (f a) => Witness p q (WitFst (:&:) f g a) where+  r \\ WitFst (a :&: _) = r \\ a++instance Witness p q (g a) => Witness p q (WitSnd (:&:) f g a) where+  r \\ WitSnd (_ :&: b) = r \\ b+-}++-- }}}++-- (:*:) {{{++data ((f :: k -> *) :*: (g :: l -> *)) :: (k,l) -> * where+  (:*:) :: !(f a) -> !(g b) -> (f :*: g) (a#b)+infixr 5 :*:++deriving instance (Eq   (f (Fst p)), Eq   (g (Snd p))) => Eq   ((f :*: g) p)+deriving instance (Ord  (f (Fst p)), Ord  (g (Snd p))) => Ord  ((f :*: g) p)+deriving instance (Show (f (Fst p)), Show (g (Snd p))) => Show ((f :*: g) p)++parFst :: (f :*: g) p -> f (Fst p)+parFst (a :*: _) = a++parSnd :: (f :*: g) p -> g (Snd p)+parSnd (_ :*: b) = b++uncurryPar :: (forall a b. (p ~ (a#b)) => f a -> g b -> r) -> (f :*: g) p -> r+uncurryPar f (a :*: b) = f a b++curryPar :: ((f :*: g) (a#b) -> r) -> f a -> g b -> r+curryPar f a b = f (a :*: b)++instance (p ~ (a#b), Known f a, Known g b) => Known (f :*: g) p where+  known = known :*: known++instance HFunctor ((:*:) f) where+  map' f (a :*: b) = a :*: f b++instance HFoldable ((:*:) f) where+  foldMap' f (_ :*: b) = f b++instance HTraversable ((:*:) f) where+  traverse' f (a :*: b) = (:*:) a <$> f b++instance HBifunctor (:*:) where+  bimap' f g (a :*: b) = f a :*: g b++_fst :: (a#b) :~: (c#d) -> a :~: c+_fst Refl = Refl++_snd :: (a#b) :~: (c#d) -> b :~: d+_snd Refl = Refl++instance (DecEquality f, DecEquality g) => DecEquality (f :*: g) where+  decideEquality (a :*: b) (c :*: d) = case decideEquality a c of+    Proven    p -> case decideEquality b d of+      Proven  q -> Proven  $ Refl \\ p \\ q+      Refuted q -> Refuted $ q . _snd+    Refuted   p -> Refuted $ p . _fst++instance (Witness p q (f a), Witness s t (g b), x ~ (a#b)) => Witness (p,s) (q,t) ((f :*: g) x) where+  type WitnessC (p,s) (q,t) ((f :*: g) x) = (Witness p q (f (Fst x)), Witness s t (g (Snd x)))+  r \\ a :*: b = r \\ a \\ b++-- }}}+
+ src/Data/Type/Disjunction.hs view
@@ -0,0 +1,130 @@+{-# 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.Disjunction+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- Two type combinators for working with disjunctions:+-- A /branch/ combinator '(:+:)', and a /choice/ combinator '(:|:)'.+--+-- These are analogous to '(+++)' and '(|||)' from 'Control.Arrow',+-- respectively.+--+-----------------------------------------------------------------------------++module Data.Type.Disjunction where++import Type.Class.HFunctor+import Type.Class.Known+import Type.Class.Witness++-- (:+:) {{{++data ((f :: k -> *) :+: (g :: k -> *)) :: k -> * where+  L :: !(f a) -> (f :+: g) a+  R :: !(g a) -> (f :+: g) a+infixr 4 :+:++(>+<) :: (f a -> r) -> (g a -> r) -> (f :+: g) a -> r+f >+< g = \case+  L a -> f a+  R b -> g b+infixr 2 >+<++instance HFunctor ((:+:) f) where+  map' f = \case+    L a -> L a+    R b -> R $ f b++instance HFoldable ((:+:) f) where+  foldMap' f = \case+    L _ -> mempty+    R b -> f b++instance HTraversable ((:+:) f) where+  traverse' f = \case+    L a -> pure $ L a+    R b -> R <$> f b++instance HBifunctor (:+:) where+  bimap' f g = \case+    L a -> L $ f a+    R b -> R $ g b++instance (Witness p q (f a), Witness p q (g a)) => Witness p q ((f :+: g) a) where+  type WitnessC p q ((f :+: g) a) = (Witness p q (f a), Witness p q (g a))+  (\\) r = \case+    L a -> r \\ a+    R b -> r \\ b++-- }}}++-- (:|:) {{{++data ((f :: k -> *) :|: (g :: l -> *)) :: Either k l -> * where+  L' :: !(f a) -> (f :|: g) (Left  a)+  R' :: !(g b) -> (f :|: g) (Right b)+infixr 4 :|:++(>|<) :: (forall a. (e ~ Left a) => f a -> r) -> (forall b. (e ~ Right b) => g b -> r) -> (f :|: g) e -> r+f >|< g = \case+  L' a -> f a+  R' b -> g b+infixr 2 >|<++instance Known f a => Known (f :|: g) (Left a) where+  type KnownC (f :|: g) (Left a) = Known f a+  known = L' known++instance Known g b => Known (f :|: g) (Right b) where+  type KnownC (f :|: g) (Right b) = Known g b+  known = R' known++instance HFunctor ((:|:) f) where+  map' f = \case+    L' a -> L' a+    R' b -> R' $ f b++instance HFoldable ((:|:) f) where+  foldMap' f = \case+    L' _ -> mempty+    R' b -> f b++instance HTraversable ((:|:) f) where+  traverse' f = \case+    L' a -> pure $ L' a+    R' b -> R' <$> f b++instance HBifunctor (:|:) where+  bimap' f g = \case+    L' a -> L' $ f a+    R' b -> R' $ g b++instance Witness p q (f a) => Witness p q ((f :|: g) (Left a)) where+  type WitnessC p q ((f :|: g) (Left a)) = Witness p q (f a)+  r \\ L' a = r \\ a++instance Witness p q (g b) => Witness p q ((f :|: g) (Right b)) where+  type WitnessC p q ((f :|: g) (Right b)) = Witness p q (g b)+  r \\ R' b = r \\ b++-- }}}+
+ src/Data/Type/Fin.hs view
@@ -0,0 +1,114 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# 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.Fin+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- A @singleton@-esque type for representing members of finite sets.+--+-----------------------------------------------------------------------------++module Data.Type.Fin where++import Data.Type.Combinator+import Data.Type.Nat+import Type.Class.Known+import Type.Class.Witness+import Type.Family.Constraint+import Type.Family.Nat+import Data.Type.Quantifier++data Fin :: N -> * where+  FZ :: Fin (S n)+  FS :: !(Fin n) -> Fin (S n)++deriving instance Eq   (Fin n)+deriving instance Ord  (Fin n)+deriving instance Show (Fin n)++-- | Gives the list of all members of the finite set of size @n@.+fins :: Nat n -> [Fin n]+fins = \case+  Z_   -> []+  S_ x -> FZ : map FS (fins x)++fin :: Fin n -> Int+fin = \case+  FZ   -> 0+  FS x -> succ $ fin x++-- | There are no members of @Fin Z@.+finZ :: Fin Z -> Void+finZ = impossible++weaken :: Fin n -> Fin (S n)+weaken = \case+  FZ   -> FZ+  FS n -> FS $ weaken n++-- | Map a finite set to a lower finite set without+-- one of its members.+without :: Fin n -> Fin n -> Maybe (Fin (Pred n))+without = \case+  FZ -> \case+    FZ   -> Nothing+    FS y -> Just y+  FS x -> \case+    FZ   -> Just FZ \\ x+    FS y -> FS <$> without x y \\ x++class (x :: N) <= (y :: N) where+  weakenN :: Fin x -> Fin y++instance {-# OVERLAPPING #-} x <= x where+  weakenN = id++instance {-# OVERLAPPABLE #-} (x <= y) => x <= S y where+  weakenN = weaken . weakenN++{-+instance Known Nat n => Known ([] :.: Fin) n where+  type KnownC ([] :.: Fin) n = Known Nat n+  known = Comp $ go (known :: Nat n)+    where+    go :: Nat x -> [Fin x]+    go = \case+      Z_   -> []+      S_ x -> FZ : map FS (go x)+-}++-- | Take a 'Fin' to an existentially quantified 'Nat'.+finNat :: Fin x -> Some Nat+finNat = \case+  FZ   -> Some Z_+  FS x -> withSome (Some . S_) $ finNat x++-- | A @Fin n@ is a 'Witness' that @n >= 1@.+--+-- That is, @'Pred' n@ is well defined.+instance (n' ~ Pred n) => Witness ØC (S n' ~ n) (Fin n) where+  type WitnessC ØC (S n' ~ n) (Fin n) = (n' ~ Pred n)+  (\\) r = \case+    FZ   -> r+    FS _ -> r+
+ src/Data/Type/Index.hs view
@@ -0,0 +1,63 @@+{-# 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+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- A @singleton@-esque type for representing indices in a type-level list.+--+-----------------------------------------------------------------------------++module Data.Type.Index where++import Type.Class.HFunctor+import Type.Class.Known+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++deriving instance Eq   (Index as a)+deriving instance Ord  (Index as a)+deriving instance Show (Index as a)++type a ∈ as = Elem as a+infix 6 ∈++class Elem (as :: [k]) (a :: k) where+  elemIndex :: Index as a++instance {-# OVERLAPPING #-} Elem (a :< as) a where+  elemIndex = IZ++instance {-# OVERLAPPABLE #-} Elem as a => Elem (b :< as) a where+  elemIndex = IS elemIndex++instance {-# OVERLAPPING #-} Known (Index (a :< as)) a where+  known = IZ++instance {-# OVERLAPPABLE #-} Known (Index as) a => Known (Index (b :< as)) a where+  known = IS known+
+ src/Data/Type/Length.hs view
@@ -0,0 +1,57 @@+{-# 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.Length+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- A @singleton@-esque type for representing lengths of type-level lists,+-- irrespective of the actual types in that list.+--+-----------------------------------------------------------------------------++module Data.Type.Length where++import Type.Class.Known+import Type.Family.List++data Length :: [k] -> * where+  LZ :: Length Ø+  LS :: !(Length as) -> Length (a :< as)++lOdd, lEven :: Length as -> Bool+lOdd = \case+  LZ   -> False+  LS l -> lEven l+lEven = \case+  LZ   -> True+  LS l -> lOdd l++deriving instance Eq   (Length as)+deriving instance Ord  (Length as)+deriving instance Show (Length as)++instance Known Length Ø where+  known = LZ++instance Known Length as => Known Length (a :< as) where+  type KnownC Length (a :< as) = Known Length as+  known = LS known+
+ src/Data/Type/Nat.hs view
@@ -0,0 +1,154 @@+{-# 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.Nat+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- A @singleton@-esque type for representing Peano natural numbers.+--+-----------------------------------------------------------------------------++module Data.Type.Nat where++import Data.Type.Equality+import Data.Type.Product+import Type.Class.Known+import Type.Class.Witness+import Type.Family.Constraint+import Type.Family.List+import Type.Family.Nat++data Nat :: N -> * where+  Z_ :: Nat Z+  S_ :: !(Nat n) -> Nat (S n)++deriving instance Eq   (Nat n)+deriving instance Ord  (Nat n)+deriving instance Show (Nat n)++-- | @'Z_'@ is the canonical construction of a @'Nat' Z@.+instance Known Nat Z where+  known = Z_++-- | If @n@ is a canonical construction of @Nat n@,+-- @'S_' n@ is the canonical construction of @Nat (S n)@.+instance Known Nat n => Known Nat (S n) where+  type KnownC Nat (S n) = Known Nat n+  known = S_ known++-- | A @Nat n@ is a 'Witness' that there is a canonical+-- construction for @Nat n@.+instance Witness ØC (Known Nat n) (Nat n) where+  (\\) r = \case+    Z_   -> r+    S_ x -> r \\ x++instance TestEquality Nat where+  testEquality = \case+    Z_ -> \case+      Z_   -> Just Refl+      S_ _ -> Nothing+    S_ x -> \case+      Z_   -> Nothing+      S_ y -> testEquality x y /? qed++instance DecEquality Nat where+  decideEquality = \case+    Z_ -> \case+      Z_   -> Proven  _Z+      S_ _ -> Refuted _ZneS+    S_ x -> \case+      Z_   -> Refuted $ _ZneS . sym+      S_ y -> (_S <-> _s) <?> decideEquality x y++_Z :: Z :~: Z+_Z = Refl++_S :: x :~: y -> S x :~: S y+_S Refl = Refl++_s :: S x :~: S y -> x :~: y+_s Refl = Refl++_ZneS :: Z :~: S x -> Void+_ZneS = impossible++-- | A proof that 'Z' is also a right identity+-- for the addition of type-level 'Nat's.+addZ :: Nat x -> (x + Z) :~: x+addZ = \case+  Z_   -> Refl+  S_ x -> _S $ addZ x+{-# INLINE addZ #-}++addS :: Nat x -> Nat y -> S (x + y) :~: (x + S y)+addS = \case+  Z_   -> pure Refl+  S_ x -> _S . addS x+{-# INLINE addS #-}++(.+) :: Nat x -> Nat y -> Nat (x + y)+(.+) = \case+  Z_   -> id+  S_ x -> S_ . (x .+)+infixr 6 .+++(.*) :: Nat x -> Nat y -> Nat (x * y)+(.*) = \case+  Z_   -> const Z_+  S_ x -> (.+) <$> (x .*) <*> id+infixr 7 .*++(.^) :: Nat x -> Nat y -> Nat (x ^ y)+(.^) x = \case+  Z_   -> S_ Z_+  S_ y -> (x .^ y) .* x+infixl 8 .^++nat :: Nat n -> Int+nat = \case+  Z_   -> 0+  S_ x -> succ $ nat x++n0  :: Nat N0+n1  :: Nat N1+n2  :: Nat N2+n3  :: Nat N3+n4  :: Nat N4+n5  :: Nat N5+n6  :: Nat N6+n7  :: Nat N7+n8  :: Nat N8+n9  :: Nat N9+n10 :: Nat N10++n0  = Z_+n1  = S_ n0+n2  = S_ n1+n3  = S_ n2+n4  = S_ n3+n5  = S_ n4+n6  = S_ n5+n7  = S_ n6+n8  = S_ n7+n9  = S_ n8+n10 = S_ n9+
+ src/Data/Type/Option.hs view
@@ -0,0 +1,76 @@+{-# 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.Option+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- A type combinator for type-level @Maybe@s,+-- lifting @(f :: k -> *)@ to @(Option f :: Maybe k -> *)@.+--+-----------------------------------------------------------------------------++module Data.Type.Option where++import Type.Class.HFunctor+import Type.Class.Known+import Type.Class.Witness+import Type.Family.Maybe++data Option (f :: k -> *) :: Maybe k -> * where+  Nothing_ :: Option f Nothing+  Just_    :: !(f a) -> Option f (Just a)++-- | Eliminator for @'Option' f@.+option :: (forall a. (m ~ Just a) => f a -> r) -> ((m ~ Nothing) => r) -> Option f m -> r+option j n = \case+  Just_ a  -> j a+  Nothing_ -> n++-- | We can take a natural transformation of @(forall x. f x -> g x)@ to+-- a natural transformation of @(forall mx. 'Option' f mx -> 'Option' g mx)@.+instance HFunctor Option where+  map' f = \case+    Just_ a  -> Just_ $ f a+    Nothing_ -> Nothing_++instance HFoldable Option where+  foldMap' f = \case+    Just_ a  -> f a+    Nothing_ -> mempty++instance HTraversable Option where+  traverse' f = \case+    Just_ a  -> Just_ <$> f a+    Nothing_ -> pure Nothing_++instance Known (Option f) Nothing where+  known = Nothing_++instance Known f a => Known (Option f) (Just a) where+  type KnownC (Option f) (Just a) = Known f a+  known = Just_ known++instance (Witness p q (f a), x ~ Just a) => Witness p q (Option f x) where+  type WitnessC p q (Option f x) = Witness p q (f (FromJust x))+  (\\) r = \case+    Just_ a -> r \\ a+    _       -> error "impossible type"+
+ src/Data/Type/Product.hs view
@@ -0,0 +1,148 @@+{-# 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.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'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.Combinator ((:.:)(..),IT(..))+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++data Prod (f :: k -> *) :: [k] -> * where+  Ø    :: Prod f Ø+  (:<) :: !(f a) -> !(Prod f as) -> Prod f (a :< as)+infixr 5 :<++pattern (:>) :: (f :: k -> *) (a :: k) -> f (b :: k) -> Prod f '[a,b]+pattern a :> b = a :< b :< Ø+infix 6 :>++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++(>:) :: 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++init' :: Prod f (a :< as) -> Prod f (Init' a as)+init' (a :< as) = case as of+  Ø      -> Ø+  (:<){} -> a :< init' as++last' :: Prod f (a :< as) -> f (Last' a as)+last' (a :< as) = case as of+  Ø      -> a+  (:<){} -> last' as++append' :: Prod f as -> Prod f bs -> Prod f (as ++ bs)+append' = \case+  Ø       -> id+  a :< as -> (a :<) . append' 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'++instance HFunctor Prod where+  map' f = \case+    Ø -> Ø+    a :< as -> f a :< map' f as++instance HIxFunctor Index Prod where+  imap' f = \case+    Ø -> Ø+    a :< as -> f IZ a :< imap' (f . IS) as++instance HFoldable Prod where+  foldMap' f = \case+    Ø       -> mempty+    a :< as -> f a `mappend` foldMap' f as++instance HIxFoldable Index Prod where+  ifoldMap' f = \case+    Ø       -> mempty+    a :< as -> f IZ a `mappend` ifoldMap' (f . IS) as++instance HTraversable Prod where+  traverse' f = \case+    Ø       -> pure Ø+    a :< as -> (:<) <$> f a <*> traverse' f as++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++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+
+ src/Data/Type/Quantifier.hs view
@@ -0,0 +1,76 @@+{-# 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.Quantifier+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- Types for working with (and under) existentially and universally+-- quantified types.+--+-- The 'Some' type can be very useful when working with type-indexed GADTs,+-- where defining instances for classes like 'Read' can be tedious at best,+-- and frequently impossible, for the GADT itself.+--+-----------------------------------------------------------------------------++module Data.Type.Quantifier where++import Data.Type.Combinator++data Some (f :: k -> *) :: * where+  Some :: f a -> Some f++-- | An eliminator for a 'Some' type.+--+-- NB: the result type of the eliminating function may+-- not refer to the universally quantified type index @a@.+--+-- 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.+some :: Some f -> (forall a. f a -> r) -> r+some (Some a) f = f a++withSome :: (forall a. f a -> r) -> Some f -> r+withSome f (Some a) = f a++onSome :: (forall a. f a -> g b) -> Some f -> Some g+onSome f (Some a) = Some (f a)++type Some2 f = Some (Some :.: f)++pattern Some2 :: f a b -> Some2 f+pattern Some2 a = Some (Comp (Some a))++data All (f :: k -> *) :: * where+  All :: { instAll :: forall (a :: k). f a } -> All f++-- | A data type for natural transformations.+data (f :: k -> *) :-> (g :: k -> *) where+  NT :: (forall a. f a -> g a) -> f :-> g+infixr 4 :->++data (p :: k -> l -> *) :--> (q :: k -> l -> *) where+  NT2 :: (forall a b. p a b -> q a b) -> p :--> q+infixr 4 :-->+
+ src/Data/Type/Sum.hs view
@@ -0,0 +1,150 @@+{-# 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+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- 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.+--+-----------------------------------------------------------------------------++module Data.Type.Sum where++import Data.Type.Index++import Type.Class.HFunctor+import Type.Class.Witness++import Type.Family.Constraint+import Type.Family.List++data Sum (f :: k -> *) :: [k] -> * where+  InL :: !(f a) -> Sum f (a :< as)+  InR :: !(Sum f as) -> Sum f (a :< as)++decomp :: Sum f (a :< as) -> Either (f a) (Sum f as)+decomp = \case+  InL a -> Left  a+  InR s -> Right s++injectSum :: Index as a -> f a -> Sum f as+injectSum = \case+  IZ   -> InL+  IS x -> InR . injectSum x++inj :: (a ∈ as) => f a -> Sum f as+inj = injectSum elemIndex++prj :: (a ∈ as) => Sum f as -> Maybe (f a)+prj = index elemIndex++index :: Index as a -> Sum f as -> Maybe (f a)+index = \case+  IZ -> \case+    InL a -> Just a+    _     -> Nothing+  IS x -> \case+    InR s -> index x s+    _     -> Nothing++-- instances {{{++instance HFunctor Sum where+  map' f = \case+    InL a -> InL $ f a+    InR s -> InR $ map' f s++instance HIxFunctor Index Sum where+  imap' f = \case+    InL a -> InL $ f IZ a+    InR s -> InR $ imap' (f . IS) s++instance HFoldable Sum where+  foldMap' f = \case+    InL a -> f a+    InR s -> foldMap' f s++instance HIxFoldable Index Sum where+  ifoldMap' f = \case+    InL a -> f IZ a+    InR s -> ifoldMap' (f . IS) s++instance HTraversable Sum where+  traverse' f = \case+    InL a -> InL <$> f a+    InR s -> InR <$> traverse' f s++instance HIxTraversable Index Sum where+  itraverse' f = \case+    InL a -> InL <$> f IZ a+    InR s -> InR <$> itraverse' (f . IS) s++instance Witness p q (f a) => Witness p q (Sum f '[a]) where+  type WitnessC p q (Sum f '[a]) = Witness p q (f a)+  (\\) r = \case+    InL a -> r \\ a+    _     -> error "impossible type"++instance (Witness p q (f a), Witness p q (Sum f (b :< as))) => Witness p q (Sum f (a :< b :< as)) where+  type WitnessC p q (Sum f (a :< b :< as)) = (Witness p q (f a), Witness p q (Sum f (b :< as)))+  (\\) r = \case+    InL a -> r \\ a+    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/Vector.hs view
@@ -0,0 +1,400 @@+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# 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.Vector+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- 'V' and its combinator analog 'VT' represent lists+-- of known length, characterized by the index @(n :: N)@ in+-- @'V' n a@ or @'VT' n f a@.+--+-- The classic example used ad nauseum for type-level programming.+--+-- The operations on 'V' and 'VT' correspond to the type level arithmetic+-- operations on the kind 'N'.+--+-----------------------------------------------------------------------------++module Data.Type.Vector where++import Data.Type.Combinator+import Data.Type.Fin+import Data.Type.Length+import Data.Type.Nat+import Data.Type.Product (Prod(..),curry',pattern (:>))++import Type.Class.HFunctor+import Type.Class.Known+import Type.Class.Witness++import Type.Family.Constraint+import Type.Family.List+import Type.Family.Nat++import Control.Applicative+import Control.Arrow+import Control.Monad (join)+import qualified Data.List as L+import Data.Monoid+import qualified Data.Foldable as F++data VT (n :: N) (f :: k -> *) :: k -> * where+  ØV   :: VT Z f a+  (:*) :: !(f a) -> !(VT n f a) -> VT (S n) f a+infixr 4 :*++type V n = VT n I+pattern (:+) :: a -> V n a -> V (S n) a+pattern a :+ as = I a :* as+infixr 4 :+++deriving instance Eq   (f a) => Eq   (VT n f a)+deriving instance Ord  (f a) => Ord  (VT n f a)+deriving instance Show (f a) => Show (VT n f a)++(.++) :: VT x f a -> VT y f a -> VT (x + y) f a+(.++) = \case+  ØV      -> id+  a :* as -> (a :*) . (as .++)+infixr 5 .++++vrep :: forall n f a. Known Nat n => f a -> VT n f a+vrep a = go (known :: Nat n)+  where+  go :: Nat x -> VT x f a+  go = \case+    Z_   -> ØV+    S_ x -> a :* go x++head' :: VT (S n) f a -> f a+head' (a :* _) = a++tail' :: VT (S n) f a -> VT n f a+tail' (_ :* as) = as++onTail :: (VT m f a -> VT n f a) -> VT (S m) f a -> VT (S n) f a+onTail f (a :* as) = a :* f as++vDel :: Fin n -> VT n f a -> VT (Pred n) f a+vDel = \case+  FZ   -> tail'+  FS x -> onTail (vDel x) \\ x++imap :: (Fin n -> f a -> g b) -> VT n f a -> VT n g b+imap f = \case+  ØV      -> ØV+  a :* as -> f FZ a :* imap (f . FS) as++ifoldMap :: Monoid m => (Fin n -> f a -> m) -> VT n f a -> m+ifoldMap f = \case+  ØV      -> mempty+  a :* as -> f FZ a <> ifoldMap (f . FS) as++itraverse :: Applicative h => (Fin n -> f a -> h (g b)) -> VT n f a -> h (VT n g b)+itraverse f = \case+  ØV      -> pure ØV+  a :* as -> (:*) <$> f FZ a <*> itraverse (f . FS) as++index :: Fin n -> VT n f a -> f a+index = \case+  FZ   -> head'+  FS x -> index x . tail'++vmap :: (f a -> g b) -> VT n f a -> VT n g b+vmap f = \case+  ØV      -> ØV+  a :* as -> f a :* vmap f as++vap :: (f a -> g b -> h c) -> VT n f a -> VT n g b -> VT n h c+vap f = \case+  ØV  -> \_ -> ØV+  a :* as -> \case+    b :* bs -> f a b :* vap f as bs+    _       -> error "impossible type"++vfoldr :: (f a -> b -> b) -> b -> VT n f a -> b+vfoldr s z = \case+  ØV      -> z+  a :* as -> s a $ vfoldr s z as++vfoldMap' :: (b -> b -> b) -> b -> (f a -> b) -> VT n f a -> b+vfoldMap' j z f = \case+  ØV       -> z+  a :* ØV  -> f a+  a :* as  -> j (f a) $ vfoldMap' j z f as++vfoldMap :: Monoid m => (f a -> m) -> VT n f a -> m+vfoldMap f = \case+  ØV      -> mempty+  a :* as -> f a <> vfoldMap f as++withVT :: [f a] -> (forall n. VT n f a -> r) -> r+withVT as k = case as of+  []     -> k ØV+  a : as -> withVT as $ \v -> k $ a :* v++withV :: [a] -> (forall n. V n a -> r) -> r+withV as k = withVT (I <$> as) k++findV :: Eq a => a -> V n a -> Maybe (Fin n)+findV = findVT . I++findVT :: Eq (f a) => f a -> VT n f a -> Maybe (Fin n)+findVT a = \case+  ØV      -> Nothing+  b :* as -> if a == b+    then Just FZ+    else FS <$> findVT a as++instance Functor f => Functor (VT n f) where+  fmap = vmap . fmap++instance (Applicative f, Known Nat n) => Applicative (VT n f) where+  pure  = vrep . pure+  (<*>) = vap (<*>)++instance (Monad f, Known Nat n) => Monad (VT n f) where+  v >>= f = imap (\x -> (>>= index x . f)) v++instance Foldable f => Foldable (VT n f) where+  foldMap f = \case+    ØV      -> mempty+    a :* as -> foldMap f a <> foldMap f as++instance Traversable f => Traversable (VT n f) where+  traverse f = \case+    ØV      -> pure ØV+    a :* as -> (:*) <$> traverse f a <*> traverse f as++{-+instance (Witness p q (f a), n ~ S x) => Witness p q (VT n f a) where+  type WitnessC p q (VT n f a) = Witness p q (f a)+  (\\) r = \case+    a :* _ -> r \\ a+    _      -> error "impossible type"+-}++instance Witness ØC (Known Nat n) (VT n f a) where+  (\\) r = \case+    ØV      -> r+    _ :* as -> r \\ as++instance (Num (f a), Known Nat n) => Num (VT n f a) where+  (*)         = vap (*)+  (+)         = vap (+)+  (-)         = vap (-)+  negate      = vmap negate+  abs         = vmap abs+  signum      = vmap signum+  fromInteger = vrep . fromInteger++newtype M ns a = M { getMatrix :: Matrix ns a }++deriving instance Eq   (Matrix ns a) => Eq   (M ns a)+deriving instance Ord  (Matrix ns a) => Ord  (M ns a)+deriving instance Show (Matrix ns a) => Show (M ns a)++instance Num (Matrix ns a) => Num (M ns a) where+  fromInteger  = M . fromInteger+  M a * M b    = M $ a * b+  M a + M b    = M $ a + b+  M a - M b    = M $ a - b+  abs (M a)    = M $ abs a+  signum (M a) = M $ signum a++type family Matrix (ns :: [N]) :: * -> * where+  Matrix Ø         = I+  Matrix (n :< ns) = VT n (Matrix ns)++vgen_ :: Known Nat n => (Fin n -> f a) -> VT n f a+vgen_ = vgen known++vgen :: Nat n -> (Fin n -> f a) -> VT n f a+vgen x f = case x of+  Z_   -> ØV+  S_ y -> f FZ :* vgen y (f . FS)++mgen_ :: Known (Prod Nat) ns => (Prod Fin ns -> a) -> M ns a+mgen_ = mgen known++mgen :: Prod Nat ns -> (Prod Fin ns -> a) -> M ns a+mgen ns f = case ns of+  Ø        -> M $ I $ f Ø+  n :< ns' -> M $ vgen n $ getMatrix . mgen ns' . curry' f++onMatrix :: (Matrix ms a -> Matrix ns b) -> M ms a -> M ns b+onMatrix f = M . f . getMatrix++diagonal :: VT n (VT n f) a -> VT n f a+diagonal = imap index++vtranspose :: Known Nat n => VT m (VT n f) a -> VT n (VT m f) a+vtranspose v = vgen_ $ \x -> vmap (index x) v++transpose :: Known Nat n => M (m :< n :< ns) a -> M (n :< m :< ns) a+transpose = onMatrix vtranspose++m0 :: M Ø Int+m0 = 1++m1 :: M '[N2] Int+m1 = 2++m2 :: M '[N2,N4] Int+m2 = 3++m3 :: M '[N2,N3,N4] (Int,Int,Int)+m3 = mgen_ $ \(x :< y :> z) -> (fin x,fin y,fin z)++m4 :: M '[N2,N3,N4,N5] (Int,Int,Int,Int)+m4 = mgen_ $ \(w :< x :< y :> z) -> (fin w,fin x,fin y,fin z)++ppVec :: (VT n ((->) String) String -> ShowS) -> (f a -> ShowS) -> VT n f a -> ShowS+ppVec pV pF = pV . vmap pF++ppMatrix :: forall ns a. (Show a, Known Length ns) => M ns a -> IO ()+ppMatrix = putStrLn . ($ "") . ppMatrix' (known :: Length ns) . getMatrix++ppMatrix' :: Show a => Length ns -> Matrix ns a -> ShowS+ppMatrix' = \case+  LZ   -> shows . getI+  LS l -> ppVec+    ( vfoldMap'+      ( if lEven l+        then zipLines $ \x y -> x . showChar '|'  . y+        else            \x y -> x . showChar '\n' . y+      ) (showString "[]") id+    ) $ ppMatrix' l++mzipWith :: Monoid a => (a -> a -> b) -> [a] -> [a] -> [b]+mzipWith f as bs = case (as,bs) of+  ([]  ,[]  ) -> []+  (a:as,[]  ) -> f a      mempty : mzipWith f as []+  ([]  ,b:bs) -> f mempty b      : mzipWith f [] bs+  (a:as,b:bs) -> f a      b      : mzipWith f as bs++zipLines :: (ShowS -> ShowS -> ShowS) -> ShowS -> ShowS -> ShowS+zipLines f a b = compose $ L.intersperse (showChar '\n') $ mzipWith+  (\(Endo x) (Endo y) -> f x y)+  (Endo . showString <$> lines (a ""))+  (Endo . showString <$> lines (b ""))++{-+juxtLines :: (ShowS -> ShowS -> ShowS) -> ShowS -> ShowS -> ShowS+juxtLines f a b = appEndo $ foldMap id $ mzip (\x y -> Endo $ f (appEndo x) (appEndo y)) as bs+  where+  as = map (Endo . showString) $ lines $ a ""+  bs = map (Endo . showString) $ lines $ b ""+-}++compose :: Foldable f => f (a -> a) -> a -> a+compose = appEndo . foldMap Endo++{-+-- Linear {{{++class Functor f => Additive f where+  zero   :: Num a => f a+  (^+^)  :: Num a => f a -> f a -> f a+  (^-^)  :: Num a => f a -> f a -> f a+  lerp   :: Num a =>   a -> f a -> f a -> f a+  liftU2 :: (a -> a -> a) -> f a -> f a -> f a+  liftI2 :: (a -> b -> c) -> f a -> f b -> f c+  --------+  default zero :: (Applicative f, Num a) => f a+  zero = pure 0+  (^+^)   = liftU2 (+)+  a ^-^ b = a ^+^ negated b+  lerp alpha a b = alpha *^ a ^+^ (1 - alpha) *^ b+  default liftU2 :: Applicative f => (a -> a -> a) -> f a -> f a -> f a+  liftU2 = liftA2+  default liftI2 :: Applicative f => (a -> b -> c) -> f a -> f b -> f c+  liftI2 = liftA2+infixl 6 ^+^, ^-^++instance Additive I+instance (Additive f, Known Nat n) => Additive (VT n f) where+  zero   = vrep zero+  liftU2 = vap . liftU2+  liftI2 = vap . liftI2++class Additive (Diff f) => Affine f where+  type Diff f :: * -> *+  type Diff f = f+  (.-.) :: Num a => f a -> f a -> Diff f a+  (.+^) :: Num a => f a -> Diff f a -> f a+  (.-^) :: Num a => f a -> Diff f a -> f a+  --------+  p .-^ d = p .+^ negated d+  default (.-.) :: (Affine f, Diff f ~ f, Num a) => f a -> f a -> Diff f a+  (.-.) = (^-^)+  default (.+^) :: (Affine f, Diff f ~ f, Num a) => f a -> f a -> Diff f a+  (.+^) = (^+^)+infixl 6 .-., .+^, .-^++instance Affine I+instance (Affine f, Known Nat n) => Affine (VT n f) where+  type Diff (VT n f) = VT n (Diff f)+  (.-.) = vap (.-.)+  (.+^) = vap (.+^)+  (.-^) = vap (.-^)++class Additive f => Metric f where+  dot       :: Num a => f a -> f a -> a+  quadrance :: Num a => f a -> a+  qd        :: Num a => f a -> f a -> a+  distance  :: Floating a => f a -> f a -> a+  norm      :: Floating a => f a -> a+  signorm   :: Floating a => f a -> f a+  --------+  default dot :: (Foldable f, Num a) => f a -> f a -> a+  dot       a b = F.sum $ liftI2 (*) a b+  quadrance     = join dot+  qd        a b = quadrance $ a ^-^ b+  distance  a b = norm $ a ^-^ b+  norm          = sqrt . quadrance+  signorm   a   = (/ norm a) <$> a++instance Metric I where+  dot (I a) (I b) = a * b++instance (Metric f, Known Nat n) => Metric (VT n f) where+  dot a b = getSum $ foldMap Sum $ vap ((I .) . dot) a b++(*^) :: (Functor f, Num a) => a -> f a -> f a+(*^) a = fmap (a*)+infixl 7 *^++negated :: (Functor f, Num a) => f a -> f a+negated = fmap negate++qdA :: (Affine f, Foldable (Diff f), Num a) => f a -> f a -> a+qdA a b = F.sum $ join (*) <$> a .-. b++distanceA :: (Affine f, Foldable (Diff f), Floating a) => f a -> f a -> a+distanceA a b = sqrt $ qdA a b++-- }}}+-}+
+ src/Type/Class/HFunctor.hs view
@@ -0,0 +1,56 @@+{-# 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.Class.HFunctor+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- Higher order functors, foldables, and traversables,+-- along with their indexed variants.+-- (oh, and bifunctors tacked on for good measure.)+----------------------------------------------------------------------------++module Type.Class.HFunctor where++class HFunctor (t :: (k -> *) -> l -> *) where+  -- | Take a natural transformation to a lifted natural transformation.+  map' :: (forall (a :: k). f a -> g a) -> t f b -> t g b++class HIxFunctor (i :: l -> k -> *) (t :: (k -> *) -> l -> *) | t -> i where+  imap' :: (forall (a :: k). i b a -> f a -> g a) -> t f b -> t g b++class HFoldable (t :: (k -> *) -> l -> *) where+  foldMap' :: Monoid m => (forall (a :: k). f a -> m) -> t f b -> m++class HIxFoldable (i :: l -> k -> *) (t :: (k -> *) -> l -> *) | t -> i where+  ifoldMap' :: Monoid m => (forall (a :: k). i b a -> f a -> m) -> t f b -> m++class (HFunctor t, HFoldable t) => HTraversable (t :: (k -> *) -> l -> *) where+  traverse' :: Applicative h => (forall (a :: k). f a -> h (g a)) -> t f b -> h (t g b)++class (HIxFunctor i t, HIxFoldable i t) => HIxTraversable (i :: l -> k -> *) (t :: (k -> *) -> l -> *) | t -> i where+  itraverse' :: Applicative h => (forall (a :: k). i b a -> f a -> h (g a)) -> t f b -> h (t g b)++class HBifunctor (t :: (k -> *) -> (l -> *) -> m -> *) where+  bimap' :: (forall (a :: k). f a -> h a)+         -> (forall (a :: l). g a -> i a)+         -> t f g b+         -> t h i b+
+ src/Type/Class/Known.hs view
@@ -0,0 +1,51 @@+{-# 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.Class.Known+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- The 'Known' class, among others in this library, use an associated+-- 'Constraint' to maintain a bidirectional chain of inference.+--+-- For instance, given evidence of @Known Nat n@, if @n@ later gets refined+-- to @n'@, we can correctly infer @Known Nat n'@, as per the type instance+-- defined for @KnownC Nat (S n')@.+----------------------------------------------------------------------------++module Type.Class.Known where++import Type.Family.Constraint++import Data.Type.Equality++-- | Each instance of 'Known' provides a canonical construction+-- of a type at a particular index.+--+-- Useful for working with singleton-esque GADTs.+class KnownC f a => Known (f :: k -> *) (a :: k) where+  type KnownC f a :: Constraint+  type KnownC (f :: k -> *) (a :: k) = ØC+  known :: f a++instance (a ~ b) => Known ((:~:) a) b where+  type KnownC ((:~:) a) b = (a ~ b)+  known = Refl+
+ src/Type/Class/Witness.hs view
@@ -0,0 +1,208 @@+{-# LANGUAGE FlexibleContexts #-}+{-# 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.Class.Witness+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- A type @t@ that is a @'Witness' p q t@ provides a 'Constraint' entailment+-- of @q@, given that @p@ holds.+--+-- The 'Witness' class uses an associated 'Constraint' @WitnessC@ to+-- maintain backwards inference of 'Witness' instances with respect+-- to type refinement. See the 'Known' class for more information.+--+-- Heavily inspired by ekmett's constraints library:+-- <http://hackage.haskell.org/package/constraints>+--+-- The code provided here does not /quite/ subsume the @constraints@+-- library, as we do not give classes and instances for representing+-- the standard library's class heirarchy and instance definitions.+----------------------------------------------------------------------------++module Type.Class.Witness+  ( module Type.Class.Witness+  , module Exports+  ) where++import Type.Class.Known+import Type.Family.Constraint++import Data.Type.Equality as Exports+import Data.Void          as Exports++import Prelude hiding (id,(.))+import Control.Category+import Unsafe.Coerce++-- | A reified 'Constraint'.+data Wit :: Constraint -> * where+  Wit :: c => Wit c++data Wit1 :: (k -> Constraint) -> k -> * where+  Wit1 :: c a => Wit1 c a++-- | Reified evidence of 'Constraint' entailment.+--+-- Given a term of @p :- q@, the Constraint @q@ holds+-- if @p@ holds.+--+-- Entailment of 'Constraint's form a 'Category':+--+-- >>> id  :: p :- p+-- >>> (.) :: (q :- r) -> (p :-> q) -> (p :- r)+data (:-) :: Constraint -> Constraint -> * where+  Sub :: { getSub :: p => Wit q } -> p :- q+infixr 4 :-++instance Category (:-) where+  id              = Sub Wit+  Sub bc . Sub ab = Sub $ bc \\ ab++-- | A general eliminator for entailment.+--+-- Given a term of type @t@ with an instance @Witness p q t@+-- and a term of type @r@ that depends on 'Constraint' @q@,+-- we can reduce the Constraint to @p@.+--+-- If @p@ is @ØC@, i.e. the empty 'Constraint' @()@, then+-- a Witness @t@ can completely discharge the Constraint @q@.+class WitnessC p q t => Witness (p :: Constraint) (q :: Constraint) (t :: *) | t -> p q where+  type WitnessC p q t :: Constraint+  type WitnessC p q t = ØC+  (\\) :: p => (q => r) -> t -> r+infixl 1 \\++-- | Convert a 'Witness' to a canonical reified entailment.+entailed :: Witness p q t => t -> p :- q+entailed t = Sub (Wit \\ t)++-- | Convert a 'Witness' to a canonical reified 'Constraint'.+witnessed :: Witness ØC q t => t -> Wit q+witnessed t = Wit \\ t++instance Witness ØC c (Wit c) where+  r \\ Wit = r++-- | An entailment @p :- q@ is a Witness of @q@, given @p@.+instance Witness p q (p :- q) where+  r \\ Sub Wit = r++-- | A type equality @a ':~:' b@ is a Witness that @(a ~ b)@.+instance Witness ØC (a ~ b) (a :~: b) where+  r \\ Refl = r++-- | If the constraint @c@ holds, there is a canonical construction+-- for a term of type @'Wit' c@, viz. the constructor @Wit@.+instance c => Known Wit c where+  type KnownC Wit c = c+  known = Wit++-- | Constraint chaining under @Maybe@.+(/?) :: (Witness p q t, p) => Maybe t -> (q => Maybe r) -> Maybe r+(/?) = \case+  Just t -> (\\ t)+  _      -> \_ -> Nothing+infixr 0 /?++qed :: Maybe (a :~: a)+qed = Just Refl++impossible :: a -> Void+impossible = unsafeCoerce++data Dec a+  = Proven   a+  | Refuted (a -> Void)++class DecEquality (f :: k -> *) where+  decideEquality :: f a -> f b -> Dec (a :~: b)++decCase :: Dec a+  -> (a -> r)+  -> ((a -> Void) -> r)+  -> r+decCase d y n = case d of+  Proven  a -> y a+  Refuted b -> n b++data Bij p a b = Bij+  { fwd :: p a b+  , bwd :: p b a+  }++($->) :: Bij p a b -> p a b+($->) = fwd+(<-$) :: Bij p a b -> p b a+(<-$) = bwd+infixr 1 $->, <-$++instance Category p => Category (Bij p) where+  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+  (.*.) :: c v w -> c x y -> c (Tensor c v x) (Tensor c w y)+  assoc  :: c (Tensor c (Tensor c x y) z) (Tensor c x (Tensor c y z))+  unitL  :: c (Tensor c (Unit c) x) x+  unitR  :: c (Tensor c x (Unit c)) x+infixr 3 .*.++class Category c => Symmetric (c :: k -> k -> *) where+  symm :: c a b -> c b a++instance Category p => Symmetric (Bij p) where+  symm p = bwd p <-> fwd p++instance Monoidal (->) where+  type Tensor (->) = (,)+  type Unit   (->) = ()+  (f .*. g) (a,b) = (f a,g b)+  assoc ((x,y),z) = (x,(y,z))+  unitL (_,x) = x+  unitR (x,_) = x++instance (Symmetric p, Monoidal p) => Monoidal (Bij p) where+  type Tensor (Bij p) = Tensor p+  type Unit   (Bij p) = Unit p+  (.*.) = (***)+  assoc = assoc <-> symm assoc+  unitL = unitL <-> symm unitL+  unitR = unitR <-> symm unitR++(***) :: 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 <->++(<->) :: p a b -> p b a -> Bij p a b+(<->) = Bij++(<?>) :: r <-> s -> Dec r -> Dec s+(<?>) p = \case+  Proven  a -> Proven  $ p $-> a+  Refuted f -> Refuted $ \a -> f $ p <-$ a+infix 3 <?>+
+ src/Type/Family/Constraint.hs view
@@ -0,0 +1,45 @@+{-# 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.Constraint+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- Reexports the kind 'GHC.Exts.Constraint', as well as some+-- conveniences for working with 'Constraint's.+----------------------------------------------------------------------------++module Type.Family.Constraint+  ( module Type.Family.Constraint+  , Constraint+  ) where++import GHC.Exts (Constraint)++-- | The empty 'Constraint'.+type ØC = (() :: Constraint)++class IffC b t f => Iff (b :: Bool) (t :: Constraint) (f :: Constraint) where+  type IffC b t f :: Constraint+instance t => Iff True  t f where+  type IffC True  t f = t+instance f => Iff False t f where+  type IffC False t f = f+
+ src/Type/Family/List.hs view
@@ -0,0 +1,99 @@+{-# 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.List+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- Convenient aliases and type families for working with+-- type-level lists.+----------------------------------------------------------------------------++module Type.Family.List+  ( module Type.Family.List+  , (==)+  ) where++import Type.Family.Constraint+import Type.Family.Monoid++import Data.Type.Bool+import Data.Type.Equality++type Ø    = '[]+type (:<) = '(:)+infixr 5 :<++-- | Type-level singleton list.+type Only a = '[a]++-- | Appends two type-level lists.+type family (as :: [k]) ++ (bs :: [k]) :: [k] where+  Ø         ++ bs = bs+  (a :< as) ++ bs = a :< (as ++ bs)+infixr 5 ++++-- | Type-level list snoc.+type family (as :: [k]) >: (a :: k) :: [k] where+  Ø         >: a = Only a+  (b :< as) >: a = b :< (as >: a)+infixl 6 >:++type family Reverse (as :: [k]) :: [k] where+  Reverse  Ø        = Ø+  Reverse (a :< as) = Reverse as >: a++type family Init' (a :: k) (as :: [k]) :: [k] where+  Init' a Ø = Ø+  Init' a (b :< as) = a :< Init' b as++type family Last' (a :: k) (as :: [k]) :: k where+  Last' a Ø         = a+  Last' a (b :< as) = Last' b as++-- | Takes a type-level list of 'Constraint's to a single+-- 'Constraint', where @ListC cs@ holds iff all elements+-- of @cs@ hold.+type family ListC (cs :: [Constraint]) :: Constraint where+  ListC  Ø        = ØC+  ListC (c :< cs) = (c, ListC cs)++-- | Map an @(f :: k -> l)@ over a type-level list @(as :: [k])@,+-- giving a list @(bs :: [l])@.+type family (f :: k -> l) <$> (a :: [k]) :: [l] where+  f <$> Ø         = Ø+  f <$> (a :< as) = f a :< (f <$> as)+infixr 4 <$>++-- | Map a list of @(fs :: [k -> l])@ over a single @(a :: k)@,+-- giving a list @(bs :: [l])@.+type family (f :: [k -> l]) <&> (a :: k) :: [l] where+  Ø         <&> a = Ø+  (f :< fs) <&> a = f a :< (fs <&> a)+infixl 5 <&>++type family (f :: [k -> l]) <*> (a :: [k]) :: [l] where+  fs <*> Ø         = Ø+  fs <*> (a :< as) = (fs <&> a) ++ (fs <*> as)+infixr 4 <*>++type instance Mempty = Ø+type instance a <> b = a ++ b+
+ src/Type/Family/Maybe.hs view
@@ -0,0 +1,71 @@+{-# 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.Maybe+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- Convenient type families for working with type-level @Maybe@s.+----------------------------------------------------------------------------++module Type.Family.Maybe+  ( module Type.Family.Maybe+  , type (==)+  ) where++import Type.Family.Constraint+import Type.Family.Monoid++import Data.Type.Equality++-- | Take a @Maybe Constraint@ to a @Constraint@.+type family MaybeC (mc :: Maybe Constraint) :: Constraint where+  MaybeC Nothing  = ØC+  MaybeC (Just c) = c++-- | Map over a type-level @Maybe@.+type family (f :: k -> l) <$> (a :: Maybe k) :: Maybe l where+  f <$> Nothing = Nothing+  f <$> Just a  = Just (f a)+infixr 4 <$>++type family (f :: Maybe (k -> l)) <&> (a :: k) :: Maybe l where+  Nothing <&> a = Nothing+  Just f  <&> a = Just (f a)+infixl 5 <&>++type family (f :: Maybe (k -> l)) <*> (a :: Maybe k) :: Maybe l where+  Nothing <*> a       = Nothing+  f       <*> Nothing = Nothing+  Just f  <*> Just a  = Just (f a)+infixr 4 <*>++type family (a :: Maybe k) <|> (b :: Maybe k) :: Maybe k where+  Nothing <|> a       = a+  a       <|> Nothing = a+  Just a  <|> Just b  = Just a+infixr 4 <|>++type family FromJust (m :: Maybe k) :: k where+  FromJust (Just a) = a++type instance Mempty = Nothing+type instance a <> b = a <|> b+
+ src/Type/Family/Monoid.hs view
@@ -0,0 +1,23 @@+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Type.Family.Monoid+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- Type-level @Monoid@, defined as an open type family.+--+-----------------------------------------------------------------------------++module Type.Family.Monoid where++type family Mempty :: k+type family (a :: k) <> (b :: k) :: k+
+ src/Type/Family/Nat.hs view
@@ -0,0 +1,84 @@+{-# 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.Nat+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- Type-level natural numbers, along with frequently used+-- type families over them.+--+-----------------------------------------------------------------------------++module Type.Family.Nat+  ( module Type.Family.Nat+  , type (==)+  ) where++import Data.Type.Equality+import Type.Family.List++data N+  = Z+  | S N+  deriving (Eq,Ord,Show)++type family NatEq (x :: N) (y :: N) :: Bool where+  NatEq  Z     Z    = True+  NatEq  Z    (S y) = False+  NatEq (S x)  Z    = False+  NatEq (S x) (S y) = NatEq x y+type instance x == y = NatEq x y++type family Iota (x :: N) :: [N] where+  Iota Z     = Ø+  Iota (S x) = x :< Iota x++type family Pred (x :: N) :: N where+  Pred (S n) = n++type family (x :: N) + (y :: N) :: N where+  Z   + y = y+  S x + y = S (x + y)+infixr 6 +++type family (x :: N) * (y :: N) :: N where+  Z   * y = Z+  S x * y = (x * y) + y+infixr 7 *++type family (x :: N) ^ (y :: N) :: N where+  x ^   Z = S Z+  x ^ S y = (x ^ y) * x+infixl 8 ^++-- | Convenient aliases for low-value Peano numbers.+type N0  = Z+type N1  = S N0+type N2  = S N1+type N3  = S N2+type N4  = S N3+type N5  = S N4+type N6  = S N5+type N7  = S N6+type N8  = S N7+type N9  = S N8+type N10 = S N9+
+ src/Type/Family/Pair.hs view
@@ -0,0 +1,58 @@+{-# 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)+
+ type-combinators.cabal view
@@ -0,0 +1,50 @@+name: type-combinators+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+version: 0.1.0.0+cabal-version: >=1.10+build-type: Simple+license: BSD3+license-file: LICENSE+maintainer: kylcarte@gmail.com+author: Kyle Carter++source-repository head+    type: git+    location: git://github.com/kylcarte/type-combinators.git++library+    exposed-modules:+        Data.Type.Combinator+        Data.Type.Conjunction+        Data.Type.Disjunction+        Data.Type.Fin+        Data.Type.Index+        Data.Type.Length+        Data.Type.Nat+        Data.Type.Option+        Data.Type.Product+        Data.Type.Quantifier+        Data.Type.Sum+        Data.Type.Vector+        Type.Class.HFunctor+        Type.Class.Known+        Type.Class.Witness+        Type.Family.Constraint+        Type.Family.List+        Type.Family.Maybe+        Type.Family.Monoid+        Type.Family.Nat+        Type.Family.Pair+    build-depends:+        base >=4.8 && <4.9+    default-language: Haskell2010+    hs-source-dirs: src+