packages feed

type-combinators 0.2.2.0 → 0.2.2.1

raw patch · 12 files changed

+274/−34 lines, 12 files

Files

src/Data/Type/Boolean.hs view
@@ -30,9 +30,9 @@  import Data.Type.Quantifier (Some(..)) import Type.Family.Bool-import Type.Family.Constraint import Type.Class.Known import Type.Class.Higher+import Type.Class.Witness  data Boolean :: Bool -> * where   False_ :: Boolean False@@ -55,53 +55,62 @@     | ("False_",s1) <- lex s0     ] +if' :: Boolean b -> ((b ~ True) => a) -> ((b ~ False) => a) -> a+if' t c a = case t of+  True_  -> c+  False_ -> a++(.?) :: ((b ~ True) => a) -> ((b ~ False) => a) -> Boolean b -> a+(c .? a) t = if' t c a+infix 4 .?+ not' :: Boolean a -> Boolean (Not a)-not' = \case-  False_ -> True_-  True_  -> False_+not' = False_ .? True_  (.||) :: Boolean a -> Boolean b -> Boolean (a || b)-(.||) = \case-  False_ -> id-  True_  -> const True_+(.||) = (True_ .? True_ )+     .? (True_ .? False_) infixr 2 .||  (.&&) :: Boolean a -> Boolean b -> Boolean (a && b)-(.&&) = \case-  False_ -> const False_-  True_  -> id+(.&&) = (True_  .? False_)+     .? (False_ .? False_) infixr 3 .&&  (.^^) :: Boolean a -> Boolean b -> Boolean (a ^^ b)-a .^^ b = (a .|| b) .&& not' (a .&& b)+(.^^) = (False_ .? True_ )+     .? (True_  .? False_) infixr 4 .^^  (==>) :: Boolean a -> Boolean b -> Boolean (a ==> b)-a ==> b = not' a .|| b+(==>) = (True_ .? False_)+     .? (True_ .? True_ ) infixr 1 ==>  (<==>) :: Boolean a -> Boolean b -> Boolean (a <==> b)-(<==>) = (.==)+(<==>) = (True_  .? False_)+      .? (False_ .? True_ ) infixr 1 <==>  class BoolEquality (f :: k -> *) where-  type BoolEqC f (a :: k) (b :: k) :: Constraint-  type BoolEqC f a b = ØC-  (.==) :: BoolEqC f a b => f a -> f b -> Boolean (a == b)+  boolEquality :: f a -> f b -> Boolean (a == b)++(.==) :: BoolEquality f => f a -> f b -> Boolean (a == b)+(.==) = boolEquality infix 4 .==  instance BoolEquality Boolean where-  (.==) = \case-    False_ -> \case-      False_ -> True_-      True_  -> False_-    True_  -> \case-      False_ -> False_-      True_  -> True_+  boolEquality = (<==>) +instance TestEquality Boolean where+  testEquality = (qed .? Nothing) .? (Nothing .? qed)+ instance Known Boolean True where   known = True_  instance Known Boolean False where   known = False_++toBool :: Boolean b -> Bool+toBool = True .? False
src/Data/Type/Combinator.hs view
@@ -36,12 +36,24 @@ module Data.Type.Combinator where  import Data.Type.Quantifier+import Data.Type.Index.Trans import Type.Class.Higher import Type.Class.Known import Type.Class.Witness import Type.Family.Tuple  import Control.Applicative++data Comp1 (f :: l -> m -> *) (g :: k -> l) :: k -> m -> * where+  Comp1 :: { getComp1 :: !(f (g h) a)+           }+        -> Comp1 f g h a++instance (Functor1 f, Functor1 g) => Functor1 (Comp1 (f :: (l -> *) -> m -> *) (g :: (k -> *) -> l -> *)) where+  map1 f (Comp1 a) = Comp1 $ map1 (map1 f) a++instance (IxFunctor1 i f, IxFunctor1 j g) => IxFunctor1 (IxComp i j) (Comp1 (f :: (l -> *) -> m -> *) (g :: (k -> *) -> l -> *)) where+  imap1 f = Comp1 . imap1 (\i -> imap1 $ \j -> f $ IxComp i j) . getComp1  -- (:.:) {{{
src/Data/Type/Conjunction.hs view
@@ -32,17 +32,17 @@  module Data.Type.Conjunction where +import Data.Type.Index.Trans import Type.Class.Higher import Type.Class.Known import Type.Class.Witness import Type.Family.Tuple-import Data.Type.Boolean  -- (:&:) {{{  data ((f :: k -> *) :&: (g :: k -> *)) :: k -> * where   (:&:) :: !(f a) -> !(g a) -> (f :&: g) a-infixr 5 :&:+infixr 6 :&:  deriving instance (Eq   (f a), Eq   (g a)) => Eq   ((f :&: g) a) deriving instance (Ord  (f a), Ord  (g a)) => Ord  ((f :&: g) a)@@ -105,7 +105,7 @@  data ((f :: k -> *) :*: (g :: l -> *)) :: (k,l) -> * where   (:*:) :: !(f a) -> !(g b) -> (f :*: g) (a#b)-infixr 5 :*:+infixr 6 :*:  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)@@ -150,6 +150,11 @@  instance Bifunctor1 (:*:) where   bimap1 f g (a :*: b) = f a :*: g b++instance IxFunctor1 (IxSecond (:~:)) ((:*:) f) where+  imap1 f (a :*: b) = a :*: f (IxSecond Refl) b++-- f :: (k -> *) ==> ((:*:) f) :: (l -> *) -> (k,l) -> *  _fst :: (a#b) :~: (c#d) -> a :~: c _fst Refl = Refl
+ src/Data/Type/Index/Trans.hs view
@@ -0,0 +1,59 @@+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE LambdaCase #-}++module Data.Type.Index.Trans+  ( module Data.Type.Index.Trans+  , (:~:)(..)+  ) where++import Data.Type.Index+import Type.Class.Witness ((:~:)(..))+import Type.Family.List++ixList :: Index a b -> i b c -> IxList i a c+ixList = \case+  IZ   -> IxHead+  IS x -> IxTail . ixList x++data IxList (i :: k -> l -> *) :: [k] -> l -> * where+  IxHead :: !(i a b)+         -> IxList i (a :< as) b+  IxTail :: !(IxList i as b)+         -> IxList i (a :< as) b++data IxFirst (i :: k -> l -> *) :: (k,m) -> l -> * where+  IxFirst :: !(i a b)+          -> IxFirst i '(a,c) b++data IxSecond (i :: k -> l -> *) :: (m,k) -> l -> * where+  IxSecond :: !(i a b)+           -> IxSecond i '(c,a) b++data IxOr (i :: k -> m -> *) (j :: l -> m -> *) :: Either k l -> m -> * where+  IxOrL :: !(i a b)+        -> IxOr i j (Left a) b+  IxOrR :: !(j a b)+        -> IxOr i j (Right a) b++data IxJust (i :: k -> l -> *) :: Maybe k -> l -> * where+  IxJust :: !(i a b)+         -> IxJust i (Just a) b++data IxComp (i :: k -> l -> *) (j :: l -> m -> *) :: k -> m -> * where+  IxComp :: !(i a b)+         -> !(j b c)+         -> IxComp i j a c+
src/Data/Type/Nat.hs view
@@ -87,7 +87,7 @@       S_ y -> testEquality x y //? qed  instance BoolEquality Nat where-  (.==) = \case+  boolEquality = \case     Z_ -> \case       Z_   -> True_       S_ _ -> False_
src/Data/Type/Option.hs view
@@ -38,6 +38,13 @@   Nothing_ :: Option f Nothing   Just_    :: !(f a) -> Option f (Just a) +deriving instance MaybeC (Eq   <$> f <$> m) => Eq   (Option f m)+deriving instance+  ( MaybeC (Eq   <$> f <$> m)+  , MaybeC (Ord  <$> f <$> m)+  ) => Ord (Option f m)+deriving instance MaybeC (Show <$> f <$> m) => Show (Option f m)+ -- | Eliminator for @'Option' f@. option :: (forall a. (m ~ Just a) => f a -> r) -> ((m ~ Nothing) => r) -> Option f m -> r option j n = \case
src/Data/Type/Product.hs view
@@ -31,7 +31,7 @@ -- -- '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+-- Oleg Kiselyov's 'HList', from <http://hackage.haskell.org/package/HList>, and --  -- Kenneth Foner's 'ConicList', from <http://hackage.haskell.org/package/IndexedList-0.1.0.1/docs/Data-List-Indexed-Conic.html>. --@@ -39,6 +39,7 @@  module Data.Type.Product where +import Data.Type.Boolean import Data.Type.Combinator import Data.Type.Conjunction import Data.Type.Index@@ -100,6 +101,19 @@       ]     ) s0 +instance BoolEquality f => BoolEquality (Prod f) where+  boolEquality = \case+    Ø -> \case+      Ø      -> True_+      (:<){} -> False_+    a :< as -> \case+      b :< bs -> case a .== b of+        True_  -> case as .== bs of+          True_  -> True_+          False_ -> False_+        False_ -> False_+      Ø -> False_+ instance TestEquality f => TestEquality (Prod f) where   testEquality = \case     Ø -> \case@@ -162,10 +176,12 @@   Ø       -> id   a :< as -> (a :<) . append' as +{- lookup' :: TestEquality f => f a -> Prod (f :&: g) as -> Maybe (g a) lookup' a = \case   Ø               -> Nothing   (b :&: v) :< bs -> witMaybe (a =?= b) (Just v) $ lookup' a bs+-}  lookupPar :: TestEquality f => f a -> Prod (f :*: g) as -> Maybe (Some g) lookupPar a = \case@@ -273,4 +289,9 @@ instance (Witness p q (f a), Witness s t (Prod f as)) => Witness (p,s) (q,t) (Prod f (a :< as)) where   type WitnessC (p,s) (q,t) (Prod f (a :< as)) = (Witness p q (f a), Witness s t (Prod f as))   r \\ (a :< as) = r \\ a \\ as++toList :: (forall a. f a -> r) -> Prod f as -> [r]+toList f = \case+  Ø       -> []+  a :< as -> f a : toList f as
+ src/Data/Type/Product/Env.hs view
@@ -0,0 +1,113 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE LambdaCase #-}++module Data.Type.Product.Env where++import Data.Type.Combinator (Comp1(..))+import Data.Type.Conjunction+import Data.Type.Boolean+import Data.Type.Index+import Data.Type.Index.Trans+import Data.Type.Option+import Data.Type.Product+import Type.Class.Higher+import Type.Class.Witness+import Type.Family.Bool+import Type.Family.List++newtype Env k v ps = Env+  { getEnv :: Prod (k :*: v) ps+  }++type family Member (x :: k) (ps :: [(k,v)]) :: Bool where+  Member x Ø              = False+  Member x ('(y,a) :< ps) = (x == y) || Member x ps++member' :: BoolEquality k => k x -> Env k v ps -> Boolean (Member x ps)+member' x = (. getEnv) $ \case+  Ø               -> False_+  (y :*: _) :< ps -> (x .== y) .|| member' x (Env ps)++type family Lookup (x :: k) (ps :: [(k,v)]) :: Maybe v where+  Lookup x Ø              = Nothing+  Lookup x ('(y,a) :< ps) = If (x == y) (Just a) (Lookup x ps)++lookup' :: BoolEquality k => k x -> Env k v ps -> Option v (Lookup x ps)+lookup' x = (. getEnv) $ \case+  Ø              -> Nothing_+  (y :*: a) :< ps -> if' (x .== y)+    (Just_ a)+    (lookup' x $ Env ps)++type family Insert (x :: k) (a :: v) (ps :: [(k,v)]) :: [(k,v)] where+  Insert x a Ø              = '[ '(x,a) ]+  Insert x a ('(y,b) :< ps) = If (x == y) ('(x,a) :< ps) ('(y,b) :< Insert x a ps)++insert' :: BoolEquality k => k x -> v a -> Env k v ps -> Env k v (Insert x a ps)+insert' x a = (. getEnv) $ \case+  Ø               -> Env $ (x :*: a) :< Ø+  (y :*: b) :< ps -> if' (x .== y)+    (Env $ (x :*: a) :< ps)+    (Env $ (y :*: b) :< getEnv (insert' x a (Env ps)))++type family Delete (x :: k) (ps :: [(k,v)]) :: [(k,v)] where+  Delete x Ø              = Ø+  Delete x ('(y,a) :< ps) = If (x == y) ps ('(y,a) :< Delete x ps)++delete' :: BoolEquality k => k x -> Env k v ps -> Env k v (Delete x ps)+delete' x = (. getEnv) $ \case+  Ø               -> Env Ø+  (y :*: a) :< ps -> if' (x .== y)+    (Env ps)+    (Env $ (y :*: a) :< getEnv (delete' x (Env ps)))++type family Difference (ps :: [(k,v)]) (qs :: [(k,w)]) :: [(k,v)] where+  Difference ps Ø              = ps+  Difference ps ('(x,a) :< qs) = Delete x (Difference ps qs)++difference' :: BoolEquality k => Env k v ps -> Env k w qs -> Env k v (Difference ps qs)+difference' ps = (. getEnv) $ \case+  Ø               -> ps+  (x :*: _) :< qs -> delete' x $ difference' ps (Env qs)++(.\\) :: BoolEquality k => Env k v ps -> Env k w qs -> Env k v (Difference ps qs)+(.\\) = difference'++type family Union (ps :: [(k,v)]) (qs :: [(k,v)]) :: [(k,v)] where+  Union ps Ø              = ps+  Union ps ('(x,a) :< qs) = Insert x a (Union ps qs)++union' :: BoolEquality k => Env k v ps -> Env k v qs -> Env k v (Union ps qs)+union' ps = (. getEnv) $ \case+  Ø               -> ps+  (x :*: a) :< qs -> insert' x a $ union' ps (Env qs)++type family Intersection (ps :: [(k,v)]) (qs :: [(k,w)]) :: [(k,v)] where+  Intersection Ø              qs = Ø+  Intersection ('(x,a) :< ps) qs = If (Member x qs) ('(x,a) :< Intersection ps qs) (Intersection ps qs)++intersection' :: BoolEquality k => Env k v ps -> Env k w qs -> Env k v (Intersection ps qs)+intersection' ps qs = case getEnv ps of+  Ø                -> Env Ø+  (x :*: a) :< ps' -> if' (member' x qs) (Env $ (x :*: a) :< getEnv rest) rest+    where+    rest = intersection' (Env ps') qs++instance Functor1 (Env k) where+  map1 f = Env . getComp1 . map1 f . Comp1 . getEnv++instance IxFunctor1 (IxList (IxSecond (:~:))) (Env k) where+  imap1 f = Env . imap1 (\i -> imap1 $ \j -> f $ ixList i j) . getEnv+
src/Data/Type/Sym.hs view
@@ -55,10 +55,6 @@ instance TestEquality Sym where   testEquality Sym Sym = sameSymbol Proxy Proxy -instance BoolEquality Sym where-  type BoolEqC Sym a b = Known Boolean (a == b)-  Sym .== Sym = known- instance KnownSymbol x => Known Sym x where   type KnownC Sym x = KnownSymbol x   known = Sym
src/Type/Family/Bool.hs view
@@ -32,7 +32,7 @@  import Type.Family.Constraint import Type.Class.Witness as Exports (type (==))-import Data.Type.Bool as Exports (type Not, type (||), type (&&))+import Data.Type.Bool as Exports (type If, type Not, type (||), type (&&))  type family BoolC (b :: Bool) :: Constraint where   BoolC True  = ØC
src/Type/Family/List.hs view
@@ -92,12 +92,24 @@  -- Head,Tail,Init,Last {{{ +type family HeadM (as :: [k]) :: Maybe k where+  HeadM Ø         = Nothing+  HeadM (a :< as) = Just a+ type family Head (as :: [k]) :: k where   Head (a :< as) = a +type family TailM (as :: [k]) :: Maybe [k] where+  TailM Ø         = Nothing+  TailM (a :< as) = Just as+ type family Tail (as :: [k]) :: [k] where   Tail (a :< as) = as +type family InitM (as :: [k]) :: Maybe [k] where+  InitM Ø         = Nothing+  InitM (a :< as) = Just (Init' a as)+ type family Init (as :: [k]) :: [k] where   Init (a :< as) = Init' a as @@ -107,6 +119,10 @@  initCong :: (a ~ b,as ~ bs) :- (Init' a as ~ Init' b bs) initCong = Sub Wit++type family LastM (as :: [k]) :: Maybe k where+  LastM Ø         = Nothing+  LastM (a :< as) = Just (Last' a as)  type family Last (as :: [k]) :: k where   Last (a :< as) = Last' a as
type-combinators.cabal view
@@ -1,5 +1,5 @@ name: type-combinators-version: 0.2.2.0+version: 0.2.2.1 category: Data synopsis: A collection of data types for type-level programming cabal-version: >=1.10@@ -24,11 +24,13 @@         Data.Type.Fin         Data.Type.Fin.Indexed         Data.Type.Index+        Data.Type.Index.Trans         Data.Type.Length         Data.Type.Nat         Data.Type.Nat.Inequality         Data.Type.Option         Data.Type.Product+        Data.Type.Product.Env         Data.Type.Product.Lifted         Data.Type.Sum         Data.Type.Sum.Lifted