packages feed

typelevel 1.0.2 → 1.0.4

raw patch · 15 files changed

+463/−28 lines, 15 filesdep +prettydep +pretty-showsetup-changed

Dependencies added: pretty, pretty-show

Files

− Setup.hs 
@@ -1,2 +0,0 @@-import Distribution.Simple-main = defaultMain
src/Type/Bool.hs view
@@ -13,31 +13,45 @@  -- === Basic operations === +type family Not a where+  Not 'True  = 'False+  Not 'False = 'True+ type family And a b where-  And True True = True-  And a    b    = False+  And 'True 'True = 'True+  And a      b    = 'False  type family Or a b where-  Or True b    = True-  Or a    True = True-  Or a    b    = False+  Or 'True b     = 'True+  Or a     'True = 'True+  Or a     b     = 'False  type family Xor a b where-  Xor True True = False-  Xor True b    = True-  Xor a    True = True-  Xor a    b    = False+  Xor 'True 'True = 'False+  Xor 'True b     = 'True+  Xor a     'True = 'True+  Xor a     b     = 'False  type family If (cond :: Bool) (a :: k) (b :: k) :: k where-  If cond  a a = a-  If True  a b = a-  If False a b = b+  If cond   a a = a+  If 'True  a b = a+  If 'False a b = b  type family If' (cond :: Bool) (a :: Constraint) (b :: Constraint) :: Constraint where-  If' cond  a a = a-  If' True  a b = a-  If' False a b = b+  If'  cond  a a = a+  If' 'True  a b = a+  If' 'False a b = b -type family (:==) (a :: k) (b :: l) where-    a :== a = True-    a :== b = False+type family (a :: k) == (b :: l) where+    a == a = 'True+    a == b = 'False+++-- === Type level queries ===++class    KnownBool (b :: Bool) where boolVal :: Proxy b -> Bool+instance KnownBool True        where boolVal _ = True+instance KnownBool False       where boolVal _ = False+++
+ src/Type/Container.hs view
@@ -0,0 +1,40 @@+{-# LANGUAGE PolyKinds            #-}+{-# LANGUAGE UndecidableInstances #-}++module Type.Container where++import Prelude+import GHC.TypeLits+++type family In     (el :: ke) (cont :: k) :: Bool+type family Index2 (idx :: i) (cont :: c) :: el+type family Index  (el :: ke) (cont :: k) :: Maybe Nat+type family Append (el :: ke) (cont :: k) :: k+type family Insert (el :: ke) (cont :: k) :: k+type family Remove (el :: ke) (cont :: k) :: k+type family Empty             (cont :: k) :: Bool+type family Size              (cont :: k) :: Nat+type family Reverse           (cont :: k) :: k+--type family Head              (cont :: k) :: Maybe *++type family Unique            (cont :: k) :: k++type family Concat (a :: k) (b :: k) :: k++type family Diff  (c :: k) (c' :: k) :: k+type family Union (c :: k) (c' :: k) :: k++--infixr 6      :<>+--type family (a :: k) :<> (b :: k) where a :<> b = Concat a b++infixr 6      <>+type family (a :: k) <> (b :: k) where a <> b = Concat a b+++++--------------------------------++type family FromJust a where FromJust ('Just a) = a+type UnsafeIndex el cont = FromJust (Index el cont)
+ src/Type/Either.hs view
@@ -0,0 +1,16 @@+{-# LANGUAGE PolyKinds #-}++module Type.Either where++import Prelude+++type family IsLeft (a :: Either l r) :: Bool where IsLeft ('Left  l) = 'True+                                                   IsLeft ('Right r) = 'False++type family IsRight (a :: Either l r) :: Bool where IsRight ('Left  l) = 'False+                                                    IsRight ('Right r) = 'True+++type family FromRight (a :: Either l r) where FromRight ('Right r) = r+type family FromLeft  (a :: Either l r) where FromLeft  ('Left  l) = l
src/Type/List.hs view
@@ -5,6 +5,7 @@ {-# LANGUAGE TypeOperators        #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE PolyKinds            #-}+{-# LANGUAGE ScopedTypeVariables            #-}  module Type.List where @@ -13,16 +14,102 @@ import GHC.Exts (Constraint) import GHC.TypeLits import Type.Bool+import Type.Container+import qualified Type.Set as Set +-- === Wrappers ===++data Lst (l :: [k])++type family FromLst a where FromLst (Lst l) = l+ -- === Basic operations === -type family Removed    (el :: e) (cont :: c) :: l+type family Removed    (el :: e)    (cont :: c) :: l type family RemovedIdx (idx :: Nat) (cont :: c) :: l type family ElAt       (idx :: Nat) (cont :: c) :: l  -type instance Removed (el :: e) ((l ': ls) :: [e]) = If (el :== l) ls (l ': Removed el ls)+type instance Removed (el :: e) ((l ': ls) :: [e]) = If (el == l) ls (l ': Removed el ls)  -type instance RemovedIdx idx (l ': ls) = If (idx :== 0) ls (l ': RemovedIdx (idx - 1) ls)+type instance RemovedIdx idx (l ': ls) = If (idx == 0) ls (l ': RemovedIdx (idx - 1) ls) -type instance ElAt idx (l ': ls) = If (idx :== 0) l (ElAt (idx - 1) ls)+type instance ElAt idx (l ': ls) = If (idx == 0) l (ElAt (idx - 1) ls)+++type instance In a (l ': ls) = If (a == l) True (In a ls)+type instance In a '[]       = False+++type family SuccMaybe (m :: Maybe Nat) where SuccMaybe (Just n) = Just (n + 1)+                                             SuccMaybe Nothing  = Nothing++type instance Index a (l ': ls) = If (a == l) (Just 0) (SuccMaybe (Index a ls))+type instance Index a '[]       = (Nothing :: Maybe Nat)+++data Recursive a++type instance Index a (Recursive (l ': ls)) = If (a == l) (Just 0) (SuccMaybe (Index a (Recursive ls)))+type instance Index a (Recursive '[]      ) = (Nothing :: Maybe Nat)+++--type family Index2 (idx :: i) (cont :: c) :: el++type instance Index2 n (a ': as) = If (n == 0) a (Index2 (n - 1) as)+++type instance Empty '[]       = 'True+type instance Empty (a ': as) = 'False+++type instance Append a '[]       = '[a]+type instance Append a (l ': ls) = l ': Append a ls+++type instance Concat (lst :: [k]) ('[]       :: [k]) = lst+type instance Concat (lst :: [k]) ((l ': ls) :: [k]) = Concat (Append l lst) ls+++type instance Remove a '[] = '[]+type instance Remove a (l ': ls) = If (a == l) ls (l ': Remove a ls)+++type instance Diff l '[]       = l+type instance Diff l (e ': es) = Diff (Remove e l) es++type instance Size '[]       = 0+type instance Size (a ': as) = 1 + Size as++type family Head lst where+    Head '[]       = 'Nothing+    Head (a ': as) = 'Just a++type family Head' lst where Head' (a ': as) = a++--type instance Unique (lst :: [k]) = Set.ToList (Set.AsSet lst)++-- FIXME[WD]: The following is just an fix for using Unique. +--            Due to lack of time this ugly fix has no background - probably some PolyKinded problem.+type family UniqueFix lst where UniqueFix '[] = '[]+                                UniqueFix lst = Unique lst+type instance Unique (lst :: [k]) = Set.ToList (Set.AsSet lst)++type instance Reverse (lst :: [k]) = Reverse' lst '[]++type family Reverse' lst lst' where+    Reverse' '[] lst = lst+    Reverse' (l ': ls) lst = Reverse' ls (l ': lst)+++type family Take (n :: Nat) lst where+	Take 0 lst       = '[]+	Take n (l ': ls) = l ': Take (n - 1) ls++--type instance Index (a :: *) (Recursive ((l ': ls) ::  [*] )) = If (a == l) (Just 0) (SuccMaybe (Index a (Recursive ls)))+--type instance Index (a :: *) (Recursive ((l ': ls) :: [[*]])) = If (Index a l == 'Nothing) (SuccMaybe (Index a (Recursive ls))) ('Just 0)+--type instance Index a '[]                                     = 'Nothing+++--type instance RecIndex a ((l ': ls) :: [[*]]) = If (RecIndex a l == 'Nothing) (SuccMaybe (RecIndex a ls)) (Just 0)+
+ src/Type/Map.hs view
@@ -0,0 +1,9 @@+{-# LANGUAGE PolyKinds #-}++module Type.Map where++data Map k v = Map [(k,v)]++type family MapLookup (k :: kk) (m :: Map kk kv) :: kv where+    MapLookup k ('Map ( '(k, v) ': ms )) = v+    MapLookup k ('Map ( '(l, v) ': ms )) = MapLookup k ('Map ms)
+ src/Type/Maybe.hs view
@@ -0,0 +1,14 @@+{-# LANGUAGE PolyKinds #-}++module Type.Maybe where++import Prelude++type family IsJust a where IsJust ('Just a) = 'True+                           IsJust a         = 'False+++type family CatMaybes (lst :: [Maybe k]) :: [k] where+    CatMaybes '[]              = '[]+    CatMaybes ('Just a  ': ms) = a ': CatMaybes ms+    CatMaybes ('Nothing ': ms) =      CatMaybes ms
+ src/Type/Operators.hs view
@@ -0,0 +1,25 @@++{-# LANGUAGE DeriveDataTypeable   #-}+{-# LANGUAGE EmptyDataDecls       #-}+{-# LANGUAGE TypeFamilies         #-}+{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE PolyKinds            #-}++module Type.Operators where++import Data.Typeable+import Prelude+import GHC.Exts (Constraint)+import GHC.TypeLits+import Type.Bool+import Type.Container+import Type.Wrapped++++infixr 0 $+type f $ a = f a++infixl 1 &+type a & f = f a
+ src/Type/Promotion.hs view
@@ -0,0 +1,43 @@+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE PolyKinds #-}++module Type.Promotion where++import Prelude++import Data.Typeable+import GHC.TypeLits+++-- === Promotion classes ===++class Known (t :: k) (val :: *) where typeVal :: Proxy t -> val+--type family TypeVal (t :: k) :: *+--type Known' t = Known t (TypeVal t)++++-- === Basic instances ===++-- Nat+instance (Num i, KnownNat t) => Known (t :: Nat) i where typeVal = fromIntegral . natVal++-- Bool+--type instance TypeVal (k :: Bool) = Bool+instance val ~ Bool => Known True  val where typeVal _ = True+instance val ~ Bool => Known False val where typeVal _ = False++-- Maybe a+--type instance TypeVal ('Just a) = Maybe (TypeVal a)+instance val ~ Maybe a              => Known 'Nothing  val where typeVal _ = Nothing+instance (val ~ Maybe a, Known t a) => Known ('Just t) val where typeVal _ = Just $ typeVal (Proxy :: Proxy t)++-- Either l r+instance (val ~ Either l r, Known t l) => Known ('Left  t) val where typeVal _ = Left  $ typeVal (Proxy :: Proxy t)+instance (val ~ Either l r, Known t r) => Known ('Right t) val where typeVal _ = Right $ typeVal (Proxy :: Proxy t)++-- Lists+instance Known ('[]) [a] where typeVal _ = []+instance (Known t a, Known ts [a]) => Known (t ': ts) [a] where typeVal _ = typeVal (Proxy :: Proxy t) : typeVal (Proxy :: Proxy ts)
+ src/Type/Sequence.hs view
@@ -0,0 +1,29 @@+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE UndecidableInstances #-}++module Type.Sequence where++import Prelude+import GHC.TypeLits++type family Succ (a :: k) :: k++type instance Succ (a :: Nat) = a + 1+++type family Empty :: k++type instance Empty = '[]+++type family Zero :: k++type instance Zero = 0++++type family Range (begin :: k) (end :: k) :: [k] where+    Range b b = Empty+    Range b e = b ': Range (Succ b) e++type family Enumerate end where Enumerate end = Range Zero end -- Implemented as TF because #11375
+ src/Type/Set.hs view
@@ -0,0 +1,50 @@++{-# LANGUAGE DeriveDataTypeable   #-}+{-# LANGUAGE EmptyDataDecls       #-}+{-# LANGUAGE TypeFamilies         #-}+{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE PolyKinds            #-}++module Type.Set where++import Data.Typeable+import Prelude+import GHC.Exts (Constraint)+import GHC.TypeLits+import Type.Bool+import Type.Container+import Type.Wrapped+import Type.Operators+++-- === Declarations ===++data Set (a :: [k])++type instance Unwrapped (Set a) = a+++-- === Conversions ===++type family AsSet  (a :: k)+type family AsSet' (a :: k)++type instance AsSet (lst :: [k]) = AsSet' (Reverse lst)+type instance AsSet' '[]         = Set '[]+type instance AsSet' (l ': ls)   = Insert l (AsSet' ls)++type family ToList s where ToList (Set s) = s++++-- === Operations ===+++type instance Insert a (Set '[])       = Set '[a]+type instance Insert a (Set (s ': ss)) = Set $ If (a == s) (s ': ss) (s ': Unwrapped (Insert a (Set ss)))++type instance Concat (Set set) (Set '[]) = Set set+type instance Concat (Set set) (Set (s ': ss)) = If (s `In` set) (Concat (Set set) (Set ss)) (Concat (Insert s (Set set)) (Set ss))++type instance Index a (Set s) = Index a s
+ src/Type/Show.hs view
@@ -0,0 +1,58 @@+{-# LANGUAGE ScopedTypeVariables  #-}+{-# LANGUAGE PolyKinds            #-}+{-# LANGUAGE ScopedTypeVariables  #-}+{-# LANGUAGE UndecidableInstances #-}++module Type.Show where++import Prelude+import Data.Typeable+import Data.Monoid+import GHC.TypeLits+import Text.Show.Pretty (ppValue, parseValue)+import Text.PrettyPrint (Doc, text)+import GHC.Exts         (Constraint)++--showType :: Typeable a => a -> String+--showType (a :: a) = showProxyType (Proxy :: Proxy a)++--showProxyType :: Typeable (Proxy a) => Proxy a -> String+--showProxyType = clear . drop 6 . show . typeOf where+--    clear = \case ('(':s)     -> init  s+--                  ('*':' ':s) -> clear s -- PolyKinded Proxies are shown as "Proxy *"+--                  s           -> s+++class TypeShow a where showType :: Proxy (a :: k) -> String++printType :: TypeShow a => Proxy a -> IO ()+printType = putStrLn . showType++ppPrintType :: TypeShow a => Proxy a -> IO ()+ppPrintType = putStrLn . ppShowType++ppShowType :: TypeShow a => Proxy a -> String+ppShowType = show . ppTypeDoc++ppTypeDoc :: TypeShow a => Proxy a -> Doc+ppTypeDoc a = case parseValue txt of+            Just v  -> ppValue v+            Nothing -> text txt+  where txt = showType a++++-- === Basic Instances === --++instance KnownNat n               => TypeShow (n :: Nat) where showType _ = show $ natVal (Proxy :: Proxy n)+instance ListElemsShow a          => TypeShow (a :: [k]) where showType _ = "[" <> showListElems (Proxy :: Proxy a) <> "]"+instance (TypeShow a, TypeShow b) => TypeShow '(a,b)     where showType _ = "(" <> showType (Proxy :: Proxy a) <> ", " <> showType (Proxy :: Proxy b) <> ")"+++-- === List Helpers === --++class                                                           ListElemsShow a         where showListElems :: Proxy a -> String+instance {-# OVERLAPPABLE #-}                                   ListElemsShow '[]       where showListElems _ = ""+instance {-# OVERLAPPABLE #-}  TypeShow a                    => ListElemsShow '[a]      where showListElems _ = showType (Proxy :: Proxy a)+instance {-# OVERLAPPABLE #-} (TypeShow a, ListElemsShow as) => ListElemsShow (a ': as) where showListElems _ = showType (Proxy :: Proxy a) <> ", " <> showListElems (Proxy :: Proxy as)+
+ src/Type/Wrapped.hs view
@@ -0,0 +1,20 @@++{-# LANGUAGE DeriveDataTypeable   #-}+{-# LANGUAGE EmptyDataDecls       #-}+{-# LANGUAGE TypeFamilies         #-}+{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE PolyKinds            #-}++module Type.Wrapped where++import Data.Typeable+import Prelude+import GHC.Exts (Constraint)+import GHC.TypeLits+import Type.Bool+import Type.Container++-- === Basic operations ===++type family Unwrapped (a :: k) :: l
+ src/Type/Zip.hs view
@@ -0,0 +1,12 @@+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE UndecidableInstances #-}++module Type.Zip where+++type family Zip lst lst' where Zip lst lst' = ZipWith '(,) lst lst' -- Implemented as TF because #11375++type family ZipWith f lst lst' where+    ZipWith f '[]       lst       = '[]+    ZipWith f lst       '[]       = '[]+    ZipWith f (l ': ls) (n ': ns) = f l n ': ZipWith f ls ns
typelevel.cabal view
@@ -1,5 +1,11 @@+---------------------------------------------------+-- This is a generated cabal configuration file. --+-- DO NOT EDIT!                                  --+-- Use gencabal instead.                         --+---------------------------------------------------+ name:                typelevel-version:             1.0.2+version:             1.0.4 synopsis:            Useful type level operations (type families and related operators). -- description:          license:             Apache-2.0@@ -45,8 +51,22 @@                       ViewPatterns                       TypeFamilies   -  exposed-modules:    Constraint.Container.Homo -                    , Type.Bool-                    , Type.List+  Exposed-modules: +        Constraint.Container.Homo,+        Type.Bool,+        Type.Container,+        Type.Either,+        Type.List,+        Type.Map,+        Type.Maybe,+        Type.Operators,+        Type.Promotion,+        Type.Sequence,+        Type.Set,+        Type.Show,+        Type.Wrapped,+        Type.Zip    build-depends:      base >=4.6 && <4.9+                    , pretty-show+                    , pretty