packages feed

type-combinators 0.2.2.1 → 0.2.4.0

raw patch · 31 files changed

+826/−390 lines, 31 filesdep ~base

Dependency ranges changed: base

Files

src/Data/Type/Boolean.hs view
@@ -1,9 +1,9 @@+{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE LambdaCase #-}@@ -28,7 +28,7 @@  module Data.Type.Boolean where -import Data.Type.Quantifier (Some(..))+-- import Data.Type.Quantifier (Some(..)) import Type.Family.Bool import Type.Class.Known import Type.Class.Higher
src/Data/Type/Combinator.hs view
@@ -35,8 +35,7 @@  module Data.Type.Combinator where -import Data.Type.Quantifier-import Data.Type.Index.Trans+-- import Data.Type.Quantifier import Type.Class.Higher import Type.Class.Known import Type.Class.Witness@@ -52,8 +51,10 @@ 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+-}  -- (:.:) {{{ @@ -322,4 +323,23 @@ mapJoin f = Join . f . getJoin  -- }}}++data Conj (t :: (k -> *) -> l -> *) (f :: k -> m -> *) :: l -> m -> * where+  Conj :: t (Flip f b) a+       -> Conj t f a b++{-+data Conj2 (t :: (k -> l -> *) -> m -> n -> *) (f :: k -> l -> o -> *) :: m -> n -> o -> * where+  Conj2 :: t +       -> Conj2 t f a b c+-}++data LL (c :: k -> *) :: l -> (l -> k) -> * where+  LL :: { getLL :: c (f a)+        }+     -> LL c a f++data RR (c :: k -> *) :: (l -> k) -> l -> * where+  RR :: { getRR :: c (f a) }+     -> RR c f a
+ src/Data/Type/Difference.hs view
@@ -0,0 +1,156 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE GADTs #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Type.Difference+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- A @singleton@-esque type for representing the removal of a subset of a type level list.+--+-----------------------------------------------------------------------------++module Data.Type.Difference where++-- import Data.Type.Quantifier+import Type.Class.Known+import Type.Class.Witness+import Type.Family.Constraint+import Type.Family.List+import Data.Type.Length+import Data.Type.Subset+import Data.Type.Remove+import Data.Type.Sum+import Control.Arrow (first,left)++data Difference :: [k] -> [k] -> [k] -> * where+  ØD   :: Difference as Ø as+  (:-) :: !(Remove bs a cs)+       -> !(Difference cs as ds)+       -> Difference bs (a :< as) ds+infixr 5 :-++diffLen :: Difference as bs cs -> Length bs+diffLen = \case+  ØD     -> LZ+  _ :- d -> LS $ diffLen d++{-+deriving instance Eq   (Difference as bs cs)+deriving instance Ord  (Difference as bs cs)+deriving instance Show (Difference as bs cs)++instance Eq1   (Difference as bs)+instance Ord1  (Difference as bs)+instance Show1 (Difference as bs)++instance Eq2   (Difference as)+instance Ord2  (Difference as)+instance Show2 (Difference as)++instance Eq3   Difference+instance Ord3  Difference+instance Show3 Difference+-}++{-+instance Read3 Remove where+  readsPrec3 d = readParen (d > 10) $ \s0 ->+    [ (Some3 RZ,s1)+    | ("RZ",s1) <- lex s0+    ] +++    [ (i >>--- Some3 . RS,s2)+    | ("RS",s1) <- lex s0+    , (i,s2)    <- readsPrec3 11 s1+    ]+-}++instance TestEquality (Difference as bs) where+  testEquality = \case+    ØD -> \case+      ØD -> qed+    r1 :- d1 -> \case+      r2 :- d2 -> r1 =?= r2 //? d1 =?= d2 //? qed++elimDifference :: (forall xs. p xs Ø xs)+               -> (forall x ws xs ys zs. Remove xs x ys -> Difference ys ws zs -> p ys ws zs -> p xs (x :< ws) zs)+               -> Difference as bs cs+               -> p as bs cs+elimDifference n c = \case+  ØD     -> n+  r :- d -> c r d $ elimDifference n c d++{-+diffSub :: Known Length as => Difference as bs cs -> Subset as bs+diffSub = \case+  ØD     -> Ø+  (r :: Remove as a ds) :- (d :: Difference ds es cs) -> x :< s+    where+    x :: Index as a+    x = remIx r+    s :: Subset as es+    s = subTrans s2 s1+    s1 :: Subset ds es+    s1 = diffSub d+    s2 :: Subset as ds+    s2 = remSub l r+    l :: Length ds+    l = _+-}++{-+subDiff :: Subset as bs -> Some (Difference as bs)+subDiff = \case+  Ø      -> Some ØD+  x :< s -> ixRem x >>- \r -> subDiff s >>- \d -> Some $ r :- _ d+-}++diffProd :: Difference as bs cs -> Prod f as -> (Prod f bs,Prod f cs)+diffProd = \case+  ØD     -> (,) Ø+  r :- d -> \as -> let+    (a,as') = remProd r as+    in first (a :<) $ diffProd d as'++diffSum :: Difference as bs cs -> Sum f as -> Either (Sum f bs) (Sum f cs)+diffSum = \case+  ØD     -> Right+  r :- d -> \as -> case remSum r as of+    Left  a  -> Left $ InL a+    Right bs -> left InR $ diffSum d bs++class WithoutAll (as :: [k]) (bs :: [k]) (cs :: [k]) | as bs -> cs where+  withoutAll :: Difference as bs cs++instance (cs ~ as) => WithoutAll as Ø cs where+  withoutAll = ØD++instance (Without as b cs, WithoutAll cs bs ds) => WithoutAll as (b :< bs) ds where+  withoutAll = without :- withoutAll++instance Witness ØC (WithoutAll as bs cs) (Difference as bs cs) where+  (\\) r = \case+    ØD     -> r+    x :- d -> r \\ x \\ d++instance WithoutAll as bs cs => Known (Difference as bs) cs where+  type KnownC (Difference as bs) cs = WithoutAll as bs cs+  known = withoutAll+
src/Data/Type/Disjunction.hs view
@@ -32,7 +32,7 @@  module Data.Type.Disjunction where -import Data.Type.Quantifier+-- import Data.Type.Quantifier import Type.Class.Higher import Type.Class.Known import Type.Class.Witness@@ -135,19 +135,15 @@   eq1 = \case     L' a -> \case       L' b -> a =#= b-      _    -> False     R' a -> \case       R' b -> a =#= b-      _    -> False  instance (Ord1 f, Ord1 g) => Ord1 (f :+: g) where   compare1 = \case     L' a -> \case       L' b -> compare1 a b-      _    -> LT     R' a -> \case       R' b -> compare1 a b-      _    -> GT  instance (Show1 f, Show1 g) => Show1 (f :+: g) where   showsPrec1 d = showParen (d > 10) . \case
src/Data/Type/Fin.hs view
@@ -32,10 +32,11 @@  import Data.Type.Nat import Type.Class.Higher+import Type.Class.Known import Type.Class.Witness import Type.Family.Constraint import Type.Family.Nat-import Data.Type.Quantifier+-- import Data.Type.Quantifier  data Fin :: N -> * where   FZ :: Fin (S n)@@ -58,6 +59,20 @@     | ("FS",s1) <- lex s0     , (n,s2)    <- readsPrec1 11 s1     ]++instance (Known Nat n, Pos n) => Enum (Fin n) where+  toEnum n+    | n <= 0 = FZ+    | otherwise = case (known :: Nat n) of+      S_ Z_   -> FZ+      S_ S_{} -> FS $ toEnum (n-1)+  fromEnum = fin++instance (Known Nat n, Pos n) => Bounded (Fin n) where+  minBound = FZ+  maxBound = case (known :: Nat n) of+    S_ Z_   -> FZ+    S_ S_{} -> FS maxBound  elimFin :: (forall x. p (S x))         -> (forall x. Fin x -> p x -> p (S x))
src/Data/Type/Fin/Indexed.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE UndecidableSuperClasses #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -37,7 +38,7 @@ import Type.Class.Witness import Type.Family.Constraint import Type.Family.Nat-import Data.Type.Quantifier+-- import Data.Type.Quantifier  data IFin :: N -> N -> * where   IFZ :: IFin (S x) Z
src/Data/Type/Index.hs view
@@ -1,10 +1,11 @@+{-# LANGUAGE UndecidableSuperClasses #-}+{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE LambdaCase #-}@@ -29,10 +30,11 @@  module Data.Type.Index where -import Data.Type.Quantifier+-- import Data.Type.Quantifier import Type.Class.Higher import Type.Class.Known import Type.Class.Witness+import Type.Family.Constraint import Type.Family.List  data Index :: [k] -> k -> * where@@ -74,16 +76,14 @@   IZ   -> z   IS x -> s x $ elimIndex z s x -ixNil :: Index Ø a -> Void-ixNil = impossible+ixNil :: Index Ø a -> b+ixNil = absurd . impossible  onIxPred :: (Index as a -> Index bs a) -> Index (b :< as) a -> Index (b :< bs) a onIxPred f = \case   IZ   -> IZ   IS x -> IS $ f x --- Elem {{{- type a ∈ as = Elem as a infix 6 ∈ @@ -91,17 +91,45 @@   elemIndex :: Index as a  instance {-# OVERLAPPING #-} Elem (a :< as) a where-  elemIndex = IZ+  elemIndex   = IZ  instance {-# OVERLAPPABLE #-} Elem as a => Elem (b :< as) a where   elemIndex = IS elemIndex +instance Witness ØC (Elem as a) (Index as a) where+  (\\) r = \case+    IZ   -> r+    IS x -> r \\ x -instance {-# OVERLAPPING #-} Known (Index (a :< as)) a where-  known = IZ+instance (a ∈ as) => Known (Index as) a where+  type KnownC (Index as) a = (a ∈ as)+  known = elemIndex -instance {-# OVERLAPPABLE #-} Known (Index as) a => Known (Index (b :< as)) a where-  known = IS known+class EveryC c as => Every (c :: k -> Constraint) (as :: [k]) where+  type EveryC c as :: Constraint+  every :: Index as a -> Wit (c a) --- }}}+instance Every c Ø where+  type EveryC c Ø = ØC+  every = ixNil++instance (c a, Every c as) => Every c (a :< as) where+  type EveryC c (a :< as) = (c a, Every c as)+  every = \case+    IZ   -> Wit+    IS x -> every x++class ListC ((c <$> xs) <&> y)+  => Every2 (c :: k -> l -> Constraint) (xs :: [k]) (y :: l) where+  every2 :: Index xs x -> Wit (c x y)++instance Every2 c Ø y where+  every2 = ixNil++instance (c x y, Every2 c xs y) => Every2 c (x :< xs) y where+  every2 = \case+    IZ   -> Wit+    IS x -> every2 x++
src/Data/Type/Index/Trans.hs view
@@ -6,7 +6,6 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE GADTs #-}-{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-}@@ -19,15 +18,18 @@   , (:~:)(..)   ) where -import Data.Type.Index import Type.Class.Witness ((:~:)(..)) import Type.Family.List+import Type.Family.Tuple -ixList :: Index a b -> i b c -> IxList i a c-ixList = \case-  IZ   -> IxHead-  IS x -> IxTail . ixList x+type IxList' = IxList (:~:)+type IxEnv   = IxList (IxFirst (:~:)) +class IxLift (t :: (k -> m -> *) -> l -> m -> *) (x :: l) where+  type LiftI t x :: k+  ixLift :: i (LiftI t x) y+         -> t i x y+ data IxList (i :: k -> l -> *) :: [k] -> l -> * where   IxHead :: !(i a b)          -> IxList i (a :< as) b@@ -38,15 +40,27 @@   IxFirst :: !(i a b)           -> IxFirst i '(a,c) b +instance (p ~ '(Fst p,Snd p)) => IxLift IxFirst p where+  type LiftI IxFirst p = Fst p+  ixLift = IxFirst+ data IxSecond (i :: k -> l -> *) :: (m,k) -> l -> * where   IxSecond :: !(i a b)            -> IxSecond i '(c,a) b +instance (p ~ '(Fst p,Snd p)) => IxLift IxSecond p where+  type LiftI IxSecond p = Snd p+  ixLift = IxSecond+ 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++instance IxLift (IxOr i) (Right a) where+  type LiftI (IxOr i) (Right a) = a+  ixLift = IxOrR  data IxJust (i :: k -> l -> *) :: Maybe k -> l -> * where   IxJust :: !(i a b)
src/Data/Type/Length.hs view
@@ -1,9 +1,9 @@+{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE LambdaCase #-}@@ -29,10 +29,14 @@  module Data.Type.Length where -import Data.Type.Quantifier+-- import Data.Type.Quantifier+import Type.Class.Witness import Type.Class.Higher import Type.Class.Known+import Type.Family.Constraint import Type.Family.List+import Type.Family.Nat+import Data.Type.Nat  data Length :: [k] -> * where   LZ :: Length Ø@@ -62,6 +66,19 @@ instance Known Length as => Known Length (a :< as) where   type KnownC Length (a :< as) = Known Length as   known = LS known++instance (n ~ Len as) => Witness ØC (Known Nat n, Known Length as) (Length as) where+  type WitnessC ØC (Known Nat n, Known Length as) (Length as) = (n ~ Len as)+  (\\) r = \case+    LZ -> r+    LS l -> r \\ l++{-+natLen :: Nat (Len as) -> Length as+natLen = \case+  Z_   -> LZ+  S_ n -> _+-}  elimLength :: p Ø            -> (forall x xs. Length xs -> p xs -> p (x :< xs))
src/Data/Type/Nat.hs view
@@ -30,7 +30,7 @@  import Data.Type.Boolean import Data.Type.Equality-import Data.Type.Quantifier+-- import Data.Type.Quantifier import Type.Class.Higher import Type.Class.Known import Type.Class.Witness
src/Data/Type/Nat/Inequality.hs view
@@ -5,7 +5,6 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE GADTs #-}-{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-}
src/Data/Type/Option.hs view
@@ -79,5 +79,4 @@   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
@@ -44,7 +44,7 @@ import Data.Type.Conjunction import Data.Type.Index import Data.Type.Length-import Data.Type.Quantifier+-- import Data.Type.Quantifier import Type.Class.Higher import Type.Class.Known import Type.Class.Witness@@ -67,19 +67,15 @@   eq1 = \case     Ø -> \case       Ø -> True-      _ -> False     a :< as -> \case       b :< bs -> a =#= b && as =#= bs-      _       -> False  instance Ord1 f => Ord1 (Prod f) where   compare1 = \case     Ø -> \case       Ø -> EQ-      _ -> LT     a :< as -> \case       b :< bs -> compare1 a b `mappend` compare1 as bs-      _       -> GT  instance Show1 f => Show1 (Prod f) where   showsPrec1 d = \case@@ -276,12 +272,27 @@     Ø       -> pure Ø     a :< as -> (:<) <$> f IZ a <*> itraverse1 (f . IS) as +instance (Known Length as, Every (Known f) as) => Known (Prod f) as where+  type KnownC (Prod f) as = (Known Length as, Every (Known f) as)+  known = go known+    where+    go :: Every (Known f) xs => Length xs -> Prod f xs+    go = \case+      LZ   -> Ø+      LS l -> known :< go l++{- instance Known (Prod f) Ø where   known = Ø  instance (Known f a, Known (Prod f) as) => Known (Prod f) (a :< as) where   type KnownC (Prod f) (a :< as) = (Known f a, Known (Prod f) as)   known = known :< known+-}++type family Witnesses (ps :: [Constraint]) (qs :: [Constraint]) (f :: k -> *) (as :: [k]) :: Constraint where+  Witnesses Ø Ø f Ø = ØC+  Witnesses (p :< ps) (q :< qs) f (a :< as) = (Witness p q (f a), Witnesses ps qs f as)  instance Witness ØC ØC (Prod f Ø) where   r \\ _ = r
src/Data/Type/Product/Env.hs view
@@ -5,7 +5,6 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE GADTs #-}-{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-}@@ -110,4 +109,9 @@  instance IxFunctor1 (IxList (IxSecond (:~:))) (Env k) where   imap1 f = Env . imap1 (\i -> imap1 $ \j -> f $ ixList i j) . getEnv++ixList :: Index as a -> i a b -> IxList i as b+ixList = \case+  IZ   -> IxHead+  IS x -> IxTail . ixList x
− src/Data/Type/Quantifier.hs 
@@ -1,188 +0,0 @@-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE FlexibleInstances #-}-{-# 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 Type.Family.Constraint---- Some {{{--data Some (f :: k -> *) :: * where-  Some :: f a -> Some f---- | An eliminator for a 'Some' type.------ 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.------ 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--(>>-) :: Some f -> (forall a. f a -> r) -> r-(>>-) = some-infixl 1 >>---(>->) :: (forall x. f x -> Some g) -> (forall x. g x -> Some h) -> f a -> Some h-(f >-> g) a = f a >>- g-infixr 1 >->--withSome :: (forall a. f a -> r) -> Some f -> r-withSome f (Some a) = f a--onSome :: (forall a. f a -> g x) -> Some f -> Some g-onSome f (Some a) = Some (f a)--msome :: Monad m => f a -> m (Some f)-msome = return . Some--(>>=-) :: Monad m => m (Some f) -> (forall a. f a -> m r) -> m r-m >>=- f = do-  s <- m-  s >>- f-infixl 1 >>=----- }}}---- Some2 {{{--data Some2 (f :: k -> l -> *) :: * where-  Some2 :: f a b -> Some2 f--some2 :: Some2 f -> (forall a b. f a b -> r) -> r-some2 (Some2 a) f = f a--(>>--) :: Some2 f -> (forall a b. f a b -> r) -> r-(>>--) = some2-infixl 1 >>----(>-->) :: (forall x y. f x y -> Some2 g) -> (forall x y. g x y -> Some2 h) -> f a b -> Some2 h-(f >--> g) a = f a >>-- g-infixr 1 >-->--withSome2 :: (forall a b. f a b -> r) -> Some2 f -> r-withSome2 f (Some2 a) = f a--onSome2 :: (forall a b. f a b -> g x y) -> Some2 f -> Some2 g-onSome2 f (Some2 a) = Some2 (f a)--msome2 :: Monad m => f a b -> m (Some2 f)-msome2 = return . Some2--(>>=--) :: Monad m => m (Some2 f) -> (forall a b. f a b -> m r) -> m r-m >>=-- f = do-  s <- m-  s >>-- f-infixl 1 >>=------ }}}---- Some3 {{{--data Some3 (f :: k -> l -> m -> *) :: * where-  Some3 :: f a b c -> Some3 f--some3 :: Some3 f -> (forall a b c. f a b c -> r) -> r-some3 (Some3 a) f = f a--(>>---) :: Some3 f -> (forall a b c. f a b c -> r) -> r-(>>---) = some3-infixl 1 >>-----(>--->) :: (forall x y z. f x y z -> Some3 g) -> (forall x y z. g x y z -> Some3 h) -> f a b c -> Some3 h-(f >---> g) a = f a >>--- g-infixr 1 >--->--withSome3 :: (forall a b c. f a b c -> r) -> Some3 f -> r-withSome3 f (Some3 a) = f a--onSome3 :: (forall a b c. f a b c -> g x y z) -> Some3 f -> Some3 g-onSome3 f (Some3 a) = Some3 (f a)--msome3 :: Monad m => f a b c -> m (Some3 f)-msome3 = return . Some3--(>>=---) :: Monad m => m (Some3 f) -> (forall a b c. f a b c -> m r) -> m r-m >>=--- f = do-  s <- m-  s >>--- f-infixl 1 >>=------- }}}---- SomeC {{{--data SomeC (c :: k -> Constraint) (f :: k -> *) where-  SomeC :: c a => f a -> SomeC c f--someC :: SomeC c f -> (forall a. c a => f a -> r) -> r-someC (SomeC a) f = f a--(>>~) :: SomeC c f -> (forall a. c a => f a -> r) -> r-(>>~) = someC-infixl 1 >>~--msomeC :: (Monad m, c a) => f a -> m (SomeC c f)-msomeC = return . SomeC--(>>=~) :: Monad m => m (SomeC c f) -> (forall a. c a => f a -> m r) -> m r-m >>=~ f = do-  s <- m-  s >>~ f-infixl 1 >>=~---- }}}---- EveryN {{{--data Every (f :: k -> *) :: * where-  Every :: { instEvery :: forall a. f a } -> Every f--data Every2 (f :: k -> l -> *) :: * where-  Every2 :: { instEvery2 :: forall a b. f a b } -> Every2 f--data Every3 (f :: k -> l -> m -> *) :: * where-  Every3 :: { instEvery3 :: forall a b c. f a b c } -> Every3 f--data EveryC (c :: k -> Constraint) (f :: k -> *) :: * where-  EveryC :: { instEveryC :: forall a. c a => f a }-         -> EveryC c f---- }}}-
+ src/Data/Type/Remove.hs view
@@ -0,0 +1,148 @@+{-# 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.Remove+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- A @singleton@-esque type for representing the removal of an element from a type level list.+--+-----------------------------------------------------------------------------++module Data.Type.Remove where++-- import Data.Type.Quantifier+import Type.Class.Higher+import Type.Class.Known+import Type.Class.Witness+import Type.Family.Constraint+import Type.Family.List+import Type.Family.Nat+import Data.Type.Length+import Data.Type.Index+import Data.Type.Subset+import Data.Type.Product+import Data.Type.Sum+import Control.Arrow (second,right)++data Remove :: [k] -> k -> [k] -> * where+  RZ :: Remove (a :< as) a as+  RS :: !(Remove as a bs)+     -> Remove (b :< as) a (b :< bs)++deriving instance Eq   (Remove as a bs)+deriving instance Ord  (Remove as a bs)+deriving instance Show (Remove as a bs)++instance Eq1   (Remove as a)+instance Ord1  (Remove as a)+instance Show1 (Remove as a)++instance Eq2   (Remove as)+instance Ord2  (Remove as)+instance Show2 (Remove as)++instance Eq3   Remove+instance Ord3  Remove+instance Show3 Remove++instance Read3 Remove where+  readsPrec3 d = readParen (d > 10) $ \s0 ->+    [ (Some3 RZ,s1)+    | ("RZ",s1) <- lex s0+    ] +++    [ (i >>--- Some3 . RS,s2)+    | ("RS",s1) <- lex s0+    , (i,s2)    <- readsPrec3 11 s1+    ]++instance TestEquality (Remove as a) where+  testEquality = \case+    RZ -> \case+      RZ -> qed+      _  -> Nothing+    RS x -> \case+      RS y -> x =?= y //? qed+      _    -> Nothing++remLen :: Remove as a bs -> S (Len bs) :~: Len as+remLen = \case+  RZ   -> Refl+  RS r -> remLen r // Refl++elimRemove :: (forall xs. p (a :< xs) a xs)+           -> (forall x xs ys. Remove xs a ys -> p xs a ys -> p (x :< xs) a (x :< ys))+           -> Remove as a bs+           -> p as a bs+elimRemove z s = \case+  RZ   -> z+  RS r -> s r $ elimRemove z s r++remIx :: Remove as a bs -> Index as a+remIx = \case+  RZ   -> IZ+  RS r -> IS $ remIx r++remSub :: Length bs -> Remove as a bs -> Subset as bs+remSub = \case+  LZ   -> \case+    RZ -> Ø+  LS l -> \case+    RZ   -> IS IZ :< map1 (IS . IS) subRefl \\ l+    RS r -> IZ :< map1 IS (remSub l r)++ixRem :: Index as a -> Some (Remove as a)+ixRem = \case+  IZ   -> Some RZ+  IS x -> ixRem x >>- Some . RS++remProd :: Remove as a bs -> Prod f as -> (f a,Prod f bs)+remProd = \case+  RZ   -> (,) <$> head' <*> tail'+  RS r -> \(a :< as) -> second (a :<) $ remProd r as++remSum :: Remove as a bs -> Sum f as -> Either (f a) (Sum f bs)+remSum = \case+  RZ   -> \case+    InL a -> Left a+    InR b -> Right b+  RS r -> \case+    InL a -> Right $ InL a+    InR b -> right InR $ remSum r b++class Without (as :: [k]) (a :: k) (bs :: [k]) | as a -> bs where+  without :: Remove as a bs++instance {-# OVERLAPPING #-} (as ~ bs) => Without (a :< as) a bs where+  without = RZ++instance {-# OVERLAPPABLE #-} (cs ~ (b :< bs), Without as a bs) => Without (b :< as) a cs where+  without = RS without++instance Witness ØC (Without as a bs) (Remove as a bs) where+  (\\) r = \case+    RZ   -> r+    RS x -> r \\ x++instance (Without as a bs) => Known (Remove as a) bs where+  type KnownC (Remove as a) bs = Without as a bs+  known = without+
+ src/Data/Type/Subset.hs view
@@ -0,0 +1,92 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE GADTs #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Type.Subset+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- A @singleton@-esque type for representing subsets of a type level list.+--+-----------------------------------------------------------------------------++module Data.Type.Subset+  ( module Data.Type.Subset+  , module Exports+  ) where++-- import Data.Type.Quantifier+import Type.Class.Higher+import Type.Class.Known+import Type.Class.Witness+import Type.Family.List+import Data.Type.Index+import Data.Type.Length+import Data.Type.Product as Exports (Prod(..))+import Data.Type.Product (index)+import Data.Type.Sum (Sum(..),prj)+import Control.Applicative ((<|>))++type Subset as = Prod (Index as)++subNil :: Subset Ø as -> (as :~: Ø)+subNil = \case+  Ø      -> Refl+  x :< _ -> ixNil x++type as ⊆ bs = Every (Elem bs) as+infix 4 ⊆++subRefl :: Known Length as+  => Subset as as+subRefl = go known+  where+  go :: Length xs -> Subset xs xs+  go = \case+    LZ   -> Ø+    LS l -> IZ :< map1 IS (go l)++subTrans :: Subset as bs -> Subset bs cs -> Subset as cs+subTrans s = map1 $ subIx s++subProd :: Subset as bs -> Prod f as -> Prod f bs+subProd = \case+  Ø      -> pure Ø+  x :< s -> (:<) <$> index x <*> subProd s++subSum :: Subset as bs -> Sum f as -> Maybe (Sum f bs)+subSum = \case+  Ø      -> pure Nothing+  x :< s -> \t -> (InL <$> (prj t \\ x))+              <|> (InR <$> subSum s t)++subIx :: Subset as bs -> Index bs x -> Index as x+subIx = \case+  Ø      -> ixNil+  x :< s -> \case+    IZ   -> x+    IS y -> subIx s y++subExt :: Known Length as => (forall x. Index as x -> Index bs x) -> Subset bs as+subExt f = subExtBy f known++subExtBy :: (forall x. Index as x -> Index bs x) -> Length as -> Subset bs as+subExtBy f = \case+  LZ   -> Ø+  LS l -> f IZ :< subExtBy (f . IS) l+
src/Data/Type/Sum.hs view
@@ -32,7 +32,7 @@ module Data.Type.Sum where  import Data.Type.Index-import Data.Type.Quantifier+-- import Data.Type.Quantifier  import Type.Class.Higher import Type.Class.Witness
− src/Data/Type/Sym.hs 
@@ -1,67 +0,0 @@-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE GADTs #-}--------------------------------------------------------------------------------- |--- Module      :  Data.Type.Sym--- Copyright   :  Copyright (C) 2015 Kyle Carter--- License     :  BSD3------ Maintainer  :  Kyle Carter <kylcarte@indiana.edu>--- Stability   :  experimental--- Portability :  RankNTypes------ A @singleton@-esque type for representing type-level Symbols.-----------------------------------------------------------------------------------module Data.Type.Sym where--import Data.Type.Boolean-import Type.Class.Higher-import Type.Class.Known-import Type.Class.Witness-import Type.Family.Constraint-import Type.Family.Symbol-import Data.Proxy--data Sym :: Symbol -> * where-  Sym :: KnownSymbol x => Sym x--deriving instance Eq   (Sym x)-deriving instance Ord  (Sym x)--instance Show (Sym x) where-  showsPrec d x = showParen (d > 0)-    $ showString "Sym "-    . shows (symbol x)--instance Eq1   Sym-instance Ord1  Sym-instance Show1 Sym--instance TestEquality Sym where-  testEquality Sym Sym = sameSymbol Proxy Proxy--instance KnownSymbol x => Known Sym x where-  type KnownC Sym x = KnownSymbol x-  known = Sym--instance Witness ØC (KnownSymbol x) (Sym x) where-  r \\ Sym = r--symbol :: Sym x -> String-symbol x = symbolVal x \\ x-
src/Data/Type/Vector.hs view
@@ -25,13 +25,13 @@ -- Stability   :  experimental -- Portability :  RankNTypes ----- 'V' and its combinator analog 'VT' represent lists+-- 'Vec' and its combinator analog 'VecT' represent lists -- of known length, characterized by the index @(n :: N)@ in--- @'V' n a@ or @'VT' n f a@.+-- @'Vec' n a@ or @'VecT' 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+-- The operations on 'Vec' and 'VecT' correspond to the type level arithmetic -- operations on the kind 'N'. -- -----------------------------------------------------------------------------@@ -44,6 +44,7 @@ import Data.Type.Nat import Data.Type.Product (Prod(..),curry',pattern (:>)) +import Type.Class.Higher import Type.Class.Known import Type.Class.Witness @@ -54,162 +55,179 @@ import qualified Data.List as L import Data.Monoid -data VT (n :: N) (f :: k -> *) :: k -> * where-  ØV   :: VT Z f a-  (:*) :: !(f a) -> !(VT n f a) -> VT (S n) f a+data VecT (n :: N) (f :: k -> *) :: k -> * where+  ØV   :: VecT Z f a+  (:*) :: !(f a) -> !(VecT n f a) -> VecT (S n) f a infixr 4 :* -elimVT :: p Z+elimVecT :: p Z        -> (forall x. f a -> p x -> p (S x))-       -> VT n f a+       -> VecT n f a        -> p n-elimVT z s = \case+elimVecT z s = \case   ØV      -> z-  a :* as -> s a $ elimVT z s as+  a :* as -> s a $ elimVecT z s as  elimV :: p Z       -> (forall x. a -> p x -> p (S x))-      -> V n a+      -> Vec n a       -> p n-elimV z s = elimVT z $ s . getI+elimV z s = elimVecT z $ s . getI -type V n = VT n I-pattern (:+) :: a -> V n a -> V (S n) a+type Vec n = VecT n I+pattern (:+) :: a -> Vec n a -> Vec (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)+deriving instance Eq   (f a) => Eq   (VecT n f a)+deriving instance Ord  (f a) => Ord  (VecT n f a)+deriving instance Show (f a) => Show (VecT n f a) -(.++) :: VT x f a -> VT y f a -> VT (x + y) f a+(.++) :: VecT x f a -> VecT y f a -> VecT (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 :: forall n f a. Known Nat n => f a -> VecT n f a vrep a = go (known :: Nat n)   where-  go :: Nat x -> VT x f a+  go :: Nat x -> VecT x f a   go = \case     Z_   -> ØV     S_ x -> a :* go x -head' :: VT (S n) f a -> f a+head' :: VecT (S n) f a -> f a head' (a :* _) = a -tail' :: VT (S n) f a -> VT n f a+tail' :: VecT (S n) f a -> VecT 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 :: (VecT m f a -> VecT n f a) -> VecT (S m) f a -> VecT (S n) f a onTail f (a :* as) = a :* f as -vDel :: Fin n -> VT n f a -> VT (Pred n) f a+vDel :: Fin n -> VecT n f a -> VecT (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 :: (Fin n -> f a -> g b) -> VecT n f a -> VecT 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 :: Monoid m => (Fin n -> f a -> m) -> VecT 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 :: Applicative h => (Fin n -> f a -> h (g b)) -> VecT n f a -> h (VecT 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 :: Fin n -> VecT 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+index' :: Fin n -> Vec n a -> a+index' i = getI . index i++vmap :: (f a -> g b) -> VecT n f a -> VecT 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 a -> g b -> h c) -> VecT n f a -> VecT n g b -> VecT n h c vap f = \case-  ØV  -> \_ -> ØV+  ØV      -> const Ø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 :: (f a -> b -> b) -> b -> VecT 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' :: (b -> b -> b) -> b -> (f a -> b) -> VecT 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 :: Monoid m => (f a -> m) -> VecT 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+withVecT :: [f a] -> (forall n. VecT n f a -> r) -> r+withVecT as k = case as of   []      -> k ØV-  a : as' -> withVT as' $ \v -> k $ a :* v+  a : as' -> withVecT as' $ \v -> k $ a :* v -withV :: [a] -> (forall n. V n a -> r) -> r-withV as k = withVT (I <$> as) k+withV :: [a] -> (forall n. Vec n a -> r) -> r+withV as = withVecT (I <$> as) -findV :: Eq a => a -> V n a -> Maybe (Fin n)-findV = findVT . I+findV :: Eq a => a -> Vec n a -> Maybe (Fin n)+findV = findVecT . I -findVT :: Eq (f a) => f a -> VT n f a -> Maybe (Fin n)-findVT a = \case+findVecT :: Eq (f a) => f a -> VecT n f a -> Maybe (Fin n)+findVecT a = \case   ØV      -> Nothing   b :* as -> if a == b     then Just FZ-    else FS <$> findVT a as+    else FS <$> findVecT a as -instance Functor f => Functor (VT n f) where+instance Functor1 (VecT n) where+  map1 f = \case+    ØV      -> ØV+    a :* as -> f a :* map1 f as++instance Foldable1 (VecT n) where+  foldMap1 f = \case+    ØV -> mempty+    a :* as -> f a <> foldMap1 f as++instance Traversable1 (VecT n) where+  traverse1 f = \case+    ØV      -> pure ØV+    a :* as -> (:*) <$> f a <*> traverse1 f as++instance Functor f => Functor (VecT n f) where   fmap = vmap . fmap -instance (Applicative f, Known Nat n) => Applicative (VT n f) where+instance (Applicative f, Known Nat n) => Applicative (VecT n f) where   pure  = vrep . pure   (<*>) = vap (<*>) -instance (Monad f, Known Nat n) => Monad (VT n f) where+instance (Monad f, Known Nat n) => Monad (VecT n f) where   v >>= f = imap (\x -> (>>= index x . f)) v -instance Foldable f => Foldable (VT n f) where+instance Foldable f => Foldable (VecT n f) where   foldMap f = \case     ØV      -> mempty     a :* as -> foldMap f a <> foldMap f as -instance Traversable f => Traversable (VT n f) where+instance Traversable f => Traversable (VecT 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)+instance (Witness p q (f a), n ~ S x) => Witness p q (VecT n f a) where+  type WitnessC p q (VecT 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+instance Witness ØC (Known Nat n) (VecT n f a) where   (\\) r = \case     ØV      -> r     _ :* as -> r \\ as -instance (Num (f a), Known Nat n) => Num (VT n f a) where+instance (Num (f a), Known Nat n) => Num (VecT n f a) where   (*)         = vap (*)   (+)         = vap (+)   (-)         = vap (-)@@ -234,12 +252,12 @@  type family Matrix (ns :: [N]) :: * -> * where   Matrix Ø         = I-  Matrix (n :< ns) = VT n (Matrix ns)+  Matrix (n :< ns) = VecT n (Matrix ns) -vgen_ :: Known Nat n => (Fin n -> f a) -> VT n f a+vgen_ :: Known Nat n => (Fin n -> f a) -> VecT n f a vgen_ = vgen known -vgen :: Nat n -> (Fin n -> f a) -> VT n f a+vgen :: Nat n -> (Fin n -> f a) -> VecT n f a vgen x f = case x of   Z_   -> ØV   S_ y -> f FZ :* vgen y (f . FS)@@ -255,10 +273,10 @@ 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 :: VecT n (VecT n f) a -> VecT n f a diagonal = imap index -vtranspose :: Known Nat n => VT m (VT n f) a -> VT n (VT m f) a+vtranspose :: Known Nat n => VecT m (VecT n f) a -> VecT n (VecT 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@@ -279,7 +297,7 @@ 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 :: (VecT n ((->) String) String -> ShowS) -> (f a -> ShowS) -> VecT n f a -> ShowS ppVec pV pF = pV . vmap pF  ppMatrix :: forall ns a. (Show a, Known Length ns) => M ns a -> IO ()@@ -343,7 +361,7 @@ infixl 6 ^+^, ^-^  instance Additive I-instance (Additive f, Known Nat n) => Additive (VT n f) where+instance (Additive f, Known Nat n) => Additive (VecT n f) where   zero   = vrep zero   liftU2 = vap . liftU2   liftI2 = vap . liftI2@@ -363,8 +381,8 @@ 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)+instance (Affine f, Known Nat n) => Affine (VecT n f) where+  type Diff (VecT n f) = VecT n (Diff f)   (.-.) = vap (.-.)   (.+^) = vap (.+^)   (.-^) = vap (.-^)@@ -388,7 +406,7 @@ instance Metric I where   dot (I a) (I b) = a * b -instance (Metric f, Known Nat n) => Metric (VT n f) where+instance (Metric f, Known Nat n) => Metric (VecT n f) where   dot a b = getSum $ foldMap Sum $ vap ((I .) . dot) a b  (*^) :: (Functor f, Num a) => a -> f a -> f a
src/Type/Class/Higher.hs view
@@ -22,12 +22,15 @@ -- Stability   :  experimental -- Portability :  RankNTypes ----- Higher order analogs of type classes from the Prelude.+-- Higher order analogs of type classes from the Prelude,+-- and quantifier data types. ----------------------------------------------------------------------------  module Type.Class.Higher where -import Data.Type.Quantifier+import Type.Class.Witness+import Type.Family.Constraint+import Data.Maybe (fromMaybe)  -- EqN {{{ @@ -124,7 +127,6 @@ shows1 :: Show1 f => f a -> ShowS shows1 = showsPrec1 0 - class Show2 (f :: k -> l -> *) where   showsPrec2 :: Int -> f a b -> ShowS   default showsPrec2 :: Show (f a b) => Int -> f a b -> ShowS@@ -135,7 +137,6 @@ shows2 :: Show2 f => f a b -> ShowS shows2 = showsPrec2 0 - class Show3 (f :: k -> l -> m -> *) where   showsPrec3 :: Int -> f a b c -> ShowS   default showsPrec3 :: Show (f a b c) => Int -> f a b c -> ShowS@@ -233,4 +234,164 @@           -> t f' g' b  -- }}}++++-- Some {{{++data Some (f :: k -> *) :: * where+  Some :: f a -> Some f++instance (TestEquality f, Eq1 f) => Eq (Some f) where+  Some a == Some b = fromMaybe False $ testEquality a b //? return (eq1 a b)++-- | An eliminator for a 'Some' type.+--+-- 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.+--+-- 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++(>>-) :: Some f -> (forall a. f a -> r) -> r+(>>-) = some+infixl 1 >>-++(>->) :: (forall x. f x -> Some g) -> (forall x. g x -> Some h) -> f a -> Some h+(f >-> g) a = f a >>- g+infixr 1 >->++withSome :: (forall a. f a -> r) -> Some f -> r+withSome f (Some a) = f a++onSome :: (forall a. f a -> g x) -> Some f -> Some g+onSome f (Some a) = Some (f a)++msome :: Monad m => f a -> m (Some f)+msome = return . Some++(>>=-) :: Monad m => m (Some f) -> (forall a. f a -> m r) -> m r+m >>=- f = do+  s <- m+  s >>- f+infixl 1 >>=-++-- }}}++-- Some2 {{{++data Some2 (f :: k -> l -> *) :: * where+  Some2 :: f a b -> Some2 f++some2 :: Some2 f -> (forall a b. f a b -> r) -> r+some2 (Some2 a) f = f a++(>>--) :: Some2 f -> (forall a b. f a b -> r) -> r+(>>--) = some2+infixl 1 >>--++(>-->) :: (forall x y. f x y -> Some2 g) -> (forall x y. g x y -> Some2 h) -> f a b -> Some2 h+(f >--> g) a = f a >>-- g+infixr 1 >-->++withSome2 :: (forall a b. f a b -> r) -> Some2 f -> r+withSome2 f (Some2 a) = f a++onSome2 :: (forall a b. f a b -> g x y) -> Some2 f -> Some2 g+onSome2 f (Some2 a) = Some2 (f a)++msome2 :: Monad m => f a b -> m (Some2 f)+msome2 = return . Some2++(>>=--) :: Monad m => m (Some2 f) -> (forall a b. f a b -> m r) -> m r+m >>=-- f = do+  s <- m+  s >>-- f+infixl 1 >>=--++-- }}}++-- Some3 {{{++data Some3 (f :: k -> l -> m -> *) :: * where+  Some3 :: f a b c -> Some3 f++some3 :: Some3 f -> (forall a b c. f a b c -> r) -> r+some3 (Some3 a) f = f a++(>>---) :: Some3 f -> (forall a b c. f a b c -> r) -> r+(>>---) = some3+infixl 1 >>---++(>--->) :: (forall x y z. f x y z -> Some3 g) -> (forall x y z. g x y z -> Some3 h) -> f a b c -> Some3 h+(f >---> g) a = f a >>--- g+infixr 1 >--->++withSome3 :: (forall a b c. f a b c -> r) -> Some3 f -> r+withSome3 f (Some3 a) = f a++onSome3 :: (forall a b c. f a b c -> g x y z) -> Some3 f -> Some3 g+onSome3 f (Some3 a) = Some3 (f a)++msome3 :: Monad m => f a b c -> m (Some3 f)+msome3 = return . Some3++(>>=---) :: Monad m => m (Some3 f) -> (forall a b c. f a b c -> m r) -> m r+m >>=--- f = do+  s <- m+  s >>--- f+infixl 1 >>=---++-- }}}++-- SomeC {{{++data SomeC (c :: k -> Constraint) (f :: k -> *) where+  SomeC :: c a => f a -> SomeC c f++someC :: SomeC c f -> (forall a. c a => f a -> r) -> r+someC (SomeC a) f = f a++(>>~) :: SomeC c f -> (forall a. c a => f a -> r) -> r+(>>~) = someC+infixl 1 >>~++msomeC :: (Monad m, c a) => f a -> m (SomeC c f)+msomeC = return . SomeC++(>>=~) :: Monad m => m (SomeC c f) -> (forall a. c a => f a -> m r) -> m r+m >>=~ f = do+  s <- m+  s >>~ f+infixl 1 >>=~++-- }}}++{-+-- EveryN {{{++data Every (f :: k -> *) :: * where+  Every :: { instEvery :: forall a. f a } -> Every f++data Every2 (f :: k -> l -> *) :: * where+  Every2 :: { instEvery2 :: forall a b. f a b } -> Every2 f++data Every3 (f :: k -> l -> m -> *) :: * where+  Every3 :: { instEvery3 :: forall a b c. f a b c } -> Every3 f++data EveryC (c :: k -> Constraint) (f :: k -> *) :: * where+  EveryC :: { instEveryC :: forall a. c a => f a }+         -> EveryC c f++-- }}}+-}
src/Type/Class/Known.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE UndecidableSuperClasses #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ConstraintKinds #-}
src/Type/Class/Witness.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE UndecidableSuperClasses #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE AllowAmbiguousTypes #-}@@ -5,7 +6,6 @@ {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-}-{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-}@@ -156,7 +156,7 @@ infixr 6 ∨  eitherC :: forall f g a b. f a :- b -> g a :- b -> (f ∨ g) a :- b-eitherC f g = Sub $ case ((disjC :: Either (Wit (f a)) (Wit (g a))),f,g) of+eitherC f g = Sub $ case (disjC :: Either (Wit (f a)) (Wit (g a)),f,g) of   (Left  a,Sub b,_    ) -> b \\ a   (Right a,_    ,Sub b) -> b \\ a @@ -180,7 +180,7 @@ -- Initial/Terminal {{{  toEquality :: (a ~ b) :- (c ~ d) -> a :~: b -> c :~: d-toEquality p = \Refl -> Refl \\ p+toEquality p Refl = Refl \\ p  commute :: (a ~ b) :- (b ~ a) commute = Sub Wit
src/Type/Family/Bool.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-}@@ -34,7 +35,7 @@ import Type.Class.Witness as Exports (type (==)) import Data.Type.Bool as Exports (type If, type Not, type (||), type (&&)) -type family BoolC (b :: Bool) :: Constraint where+type family BoolC (b :: Bool) = (c :: Constraint) | c -> b where   BoolC True  = ØC   BoolC False = Fail
src/Type/Family/Constraint.hs view
@@ -1,9 +1,9 @@+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE UndecidableSuperClasses #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-}-{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE LambdaCase #-}@@ -43,4 +43,7 @@   type IffC True  t f = t instance f => Iff False t f where   type IffC False t f = f++class d (c a) => Comp (d :: l -> Constraint) (c :: k -> l) (a :: k)+instance d (c a) => Comp d c a
src/Type/Family/Either.hs view
@@ -1,9 +1,7 @@ {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-}-{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE LambdaCase #-}
src/Type/Family/List.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-}@@ -74,7 +75,7 @@  -- | Type-level list snoc. type family (as :: [k]) >: (a :: k) :: [k] where-  Ø         >: a = Only a+  Ø         >: a = a :< Ø   (b :< as) >: a = b :< (as >: a) infixl 6 >: @@ -139,7 +140,7 @@ -- | 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+type family ListC (cs :: [Constraint]) = (c :: Constraint) | c -> cs where   ListC  Ø        = ØC   ListC (c :< cs) = (c, ListC cs) @@ -179,7 +180,7 @@   Snds  Ø        = Ø   Snds (p :< ps) = Snd p :< Snds ps -type family Zip (as :: [k]) (bs :: [l]) :: [(k,l)] where+type family Zip (as :: [k]) (bs :: [l]) = (cs :: [(k,l)]) | cs -> as bs where   Zip  Ø         Ø        = Ø   Zip (a :< as) (b :< bs) = a#b :< Zip as bs
src/Type/Family/Maybe.hs view
@@ -1,9 +1,7 @@ {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-}-{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE LambdaCase #-}
src/Type/Family/Nat.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-}@@ -63,7 +64,7 @@   NatEq (S x) (S y) = NatEq x y type instance x == y = NatEq x y -type family Iota (x :: N) :: [N] where+type family Iota (x :: N) = (xs :: [N]) | xs -> x where   Iota Z     = Ø   Iota (S x) = x :< Iota x @@ -73,6 +74,8 @@ type family Pred (x :: N) :: N where   Pred (S n) = n +type Pos n = (n ~ S (Pred n))+ predCong :: (x ~ y) :- (Pred x ~ Pred y) predCong = Sub Wit @@ -81,6 +84,11 @@   S x + y = S (x + y) infixr 6 + +data AddW (f :: N -> *) :: N -> * where+  AddW :: !(f x)+       -> !(f y)+       -> AddW f (x + y)+ addCong :: (w ~ y,x ~ z) :- ((w + x) ~ (y + z)) addCong = Sub Wit @@ -88,6 +96,11 @@   Z   * y = Z   S x * y = (x * y) + y infixr 7 *++data MulW (f :: N -> *) :: N -> * where+  MulW :: !(f x)+       -> !(f y)+       -> MulW f (x * y)  mulCong :: (w ~ y,x ~ z) :- ((w * x) ~ (y * z)) mulCong = Sub Wit
− src/Type/Family/Symbol.hs 
@@ -1,7 +0,0 @@--module Type.Family.Symbol-  ( module GHC.TypeLits-  ) where--import GHC.TypeLits (Symbol,KnownSymbol,sameSymbol,symbolVal)-
type-combinators.cabal view
@@ -1,5 +1,5 @@ name: type-combinators-version: 0.2.2.1+version: 0.2.4.0 category: Data synopsis: A collection of data types for type-level programming cabal-version: >=1.10@@ -17,9 +17,11 @@  library     exposed-modules:+        -- Data.Type.Polynomial         Data.Type.Boolean         Data.Type.Combinator         Data.Type.Conjunction+        Data.Type.Difference         Data.Type.Disjunction         Data.Type.Fin         Data.Type.Fin.Indexed@@ -32,10 +34,12 @@         Data.Type.Product         Data.Type.Product.Env         Data.Type.Product.Lifted+        Data.Type.Remove+        Data.Type.Subset         Data.Type.Sum         Data.Type.Sum.Lifted-        Data.Type.Sym-        Data.Type.Quantifier+        -- Data.Type.Sym+        -- Data.Type.Quantifier         Data.Type.Vector         Type.Class.Higher         Type.Class.Known@@ -47,10 +51,10 @@         Type.Family.Maybe         Type.Family.Monoid         Type.Family.Nat-        Type.Family.Symbol+        -- Type.Family.Symbol         Type.Family.Tuple     build-depends:-        base >=4.8 && <4.9+        base >=4.9 && <5.0     default-language: Haskell2010     hs-source-dirs: src     ghc-options: -Wall -fno-warn-unticked-promoted-constructors