type-combinators 0.2.0.0 → 0.2.1.0

raw patch · 12 files changed

+473/−6 lines, 12 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• src/Data/Type/Boolean.hs +104/−0
• src/Data/Type/Fin/Indexed.hs +179/−0
• src/Data/Type/Nat.hs +6/−0
• src/Data/Type/Nat/Inequality.hs +82/−0
• src/Data/Type/Quantifier.hs +12/−0
• src/Data/Type/Sym.hs +1/−1
• src/Type/Class/Witness.hs +10/−2
• src/Type/Family/Bool.hs +62/−0
• src/Type/Family/Constraint.hs +2/−1
• src/Type/Family/List.hs +8/−1
• src/Type/Family/Nat.hs +1/−0
• type-combinators.cabal +6/−1

@@ -0,0 +1,104 @@+{-# 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.Boolean+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- A @singleton@-esque type for type-level Bool values.+--+-----------------------------------------------------------------------------++module Data.Type.Boolean where++import Data.Type.Quantifier (Some(..))+import Type.Family.Bool+import Type.Class.Known+import Type.Class.Higher++data Boolean :: Bool -> * where+  False_ :: Boolean False+  True_  :: Boolean True++deriving instance Eq   (Boolean b)+deriving instance Ord  (Boolean b)+deriving instance Show (Boolean b)++instance Eq1   Boolean+instance Ord1  Boolean+instance Show1 Boolean++instance Read1 Boolean where+  readsPrec1 _ s0 =+    [ (Some True_,s1)+    | ("True_",s1) <- lex s0+    ] +++    [ (Some False_,s1)+    | ("False_",s1) <- lex s0+    ]++not' :: Boolean a -> Boolean (Not a)+not' = \case+  False_ -> True_+  True_  -> False_++(.||) :: Boolean a -> Boolean b -> Boolean (a || b)+(.||) = \case+  False_ -> id+  True_  -> const True_+infixr 2 .||++(.&&) :: Boolean a -> Boolean b -> Boolean (a && b)+(.&&) = \case+  False_ -> const False_+  True_  -> id+infixr 3 .&&++(.^^) :: Boolean a -> Boolean b -> Boolean (a ^^ b)+a .^^ b = (a .|| b) .&& not' (a .&& b)+infixr 4 .^^++(==>) :: Boolean a -> Boolean b -> Boolean (a ==> b)+a ==> b = not' a .|| b+infixr 1 ==>++(<==>) :: Boolean a -> Boolean b -> Boolean (a <==> b)+(<==>) = (.==)+infixr 1 <==>++class BoolEq (f :: k -> *) where+  (.==) :: f a -> f b -> Boolean (a == b)+infix 4 .==++instance BoolEq Boolean where+  (.==) = \case+    False_ -> \case+      False_ -> True_+      True_  -> False_+    True_  -> \case+      False_ -> False_+      True_  -> True_++instance Known Boolean True where+  known = True_++instance Known Boolean False where+  known = False_+

@@ -0,0 +1,179 @@+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE GADTs #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Type.Fin.Indexed+-- 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,+-- indexed by its Nat value.+--+-----------------------------------------------------------------------------++module Data.Type.Fin.Indexed where++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++data IFin :: N -> N -> * where+  IFZ :: IFin (S x) Z+  IFS :: !(IFin x y) -> IFin (S x) (S y)++deriving instance Eq   (IFin x y)+deriving instance Ord  (IFin x y)+deriving instance Show (IFin x y)++instance Eq1   (IFin x)+instance Ord1  (IFin x)+instance Show1 (IFin x)++instance Eq2   IFin+instance Ord2  IFin+instance Show2 IFin++instance Read2 IFin where+  readsPrec2 d = readParen (d > 10) $ \s0 ->+    [ (Some2 IFZ,s1)+    | ("IFZ",s1) <- lex s0+    ] ++ +    [ (n >>-- Some2 . IFS,s2)+    | ("IFS",s1) <- lex s0+    , (n,s2)    <- readsPrec2 11 s1+    ]++class LTC x y => LessEq (x :: N) (y :: N) where+  type LTC x y :: Constraint+  liftIFin :: IFin x z -> IFin y z++instance LessEq Z y where+  type LTC Z y = ØC+  liftIFin = absurd . ifinZ++instance (y ~ S (Pred y), LessEq x (Pred y)) => LessEq (S x) y where+  type LTC (S x) y = (y ~ S (Pred y), LessEq x (Pred y))+  liftIFin = \case+    IFZ   -> IFZ+    IFS x -> IFS $ liftIFin x++ifinZ :: IFin Z x -> Void+ifinZ = impossible++weaken :: IFin x y -> IFin (S x) y+weaken = \case+  IFZ   -> IFZ+  IFS n -> IFS $ weaken n++ifinNat :: IFin x y -> Nat y+ifinNat = \case+  IFZ   -> Z_+  IFS n -> S_ $ ifinNat n++ifinVal :: IFin x y -> Int+ifinVal = natVal . ifinNat++onIFinPred :: (forall x. IFin m x -> IFin n x) -> IFin (S m) y -> IFin (S n) y+onIFinPred f = \case+  IFZ   -> IFZ+  IFS m -> IFS $ f m++{-+-- | Map a finite set to a lower finite set without+-- one of its members.+without :: IFin n x -> IFin n y -> Maybe (IFin (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+-}++-- | An @IFin x y@ is a 'Witness' that @x >= 1@.+--+-- That is, @'Pred' x@ is well defined.+instance (x' ~ Pred x) => Witness ØC (S x' ~ x) (IFin x y) where+  type WitnessC ØC (S x' ~ x) (IFin x y) = (x' ~ Pred x)+  (\\) r = \case+    IFZ   -> r+    IFS _ -> r++{-+elimFin :: (forall x. p (S x))+        -> (forall x. Fin x -> p x -> p (S x))+        -> Fin n -> p n+elimFin z s = \case+  FZ   -> z+  FS n -> s n $ elimFin z s 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++-- | 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+-}+

@@ -85,6 +85,12 @@       Z_   -> Nothing       S_ y -> testEquality x y //? qed +pred' :: Nat (S x) -> Nat x+pred' (S_ x) = x++onNatPred :: (Nat x -> Nat y) -> Nat (S x) -> Nat (S y)+onNatPred f (S_ x) = S_ $ f x+ _Z :: Z :~: Z _Z = Refl 

@@ -0,0 +1,82 @@+{-# 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.Nat.Inequality where++import Data.Type.Nat+import Type.Class.Known+import Type.Class.Witness+import Type.Family.Constraint+import Type.Family.Nat++type family (x :: N) < (y :: N) :: Bool where+  Z   < Z   = False+  Z   < S y = True+  S x < Z   = False+  S x < S y = x < y+infix 4 <++type family (x :: N) > (y :: N) :: Bool where+  Z   > Z   = False+  Z   > S y = False+  S x > Z   = True+  S x > S y = x > y+infix 4 >++data NatLT :: N -> N -> * where+  LTZ :: NatLT Z (S y)+  LTS :: !(NatLT x y)+      -> NatLT (S x) (S y)++data NatEQ :: N -> N -> * where+  EQZ :: NatEQ Z Z+  EQS :: !(NatEQ x y)+      -> NatEQ (S x) (S y)++data NatGT :: N -> N -> * where+  GTZ :: NatGT (S x) Z+  GTS :: !(NatGT x y)+      -> NatGT (S x) (S y)++instance (lt ~ (x < y), eq ~ (x == y), gt ~ (x > y), y' ~ Pred y) => Witness ØC (y ~ S y', Known Nat x, lt ~ True, eq ~ False, gt ~ False) (NatLT x y) where+  type WitnessC ØC (y ~ S y', Known Nat x, lt ~ True, eq ~ False, gt ~ False) (NatLT x y) = (lt ~ (x < y), eq ~ (x == y), gt ~ (x > y), y' ~ Pred y)+  (\\) r = \case+    LTZ   -> r+    LTS l -> r \\ l++instance (lt ~ (x < y), eq ~ (x == y), gt ~ (x > y)) => Witness ØC (x ~ y, Known Nat x, lt ~ False, eq ~ True, gt ~ False) (NatEQ x y) where+  type WitnessC ØC (x ~ y, Known Nat x, lt ~ False, eq ~ True, gt ~ False) (NatEQ x y) = (lt ~ (x < y), eq ~ (x == y), gt ~ (x > y))+  (\\) r = \case+    EQZ   -> r+    EQS l -> r \\ l++instance (lt ~ (x < y), eq ~ (x == y), gt ~ (x > y), x' ~ Pred x) => Witness ØC (x ~ S x', Known Nat y, lt ~ False, eq ~ False, gt ~ True) (NatGT x y) where+  type WitnessC ØC (x ~ S x', Known Nat y, lt ~ False, eq ~ False, gt ~ True) (NatGT x y) = (lt ~ (x < y), eq ~ (x == y), gt ~ (x > y), x' ~ Pred x)+  (\\) r = \case+    GTZ   -> r+    GTS l -> r \\ l++natCompare :: Nat x -> Nat y -> Either (NatLT x y) (Either (NatEQ x y) (NatGT x y))+natCompare = \case+  Z_   -> \case+    Z_   -> Right $ Left EQZ+    S_ _ -> Left LTZ+  S_ x -> \case+    Z_   -> Right $ Right GTZ+    S_ y -> case natCompare x y of+      Left         lt  -> Left          $ LTS lt+      Right (Left  eq) -> Right $ Left  $ EQS eq+      Right (Right gt) -> Right $ Right $ GTS gt+

@@ -59,6 +59,10 @@ (>>-) = 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 @@ -79,6 +83,10 @@ (>>--) = 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 @@ -98,6 +106,10 @@ (>>---) :: 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

@@ -44,7 +44,7 @@  instance Show (Sym x) where   showsPrec d x = showParen (d > 0)-    $ showString "Sym :: Sym "+    $ showString "Sym "     . shows (symbol x)  instance Eq1   Sym

@@ -106,6 +106,10 @@   (\\) :: p => (q => r) -> t -> r infixl 1 \\ +(//) :: (Witness p q t, p) => t -> (q => r) -> r+t // r = r \\ t+infixr 0 //+ -- | Convert a 'Witness' to a canonical reified 'Constraint'. witnessed :: Witness ØC q t => t -> Wit q witnessed t = Wit \\ t@@ -185,8 +189,6 @@ top :: a :- ØC top = Sub Wit -type Fail = (True ~ False)- bottom :: Fail :- c bottom = falso @@ -220,6 +222,12 @@   Just t -> (\\ t)   _      -> \_ -> Nothing infixr 0 //?++(//?+) :: (Witness p q t, p) => Either e t -> (q => Either e r) -> Either e r+(//?+) = \case+  Left  e -> \_ -> Left e+  Right t -> (\\ t)+infixr 0 //?+  witMaybe :: (Witness p q t, p) => Maybe t -> (q => Maybe r) -> Maybe r -> Maybe r witMaybe mt y n = case mt of

@@ -0,0 +1,62 @@+{-# 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.Bool+-- 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 @Bool@s.+----------------------------------------------------------------------------++module Type.Family.Bool+  ( module Type.Family.Bool+  , type (==)+  ) where++import Type.Family.Constraint+import Type.Class.Witness (type (==))++type family BoolC (b :: Bool) :: Constraint where+  BoolC True  = ØC+  BoolC False = Fail++type family (a :: Bool) || (b :: Bool) :: Bool where+  True  || b = True+  False || b = b+infixr 2 ||++type family (a :: Bool) && (b :: Bool) :: Bool where+  True  && b = b+  False && b = False+infixr 3 &&++type family Not (a :: Bool) :: Bool where+  Not True  = False+  Not False = True++type a ==> b = Not a || b+infixr 1 ==>++type a <==> b = a == b+infixr 1 <==>++type a ^^ b = (a || b) && Not (a && b)+infixr 4 ^^+

@@ -34,7 +34,8 @@ import GHC.Exts (Constraint)  -- | The empty 'Constraint'.-type ØC = (() :: Constraint)+type ØC   = (() :: Constraint)+type Fail = (True ~ False)  class IffC b t f => Iff (b :: Bool) (t :: Constraint) (f :: Constraint) where   type IffC b t f :: Constraint

@@ -40,7 +40,7 @@ -- | Type-level singleton list. type Only a = '[a] --- Null,Append {{{+-- Null,Append,Concat {{{  type family Null (as :: [k]) :: Bool where   Null Ø         = True@@ -60,6 +60,13 @@  appendCong :: (a ~ b,c ~ d) :- ((a ++ c) ~ (b ++ d)) appendCong = Sub Wit++type family Concat (ls :: [[k]]) :: [k] where+  Concat Ø         = Ø+  Concat (l :< ls) = l ++ Concat ls++concatCong :: (as ~ bs) :- (Concat as ~ Concat bs)+concatCong = Sub Wit  -- }}} 

@@ -30,6 +30,7 @@ module Type.Family.Nat where  import Data.Type.Equality+import Type.Family.Constraint import Type.Family.List import Type.Class.Witness 

@@ -1,5 +1,5 @@ name: type-combinators-version: 0.2.0.0+version: 0.2.1.0 category: Data synopsis: A collection of data types for type-level programming cabal-version: >=1.10@@ -7,6 +7,7 @@ license: BSD3 license-file: LICENSE maintainer: kylcarte@gmail.com+copyright: (c) 2015 Kyle Carter, all rights reserved author: Kyle Carter homepage: https://github.com/kylcarte/type-combinators @@ -16,13 +17,16 @@  library     exposed-modules:+        Data.Type.Boolean         Data.Type.Combinator         Data.Type.Conjunction         Data.Type.Disjunction         Data.Type.Fin+        Data.Type.Fin.Indexed         Data.Type.Index         Data.Type.Length         Data.Type.Nat+        Data.Type.Nat.Inequality         Data.Type.Option         Data.Type.Product         Data.Type.Product.Lifted@@ -34,6 +38,7 @@         Type.Class.Higher         Type.Class.Known         Type.Class.Witness+        Type.Family.Bool         Type.Family.Constraint         Type.Family.Either         Type.Family.List