haskus-utils-types 1.3.1 → 1.4

raw patch · 10 files changed

+544/−103 lines, 10 filesdep +doctestdep ~basePVP ok

version bump matches the API change (PVP)

Dependencies added: doctest

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• haskus-utils-types.cabal +19/−2
• src/lib/Haskus/Utils/Types.hs +9/−96
• src/lib/Haskus/Utils/Types/Bool.hs +226/−0
• src/lib/Haskus/Utils/Types/Constraint.hs +9/−0
• src/lib/Haskus/Utils/Types/Error.hs +38/−0
• src/lib/Haskus/Utils/Types/List.hs +42/−5
• src/lib/Haskus/Utils/Types/Nat.hs +124/−0
• src/lib/Haskus/Utils/Types/Proxy.hs +23/−0
• src/lib/Haskus/Utils/Types/Symbol.hs +28/−0
• src/tests/Main.hs +26/−0

@@ -1,6 +1,6 @@ name:                haskus-utils-types-version:             1.3.1-synopsis:            Haskus utility modules+version:             1.4+synopsis:            Haskus types utility modules license:             BSD3 license-file:        LICENSE author:              Sylvain Henry@@ -21,8 +21,14 @@ library   exposed-modules:     Haskus.Utils.Types+    Haskus.Utils.Types.Bool     Haskus.Utils.Types.List     Haskus.Utils.Types.Generics+    Haskus.Utils.Types.Proxy+    Haskus.Utils.Types.Nat+    Haskus.Utils.Types.Symbol+    Haskus.Utils.Types.Error+    Haskus.Utils.Types.Constraint    other-modules: @@ -33,3 +39,14 @@   ghc-options:          -Wall   default-language:     Haskell2010   hs-source-dirs:       src/lib++test-suite tests+   type:                exitcode-stdio-1.0+   main-is:             Main.hs+   hs-source-dirs:      src/tests+   ghc-options:         -Wall -threaded+   default-language:    Haskell2010++   build-depends:+         base+      ,  doctest                 >= 0.16

@@ -1,100 +1,13 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE CPP #-}---- We need this otherwise GHC chokes on the export of--- "type (*)"-#if MIN_VERSION_GLASGOW_HASKELL (8,6,0,0)-{-# LANGUAGE NoStarIsType #-}-#endif---- | Common type functions+-- | Type-level utils module Haskus.Utils.Types-   ( Nat-   , Symbol-   , natValue-   , natValue'-   , symbolValue-   , KnownNat-   , KnownSymbol-   , CmpNat-   , CmpSymbol-   , type (<=?)-   , type (<=)-   , type (+)-   , type (-)-   , type (*)-   , type (^)-   , Assert-   , If-   , Modulo-   , Same-   , Proxy (..)-   , TypeError-   , ErrorMessage (..)+   ( module X    ) where -import GHC.TypeLits-import Data.Proxy---- | Get a Nat value-natValue :: forall (n :: Nat) a. (KnownNat n, Num a) => a-{-# INLINE natValue #-}-natValue = fromIntegral (natVal (Proxy :: Proxy n))---- | Get a Nat value-natValue' :: forall (n :: Nat). KnownNat n => Word-{-# INLINE natValue' #-}-natValue' = natValue @n---- | Get a Symbol value-symbolValue :: forall (s :: Symbol). (KnownSymbol s) => String-{-# INLINE symbolValue #-}-symbolValue = symbolVal (Proxy :: Proxy s)---- | If-then-else-type family If (c :: Bool) (t :: k) (e :: k) where-   If 'True  t e = t-   If 'False t e = e----- | Like: If cond t (TypeError msg)------ The difference is that the TypeError doesn't appear in the RHS of the type--- which leads to better error messages (see GHC #14771).------ For instance:---    type family F n where---       F n = If (n <=? 8) Int8 (TypeError (Text "ERROR"))------    type family G n where---       G n = Assert (n <=? 8) Int8 (Text "ERROR")------    If GHC cannot solve `F n ~ Word`, it shows: ERROR---    If GHC cannot solve `G n ~ Word`, it shows:---       can't match `Assert...` with `Word`----type family Assert (prop :: Bool) (val :: k) (msg :: ErrorMessage) where-   Assert 'True  val msg = val-   Assert 'False val msg = TypeError msg---- | Modulo-type family Modulo (a :: Nat) (b :: Nat) where-   Modulo a b = Modulo' (a <=? b) a b---- | Helper for Modulo-type family Modulo' c a b where-   Modulo' 'True  a b = a-   Modulo' 'False a b = Modulo' ((a-b) <=? b) (a-b) b---- | Type equality to Nat-type family Same a b :: Nat where-   Same a a = 1-   Same a b = 0+import Haskus.Utils.Types.Nat        as X+import Haskus.Utils.Types.Symbol     as X+import Haskus.Utils.Types.Error      as X+import Haskus.Utils.Types.Bool       as X+import Haskus.Utils.Types.List       as X+import Haskus.Utils.Types.Proxy      as X+import Haskus.Utils.Types.Constraint as X

@@ -0,0 +1,226 @@+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE AllowAmbiguousTypes #-}++-- | Type level booleans+module Haskus.Utils.Types.Bool+   ( If+   , NotB+   , OrB+   , AndB+   , XorB+   , KnownBool (..)+   -- * Generic+   , Not+   , And+   , Or+   , Xor+   , AndMany+   , OrMany+   , XorMany+   , AllFalse+   , AllTrue+   )+where++-- $setup+-- >>> :set -XDataKinds+-- >>> :set -XTypeApplications+-- >>> :set -XFlexibleContexts+-- >>> :set -XTypeFamilies+-- >>> import Haskus.Utils.Types+++-- | If-then-else+type family If (c :: Bool) (t :: k) (e :: k) where+   If 'True  t e = t+   If 'False t e = e+++-- | Type-level Bool known at compile time+class KnownBool a where+   -- | Get a bool value from a Bool at type level+   --+   -- >>> boolValue @'True+   -- True+   -- >>> boolValue @(AndB 'True 'False)+   -- False+   boolValue :: Bool++instance KnownBool 'True where+   {-# INLINE boolValue #-}+   boolValue = True++instance KnownBool 'False where+   {-# INLINE boolValue #-}+   boolValue = False+++-- | Boolean Not+--+-- >>> boolValue @(NotB 'True)+-- False+-- >>> boolValue @(NotB 'False)+-- True+type family NotB x where+   NotB 'True  = 'False+   NotB 'False = 'True++-- | Boolean And+--+-- >>> boolValue @(AndB 'True 'False)+-- False+-- >>> boolValue @(AndB 'True 'True)+-- True+type family AndB x y where+   AndB 'True 'True   = 'True+   AndB 'True 'False  = 'False+   AndB 'False 'True  = 'False+   AndB 'False 'False = 'False++-- | Boolean Or+--+-- >>> boolValue @(OrB 'True 'False)+-- True+-- >>> boolValue @(OrB 'False 'False)+-- False+type family OrB x y where+   OrB 'True 'True   = 'True+   OrB 'False 'True  = 'True+   OrB 'True 'False  = 'True+   OrB 'False 'False = 'False++-- | Boolean Xor+--+-- >>> boolValue @(XorB 'True 'False)+-- True+-- >>> boolValue @(XorB 'False 'False)+-- False+-- >>> boolValue @(XorB 'True 'True)+-- False+type family XorB x y where+   XorB 'True 'True   = 'False+   XorB 'False 'True  = 'True+   XorB 'True 'False  = 'True+   XorB 'False 'False = 'False++---------------------------------------+-- Generic+---------------------------------------++-- | Generic boolean Not+--+-- >>> natValue' @(Not 1 0 1 :: Nat)+-- 0+-- >>> natValue' @(Not 1 0 0 :: Nat)+-- 1+type family Not (t :: b) (f :: b) (x :: b) :: b where+   Not t f t = f+   Not t f f = t++-- | Generic boolean And+--+-- >>> natValue' @(And 1 0 1 0 :: Nat)+-- 0+-- >>> natValue' @(And 1 0 1 1 :: Nat)+-- 1+type family And (t :: b) (f :: b) (x :: b) (y :: b) :: b where+   And t f t t = t+   And t f t f = f+   And t f f t = f+   And t f f f = f++-- | Generic boolean Or+--+-- >>> natValue' @(Or 1 0 1 0 :: Nat)+-- 1+-- >>> natValue' @(Or 1 0 0 0 :: Nat)+-- 0+type family Or (t :: b) (f :: b) (x :: b) (y :: b) :: b where+   Or t f t t = t+   Or t f f t = t+   Or t f t f = t+   Or t f f f = f++-- | Generic boolean Xor+--+-- >>> natValue' @(Xor 1 0 1 0 :: Nat)+-- 1+-- >>> natValue' @(Xor 1 0 0 0 :: Nat)+-- 0+-- >>> natValue' @(Xor 1 0 1 1 :: Nat)+-- 0+type family Xor (t :: b) (f :: b) (x :: b) (y :: b) :: b where+   Xor t f t t = f+   Xor t f f t = t+   Xor t f t f = t+   Xor t f f f = f+++-- | Generic boolean And on a list+--+-- >>> natValue' @(AndMany 1 0 '[1,0,1] :: Nat)+-- 0+-- >>> natValue' @(AndMany 1 0 '[1,1,1] :: Nat)+-- 1+type family AndMany (t :: b) (f :: b) (xs :: [b]) :: b where+   AndMany t f '[t]      = t+   AndMany t f '[f]      = f+   AndMany t f (f ': xs) = f+   AndMany t f (t ': xs) = AndMany t f xs++-- | Generic boolean Or on a list+--+-- >>> natValue' @(OrMany 1 0 '[1,0,1] :: Nat)+-- 1+-- >>> natValue' @(OrMany 1 0 '[1,1,1] :: Nat)+-- 1+-- >>> natValue' @(OrMany 1 0 '[0,0,0] :: Nat)+-- 0+type family OrMany (t :: b) (f :: b) (xs :: [b]) :: b where+   OrMany t f '[t]      = t+   OrMany t f '[f]      = f+   OrMany t f (t ': xs) = t+   OrMany t f (f ': xs) = OrMany t f xs++-- | Generic boolean Xor on a list (i.e. check if there is a single true element+-- in the list)+--+-- >>> natValue' @(XorMany 1 0 '[0,0,1] :: Nat)+-- 1+-- >>> natValue' @(XorMany 1 0 '[1,0,1] :: Nat)+-- 0+-- >>> natValue' @(XorMany 1 0 '[0,0,0] :: Nat)+-- 0+type family XorMany (t :: b) (f :: b) (xs :: [b]) :: b where+   XorMany t f '[t]      = t+   XorMany t f '[f]      = f+   XorMany t f (t ': xs) = AllFalse t f xs+   XorMany t f (f ': xs) = XorMany t f xs++-- | Check if all the elements are false+--+-- >>> natValue' @(AllFalse 1 0 '[0,0,1] :: Nat)+-- 0+-- >>> natValue' @(AllFalse 1 0 '[0,0,0] :: Nat)+-- 1+type family AllFalse (t :: b) (f :: b) (xs :: [b]) :: b where+   AllFalse t f '[t]      = f+   AllFalse t f '[f]      = t+   AllFalse t f (t ': xs) = f+   AllFalse t f (f ': xs) = AllFalse t f xs++-- | Check if all the elements are true+--+-- >>> natValue' @(AllTrue 1 0 '[0,0,1] :: Nat)+-- 0+-- >>> natValue' @(AllTrue 1 0 '[1,1,1] :: Nat)+-- 1+type family AllTrue (t :: b) (f :: b) (xs :: [b]) :: b where+   AllTrue t f '[t]      = t+   AllTrue t f '[f]      = f+   AllTrue t f (f ': xs) = f+   AllTrue t f (t ': xs) = AllTrue t f xs

@@ -0,0 +1,9 @@+-- | Type-level Constraint+--+-- Use it with `ConstraintKinds` LANGUAGE pragma+module Haskus.Utils.Types.Constraint+   ( Constraint+   )+where++import GHC.Exts (Constraint)

@@ -0,0 +1,38 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE PolyKinds #-}++-- | Type-level Error+module Haskus.Utils.Types.Error+   ( TypeError+   , ErrorMessage (..)+   , Assert+   )+where++import GHC.TypeLits++-- | Like: If cond t (TypeError msg)+--+-- The difference is that the TypeError doesn't appear in the RHS of the type+-- which leads to better error messages (see GHC #14771).+--+-- For instance:+--    type family F n where+--       F n = If (n <=? 8) Int8 (TypeError (Text "ERROR"))+--+--    type family G n where+--       G n = Assert (n <=? 8) Int8 (Text "ERROR")+--+--    If GHC cannot solve `F n ~ Word`, it shows: ERROR+--    If GHC cannot solve `G n ~ Word`, it shows:+--       can't match `Assert...` with `Word`+--+type family Assert (prop :: Bool) (val :: k) (msg :: ErrorMessage) :: k where+   Assert 'True  val msg = val+   Assert 'False val msg = TypeError msg+

@@ -36,6 +36,8 @@    , ReplaceN    , ReplaceNS    -- * Set operations+   , Subset+   , SetEq    , CheckMember    , CheckMembers    , Union@@ -49,20 +51,25 @@    , IndexesOf    , MaybeIndexOf    , Index+   , Elem+   , MapElem    , Reverse    -- * Nat list    , Generate    -- * Others    , Map-   , Max+   , ListMax+   , ListMin    , Length    , Indexes    , MapTest    ) where -import Haskus.Utils.Types-import GHC.Exts (Constraint)+import Haskus.Utils.Types.Bool+import Haskus.Utils.Types.Error+import Haskus.Utils.Types.Nat+import Haskus.Utils.Types.Constraint  -- | Map a type function type family Map (f :: a -> k) (xs :: [a]) :: [k] where@@ -70,14 +77,23 @@    Map f (x ': xs) = f x ': Map f xs  -- | Get the max of a list of Nats-type family Max (xs :: [Nat]) where-   Max (x ': xs) = Max' x xs+type family ListMax (xs :: [Nat]) where+   ListMax (x ': xs) = Max' x xs  -- | Helper for Max type family Max' (x :: Nat) (xs :: [Nat]) where    Max' x '[]       = x    Max' x (a ': xs) = Max' (If (x <=? a) a x) xs +-- | Get the min of a list of Nats+type family ListMin (xs :: [Nat]) where+   ListMin (x ': xs) = Min' x xs++-- | Helper for Min+type family Min' (x :: Nat) (xs :: [Nat]) where+   Min' x '[]       = x+   Min' x (a ': xs) = Min' (If (x <=? a) x a) xs+ -- | Tail of a list type family Tail (xs :: [k]) :: [k] where    Tail (x ': xs) = xs@@ -286,6 +302,27 @@ type family Index (n :: Nat) (l :: [k]) :: k where    Index 0 (x ': xs) = x    Index n (x ': xs) = Index (n-1) xs++-- | List membership test+type family Elem (t :: b) (f :: b) (x :: k) (xs :: [k]) :: b where+   Elem t f x '[]       = f+   Elem t f x (x ': xs) = t+   Elem t f x (y ': xs) = Elem t f x xs++-- | MapElem t f xs ys = Map (\x -> Elem t f x ys) xs+type family MapElem (t :: b) (f :: b) (xs :: [a]) (ys :: [a]) :: [b] where+   MapElem t f '[]       ys = '[]+   MapElem t f (x ': xs) ys = Elem t f x ys ':  MapElem t f xs ys++-- | Subset test+type family Subset (t :: b) (f :: b) (xs :: [a]) (ys :: [a]) :: b where+   Subset t f '[] '[] = t+   Subset t f xs ys   = AndMany t f (MapElem t f xs ys)++-- | Set equality+type family SetEq (t :: b) (f :: b) (xs :: [a]) (ys :: [a]) :: b where+   SetEq t f xs ys = And t f (Subset t f xs ys)+                             (Subset t f ys xs)  -- | Union two lists type family Union (xs :: [k]) (ys :: [k]) :: [k] where

@@ -0,0 +1,124 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE CPP #-}++-- We need this otherwise GHC chokes on the export of+-- "type (*)"+#if MIN_VERSION_GLASGOW_HASKELL (8,6,0,0)+{-# LANGUAGE NoStarIsType #-}+#endif++-- | Type-level Nat+module Haskus.Utils.Types.Nat+   ( Nat+   , natValue+   , natValue'+   , KnownNat+   , SomeNat (..)+   , someNatVal+   , sameNat+   -- * Comparisons+   , CmpNat+   , type (<=?)+   , type (<=)+   , NatEq+   , NatNotEq+   , Max+   , Min+   , IsZero+   , IsNotZero+   -- * Operations+   , type (+)+   , type (-)+   , type (*)+   , type (^)+   , Mod+   , Log2+   , Div+   -- * Helpers+   , NatBitCount+   )+where++import GHC.TypeNats+import Haskus.Utils.Types.Bool+import Data.Proxy++-- $setup+-- >>> :set -XDataKinds+-- >>> :set -XTypeApplications+-- >>> :set -XFlexibleContexts+-- >>> :set -XTypeFamilies+-- >>> import Haskus.Utils.Types++-- | Get a Nat value+natValue :: forall (n :: Nat) a. (KnownNat n, Num a) => a+{-# INLINABLE natValue #-}+natValue = fromIntegral (natVal (Proxy :: Proxy n))++-- | Get a Nat value as a Word+natValue' :: forall (n :: Nat). KnownNat n => Word+{-# INLINABLE natValue' #-}+natValue' = natValue @n+++-- | Type equality to Nat+type family NatEq a b :: Nat where+   NatEq a a = 1+   NatEq a b = 0++-- | Type inequality to Nat+type family NatNotEq a b :: Nat where+   NatNotEq a a = 0+   NatNotEq a b = 1++-- | Max of two naturals+type family Max (a :: Nat) (b :: Nat) where+   Max a b = If (a <=? b) b a++-- | Min of two naturals+type family Min (a :: Nat) (b :: Nat) where+   Min a b = If (a <=? b) a b++-- | Number of bits (>= 1) required to store a Nat value+--+-- >>> natValue' @(NatBitCount 0)+-- 1+--+-- >>> natValue' @(NatBitCount 1)+-- 1+--+-- >>> natValue' @(NatBitCount 2)+-- 2+--+-- >>> natValue' @(NatBitCount 5)+-- 3+--+-- >>> natValue' @(NatBitCount 15)+-- 4+--+-- >>> natValue' @(NatBitCount 16)+-- 5+--+type family NatBitCount (n :: Nat) :: Nat where+   NatBitCount 0 = 1+   NatBitCount n = NatBitCount' (n+1) (Log2 (n+1))++type family NatBitCount' v log2 where+   NatBitCount' v log2 = log2 + NatNotEq v (2^log2)++-- | Return 1 if 0, and 0 otherwise+type family IsZero (n :: Nat) :: Nat where+   IsZero 0 = 1+   IsZero _ = 0++-- | Return 0 if 0, and 1 otherwise+type family IsNotZero (n :: Nat) :: Nat where+   IsNotZero 0 = 0+   IsNotZero _ = 1

@@ -0,0 +1,23 @@+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE MagicHash #-}++module Haskus.Utils.Types.Proxy+   ( module Data.Proxy+   , NatVal (..)+   , Proxy#+   )+where++import Data.Proxy+import Haskus.Utils.Types.Nat+import GHC.Exts (Proxy#)++-- | A natural value Proxy+data NatVal (t :: Nat) = NatVal++instance KnownNat t => Show (NatVal t) where+   show _ = show (natValue' @t)+

@@ -0,0 +1,28 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE PolyKinds #-}++-- | Type-level Symbol (i.e. string)+module Haskus.Utils.Types.Symbol+   ( Symbol+   , symbolValue+   , KnownSymbol+   , CmpSymbol+   , SomeSymbol (..)+   , sameSymbol+   , someSymbolVal+   )+where++import GHC.TypeLits+import Data.Proxy++--- | Get a Symbol value+symbolValue :: forall (s :: Symbol). (KnownSymbol s) => String+{-# INLINABLE symbolValue #-}+symbolValue = symbolVal (Proxy :: Proxy s)

@@ -0,0 +1,26 @@+{-# LANGUAGE LambdaCase #-}+import Test.DocTest++import Control.Exception+import System.Exit++main :: IO ()+main = wrapTests+   [ title "DOCTEST" $ doctest ["src/lib/"]+   ]++title :: String -> IO () -> IO ()+title s m = do+   putStrLn ""+   putStrLn (replicate 30 '=')+   putStrLn s+   putStrLn (replicate 30 '=')+   m++wrap :: IO () -> IO Bool+wrap m = (m >> return True) `catch` (\e -> return (e == ExitSuccess))++wrapTests :: [IO ()] -> IO ()+wrapTests ts = (and <$> traverse wrap ts) >>= \case+   True  -> title "SUMMARY" exitSuccess+   False -> title "SUMMARY" exitFailure