fcf-containers 0.8.1 → 0.8.2

raw patch · 20 files changed

+812/−127 lines, 20 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +16/−0
• README.md +29/−3
• fcf-containers.cabal +11/−3
• flake.nix +3/−0
• src/Fcf/Alg/Morphism.hs +8/−18
• src/Fcf/Alg/Other.hs +2/−11
• src/Fcf/Alg/Sort.hs +2/−11
• src/Fcf/Alg/Symbol.hs +20/−21
• src/Fcf/Alg/Tree.hs +6/−8
• src/Fcf/Data/OldText.hs +2/−1
• src/Fcf/Data/Reflect.hs +51/−21
• src/Fcf/Data/Text.hs +1/−0
• test/Test/Alg.hs +14/−2
• test/Test/Alg/Morphism.hs +85/−0
• test/Test/Alg/Nat.hs +66/−0
• test/Test/Alg/Other.hs +54/−0
• test/Test/Alg/Sort.hs +56/−0
• test/Test/Alg/Symbol.hs +157/−0
• test/Test/Alg/Tree.hs +129/−0
• test/Test/Data/Reflect.hs +100/−28

@@ -1,4 +1,20 @@ +# 0.8.2++Thank you again to Skyfold (Martin P.)++- Deprecation warning for the KnownNats class and its instances: the KnownVal+  can be used instead.+- Instances to IntMap, Map and Set to convert directly from '[a] or '[ '(key,val) ]+- The ErrorMessage instance for KnownVal to show information about types +- Add KnownVal instance for typeable types, this can be used as Show for+  the types presented at the kind level. +- Fix the Test.Alg test description+- Remove doc-tests from all Fcf.Alg modules and write the corresponding test modules+- Some cleaning+- Add depracation and warning pragmas to text modules.++ # 0.8.1  20230410

@@ -56,18 +56,38 @@ cabal test  ``` -The doc-tests both document and work as main testing mechanism for this lib. +If you are flakes user, `nix develop -c zsh` (or without that `-c zsh`) works as well. +The doc-tests both document and work partly as testing mechanism for this lib. Please +do note that we are moving away from the doc-tests and building the testing modules +under `test` directory.+ If you don't use nix, `cabal install fcf-containers` should be enough. This package has almost as good number of dependencies as the first-class-families.   ## Example ++### Test cases as examples+ The   [test directory](https://github.com/gspia/fcf-containers/blob/master/test)-contains a lot of useful examples.+contains a lot of useful examples.  There you will find out, how to apply most+of the methods: examples that only work on "compile time", and examples on how+to get the results from type level calculations to value level (see the Reflect+test module and the `fromType` method applications, also in some other testing+modules). ++### Three example programs calculating something++These are a bit larger examples, but not yet too large: somewhat convenient small +module size.  Idea was to take an algorithm, and convert it to a type-level +computation, or in some other way give an example of methods that this library+provides.++ See [Orbits.hs](https://github.com/gspia/fcf-containers/blob/master/examples/Orbits.hs).  It shows how to solve a real problem, what PRAGMAs are probably needed etc.@@ -76,12 +96,18 @@ cabal run orbits  ``` -There is also another example that show how to use MapC, see+There is also another Advent of Code problem, see the Carbcombat file.+++To see, how to use MapC, take a look at [Haiku.hs](https://github.com/gspia/fcf-containers/blob/master/examples/Haiku.hs)  ``` cabal run haiku  ```+++### Other example material  Please, do take a look of the notes made for the Helsinki Haskell meetup on 11th January 2023

@@ -7,7 +7,7 @@     contents of containers-package and show how these can be used. Everything is     based on the ideas given in the first-class-families -package. Homepage:            https://github.com/gspia/fcf-containers-Version:             0.8.1+Version:             0.8.2 Build-type:          Simple Author:              gspia Maintainer:          iahogsp@gmail.com@@ -96,11 +96,17 @@   default-language:    Haskell2010   other-modules:       Test.Alg                      , Test.Alg.List+                     , Test.Alg.Morphism+                     , Test.Alg.Nat+                     , Test.Alg.Other+                     , Test.Alg.Sort+                     , Test.Alg.Symbol+                     , Test.Alg.Tree+                     , Test.Control+                     , Test.Control.Monad                      , Test.Data                      , Test.Data.Reflect                      , Test.Data.Set-                     , Test.Control-                     , Test.Control.Monad   build-depends:       base     , first-class-families@@ -108,6 +114,8 @@     , hspec     , containers     , text+--  ghc-options:+--      -freduction-depth=0  test-suite fcf-doctest   type:                exitcode-stdio-1.0

@@ -13,6 +13,8 @@       # filter = import nix-filter { };        ghcVersion = "925";+      # ghcVersion = "92";+      # ghcVersion = "902";        src = nix-filter.lib {         root = ./.;@@ -65,5 +67,6 @@         library = fcf-containers;         # packages.x86_64-linux.default = ;         devShell.x86_64-linux = shell;+        inherit pkgs;       }; }

@@ -32,15 +32,6 @@  -------------------------------------------------------------------------------- --- For the doctests:---- $setup--- >>> import qualified GHC.TypeLits as TL--- >>> import           Fcf.Alg.List--- >>> import           Fcf.Data.Nat----------------------------------------------------------------------------------- -- | Structure that 'Cata' can fold and that is a result structure of 'Ana'. newtype Fix f = Fix (f (Fix f)) @@ -68,15 +59,15 @@ -- -- === __Example__ ----- >>> data NToOneCoA :: CoAlgebra (ListF Nat) Nat--- >>> :{+-- > data NToOneCoA :: CoAlgebra (ListF Nat) Nat+-- > :{ --   type instance Eval (NToOneCoA b) = --     If (Eval (b < 1) ) --         'NilF --         ('ConsF b ( b TL.- 1)) -- :} ----- >>> :kind! Eval (Ana NToOneCoA 3)+-- > :kind! Eval (Ana NToOneCoA 3) -- Eval (Ana NToOneCoA 3) :: Fix (ListF TL.Natural) -- = 'Fix ('ConsF 3 ('Fix ('ConsF 2 ('Fix ('ConsF 1 ('Fix 'NilF)))))) data Ana :: CoAlgebra f a -> a -> Exp (Fix f)@@ -89,15 +80,15 @@ -- -- === __Example__ ----- >>> data NToOneCoA :: CoAlgebra (ListF Nat) Nat--- >>> :{+-- > data NToOneCoA :: CoAlgebra (ListF Nat) Nat+-- > :{ --   type instance Eval (NToOneCoA b) = --     If (Eval (b < 1) ) --         'NilF --         ('ConsF b ( b TL.- 1)) -- :} ----- >>> :kind! Eval (Hylo SumAlg NToOneCoA 5)+-- > :kind! Eval (Hylo SumAlg NToOneCoA 5) -- Eval (Hylo SumAlg NToOneCoA 5) :: TL.Natural -- = 15 data Hylo :: Algebra f a -> CoAlgebra f b -> b -> Exp a@@ -183,7 +174,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (First ((+) 1) '(3,"a"))+-- > :kind! Eval (First ((+) 1) '(3,"a")) -- Eval (First ((+) 1) '(3,"a")) :: (TL.Natural, TL.Symbol) -- = '(4, "a") data First :: (a -> Exp b) -> f a c -> Exp (f b c)@@ -199,7 +190,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (Second ((+) 1) '("a",3))+-- > :kind! Eval (Second ((+) 1) '("a",3)) -- Eval (Second ((+) 1) '("a",3)) :: (TL.Symbol, TL.Natural) -- = '("a", 4) data Second :: (c -> Exp d) -> f a c -> Exp (f a d)@@ -210,4 +201,3 @@ -- Either type instance Eval (Second f ('Left a)) = 'Left a type instance Eval (Second f ('Right b)) = 'Right (f @@ b)-

@@ -26,19 +26,11 @@  -------------------------------------------------------------------------------- --- For the doctests:---- $setup--- >>> import           GHC.Types--- >>> import qualified GHC.TypeLits as TL----------------------------------------------------------------------------------- -- | Helper. -- -- === __Example__ ----- >>> :kind! Eval (PairMaybeToMaybePair '( 'Just "txt", 'Just 1))+-- > :kind! Eval (PairMaybeToMaybePair '( 'Just "txt", 'Just 1)) -- Eval (PairMaybeToMaybePair '( 'Just "txt", 'Just 1)) :: Maybe --                                                           (Symbol, TL.Natural) -- = 'Just '("txt", 1)@@ -52,9 +44,8 @@ -- -- === __Example__ ----- >>> :kind! Eval (Id "id")+-- > :kind! Eval (Id "id") -- Eval (Id "id") :: Symbol -- = "id" data Id :: a -> Exp a type instance Eval (Id a) = a-

@@ -36,14 +36,6 @@  -------------------------------------------------------------------------------- --- For the doctests:---- $setup--- >>> import qualified Fcf.Data.Nat as N ( type (<) )--- >>> import qualified Fcf.Alg.Symbol as S ( type (<) )----------------------------------------------------------------------------------- -- helper for the ListCmp data ListCmpFnd :: [Ordering] -> Exp Ordering type instance Eval (ListCmpFnd '[]) = 'EQ@@ -106,11 +98,11 @@ -- -- __Example__ ----- >>> :kind! Eval (Qsort (N.<) '[5,3,1,9,4,6,3])+-- > :kind! Eval (Qsort (N.<) '[5,3,1,9,4,6,3]) -- Eval (Qsort (N.<) '[5,3,1,9,4,6,3]) :: [TL.Natural] -- = '[1, 3, 3, 4, 5, 6, 9] ----- >>> :kind! Eval (Qsort (S.<) '[ "bb", "e", "a", "e", "d" ])+-- > :kind! Eval (Qsort (S.<) '[ "bb", "e", "a", "e", "d" ]) -- Eval (Qsort (S.<) '[ "bb", "e", "a", "e", "d" ]) :: [Symbol] -- = '["a", "bb", "d", "e", "e"] data Qsort :: (a -> a -> Exp Bool) -> [a] -> Exp [a]@@ -122,4 +114,3 @@ -- Nat-list. Sorting would work without PartCmp. data PartCmp :: (a -> a -> Exp Bool) -> CoAlgebra (BTreeF a) [a]  type instance Eval (PartCmp cmp coalg) = Eval (PartHlp (Flip cmp) coalg)-

@@ -71,7 +71,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (Append "hmm" " ok")+-- > :kind! Eval (Append "hmm" " ok") -- Eval (Append "hmm" " ok") :: Symbol -- = "hmm ok" data Append :: Symbol -> Symbol -> Exp Symbol@@ -82,15 +82,15 @@ -- -- === __Example__ ----- >>> :kind! Eval (Intercalate "+" '["aa", "bb", "cc"])+-- > :kind! Eval (Intercalate "+" '["aa", "bb", "cc"]) -- Eval (Intercalate "+" '["aa", "bb", "cc"]) :: Symbol -- = "aa+bb+cc" ----- >>> :kind! Eval (Intercalate "+" '["aa"])+-- > :kind! Eval (Intercalate "+" '["aa"]) -- Eval (Intercalate "+" '["aa"]) :: Symbol -- = "aa" ----- >>> :kind! Eval (Intercalate "+" '[])+-- > :kind! Eval (Intercalate "+" '[]) -- Eval (Intercalate "+" '[]) :: Symbol -- = "" data Intercalate :: Symbol -> [Symbol] -> Exp Symbol@@ -107,11 +107,11 @@ -- -- === __Example__ ----- >>> :kind! Eval (IsSpace "a")+-- > :kind! Eval (IsSpace "a") -- Eval (IsSpace "a") :: Bool -- = 'False ----- >>> :kind! Eval (IsSpace " ")+-- > :kind! Eval (IsSpace " ") -- Eval (IsSpace " ") :: Bool -- = 'True data IsSpace :: Symbol -> Exp Bool@@ -122,11 +122,11 @@ -- -- === __Example__ ----- >>> :kind! Eval (IsNewLine "a")+-- > :kind! Eval (IsNewLine "a") -- Eval (IsNewLine "a") :: Bool -- = 'False ----- >>> :kind! Eval (IsNewLine "\n")+-- > :kind! Eval (IsNewLine "\n") -- Eval (IsNewLine "\n") :: Bool -- = 'True data IsNewLine :: Symbol -> Exp Bool@@ -137,11 +137,11 @@ -- -- === __Example__ ----- >>> :kind! Eval (IsTab "a")+-- > :kind! Eval (IsTab "a") -- Eval (IsTab "a") :: Bool -- = 'False ----- >>> :kind! Eval (IsTab "\t")+-- > :kind! Eval (IsTab "\t") -- Eval (IsTab "\t") :: Bool -- = 'True data IsTab :: Symbol -> Exp Bool@@ -152,11 +152,11 @@ -- -- === __Example__ ----- >>> :kind! Eval (IsSpaceDelim "a")+-- > :kind! Eval (IsSpaceDelim "a") -- Eval (IsSpaceDelim "a") :: Bool -- = 'False ----- >>> :kind! Eval (IsSpaceDelim "\n")+-- > :kind! Eval (IsSpaceDelim "\n") -- Eval (IsSpaceDelim "\n") :: Bool -- = 'True data IsSpaceDelim :: Symbol -> Exp Bool@@ -168,11 +168,11 @@ -- -- === __Example__ ----- >>> :kind! Eval (IsDigit "3")+-- > :kind! Eval (IsDigit "3") -- Eval (IsDigit "3") :: Bool -- = 'True ----- >>> :kind! Eval (IsDigit "a")+-- > :kind! Eval (IsDigit "a") -- Eval (IsDigit "a") :: Bool -- = 'False data IsDigit :: Symbol -> Exp Bool@@ -189,7 +189,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (SymbolOrd "a" "b")+-- > :kind! Eval (SymbolOrd "a" "b") -- Eval (SymbolOrd "a" "b") :: Ordering -- = 'LT data SymbolOrd :: Symbol -> Symbol -> Exp Ordering@@ -199,10 +199,9 @@ -- -- === __Example__ ----- >>> :kind! Eval ("b" <= "a")+-- > :kind! Eval ("b" <= "a") -- Eval ("b" <= "a") :: Bool -- = 'False--- data (<=) :: Symbol -> Symbol -> Exp Bool type instance Eval ((<=) a b) =     Eval (Eval (TyEq (TL.CmpSymbol a b) 'LT) || Eval (TyEq (TL.CmpSymbol a b) 'EQ))@@ -211,7 +210,7 @@ -- -- === __Example__ ----- >>> :kind! Eval ("b" >= "a")+-- > :kind! Eval ("b" >= "a") -- Eval ("b" >= "a") :: Bool -- = 'True data (>=) :: Symbol -> Symbol -> Exp Bool@@ -222,7 +221,7 @@ -- -- === __Example__ ----- >>> :kind! Eval ("a" < "b")+-- > :kind! Eval ("a" < "b") -- Eval ("a" < "b") :: Bool -- = 'True data (<) :: Symbol -> Symbol -> Exp Bool@@ -232,7 +231,7 @@ -- -- === __Example__ ----- >>> :kind! Eval ("b" > "a")+-- > :kind! Eval ("b" > "a") -- Eval ("b" > "a") :: Bool -- = 'True data (>) :: Symbol -> Symbol -> Exp Bool@@ -242,7 +241,7 @@ -- -- === __Example__ ----- >>> :kind! Eval ("b" == "a")+-- > :kind! Eval ("b" == "a") -- Eval ("b" == "a") :: Bool -- = 'False data (==) :: Symbol -> Symbol -> Exp Bool

@@ -75,15 +75,15 @@ -- Size is defined as @ Cata CountNodesAlg =<< TreeToFix tr @ -- and can be used with the following. ----- >>> data BuildNode :: Nat -> Exp (Nat,[Nat])--- >>> :{+-- > data BuildNode :: Nat -> Exp (Nat,[Nat])+-- > :{ --   type instance Eval (BuildNode x) = --       If (Eval ((2 TL.* x TL.+ 1) >= 8)) --           '(x, '[]) --           '(x, '[ 2 TL.* x, (2 TL.* x) TL.+ 1 ]) -- :} ----- >>> :kind! Eval (Size =<< UnfoldTree BuildNode 1)+-- > :kind! Eval (Size =<< UnfoldTree BuildNode 1) -- Eval (Size =<< UnfoldTree BuildNode 1) :: TL.Natural -- = 7 data Size :: Tree a -> Exp Nat@@ -114,7 +114,7 @@ -- -- __Example__ ----- >>> :kind! Eval (FibHylo 10)+-- > :kind! Eval (FibHylo 10) -- Eval (FibHylo 10) :: TL.Natural -- = 55 data FibHylo :: Nat -> Exp Nat@@ -147,7 +147,7 @@ -- -- __Example__ ----- >>> :kind! Eval (Sizes =<< Ana BuildNodeCoA 1)+-- > :kind! Eval (Sizes =<< Ana BuildNodeCoA 1) -- Eval (Sizes =<< Ana BuildNodeCoA 1) :: Fix --                                          (AnnF (TreeF TL.Natural) TL.Natural) -- = 'Fix@@ -208,10 +208,8 @@ -- -- __Example__ ----- >>> :kind! Eval (FibHisto 100)+-- > :kind! Eval (FibHisto 100) -- Eval (FibHisto 100) :: TL.Natural -- = 354224848179261915075 data FibHisto :: Nat -> Exp Nat type instance Eval (FibHisto n) = Eval (Histo FibAlgebra =<< NatToFix n)--

@@ -6,7 +6,7 @@ {-# OPTIONS_GHC -Werror=incomplete-patterns #-}  {-|-Module      : Fcf.Data.Text+Module      : Fcf.Data.OldText Description : Type-level Text data structure with methods Copyright   : (c) gspia 2020- License     : BSD@@ -25,6 +25,7 @@ --------------------------------------------------------------------------------  module Fcf.Data.OldText+    {-# DEPRECATED "Use Fcf.Data.NewText instead" #-}     ( Text (..)      -- * Creation

@@ -31,7 +31,8 @@ import           GHC.TypeLits (Nat, Symbol, KnownNat, KnownSymbol) import           Data.String (fromString, IsString) import           Data.Proxy--- import qualified Data.Map.Strict as MS+import           Data.Typeable (Typeable, typeRep)+import           Data.Kind (Type) import qualified Data.Map as DM import qualified Data.IntMap.Strict as IMS import qualified Data.Set as S@@ -39,7 +40,6 @@ -- #endif import qualified Data.Tree as T --- import qualified Fcf.Core as C (Eval) import qualified Fcf.Data.MapC as MC import qualified Fcf.Data.NatMap as NM import qualified Fcf.Data.Set as FS@@ -50,15 +50,6 @@  -------------------------------------------------------------------------------- --- For the doctests:---- $setup--- >>> import qualified GHC.TypeLits as TL--- >>> import           Fcf.Data.Nat------------------------------------------------------------------------------------ -- | Reflect a list of Nats -- -- Note that you may also use the KnownVal methods given below.@@ -68,16 +59,18 @@ -- -- === __Example__ ----- >>> :{+-- > :{ -- afun :: forall n. (n ~ '[1,2,3,4]) => [Int] -- afun = natVals @n Proxy -- :} ----- >>> afun+-- > afun -- [1,2,3,4] class KnownNats (ns :: [Nat]) where   natVals :: Proxy ns -> [Int] +{-# DEPRECATED KnownNats "Replaced with KnownVal" #-}+ instance KnownNats '[] where   natVals _ = [] @@ -95,27 +88,36 @@  instance KnownVal Bool 'True where fromType _ = True instance KnownVal Bool 'False where fromType _ = False+instance KnownVal () '() where fromType _ = () -instance (IsString str, KnownSymbol s) => KnownVal str (s :: Symbol )where+instance (IsString str, KnownSymbol s) => KnownVal str (s :: Symbol) where     fromType _ = fromString $ TL.symbolVal (Proxy @s) +#if __GLASGOW_HASKELL__ >= 920+instance (TL.KnownChar c) => KnownVal Char c where+    fromType _ = TL.charVal (Proxy @c)+#endif++instance (IsString str, Typeable typ) => KnownVal str (typ :: Type) where+    fromType = fromString . show . typeRep+ #if __GLASGOW_HASKELL__ >= 902  -- | Text instance. -- -- === __Example__ ----- >>> import qualified Data.Text as Txt--- >>> :{+-- > import qualified Data.Text as Txt+-- > :{ -- afun :: forall r. (r ~ 'FTxt.Text "hmm") => Txt.Text -- afun = fromType (Proxy @r) -- :} ----- >>> afun+-- > afun -- "hmm" instance (IsString str, KnownSymbol sym) => KnownVal str ('FTxt.Text sym)   where-    fromType _ = fromString $ fromType $ Proxy @sym +    fromType _ = fromType @str (Proxy @sym)   #endif @@ -126,14 +128,14 @@ instance KnownVal [a] '[] where     fromType _ = [] -instance (KnownVal typ x, KnownVal [typ] xs) => KnownVal [typ] (x ': xs) where+instance (KnownVal val x, KnownVal [val] xs) => KnownVal [val] (x ': xs) where     fromType _ = fromType (Proxy @x) : fromType (Proxy @xs)  --------------------------------------------------------------------------------  -- Trees ---instance (KnownVal typ k, KnownVal (T.Forest typ) trees) => KnownVal (T.Tree typ) ('FT.Node k trees)+instance (KnownVal val k, KnownVal (T.Forest val) trees) => KnownVal (T.Tree val) ('FT.Node k trees)   where     fromType _ = T.Node (fromType (Proxy @k)) (fromType (Proxy @trees)) @@ -145,6 +147,10 @@   where     fromType _ = IMS.fromList (fromType (Proxy @pairs)) +instance (KnownVal [(Int,val)] pairs) => KnownVal (IMS.IntMap val) (pairs :: [(Nat, val')])+  where+    fromType _ = IMS.fromList (fromType (Proxy @pairs))+ --------------------------------------------------------------------------------  -- Maps@@ -153,13 +159,21 @@   where     fromType _ = DM.fromList (fromType (Proxy @pairs)) +instance (Ord key, KnownVal [(key,val)] pairs) => KnownVal (DM.Map key val) (pairs :: [(key',val')])+  where+    fromType _ = DM.fromList (fromType (Proxy @pairs))+ --------------------------------------------------------------------------------  -- Set -instance (Ord typ, KnownVal [typ] kind) => KnownVal (S.Set typ) ('FS.Set kind)+instance (Ord val, KnownVal [val] kind) => KnownVal (S.Set val) ('FS.Set kind)   where     fromType _ = S.fromList (fromType (Proxy @kind))++instance (Ord val, KnownVal [val] kind) => KnownVal (S.Set val) (kind :: [kind'])+  where+    fromType _ = S.fromList (fromType (Proxy @kind))   -------------------------------------------------------------------------------- @@ -196,3 +210,19 @@  instance (KnownVal a1 a, KnownVal b1 b, KnownVal c1 c, KnownVal d1 d, KnownVal e1 e) => KnownVal (a1,b1,c1,d1,e1) '(a,b,c,d,e) where     fromType _ = (fromType @a1 (Proxy @a), fromType @b1 (Proxy @b), fromType @c1 (Proxy @c), fromType @d1 (Proxy @d), fromType @e1 (Proxy @e))++--------------------------------------------------------------------------------++-- ErrorMessage from GHC.TypeLits++instance (IsString str, KnownSymbol sym) => KnownVal str ('TL.Text sym) where+  fromType _ = fromType @str (Proxy @sym)++instance (IsString str, Typeable typ) => KnownVal str ('TL.ShowType typ) where+  fromType _ = fromString $ show $ typeRep (Proxy @typ)++instance (IsString str, KnownVal str err1, KnownVal str err2, Semigroup str) => KnownVal str (err1 'TL.:<>: err2) where+  fromType _ = fromType (Proxy @err1) <> fromType (Proxy @err2)++instance (IsString str, KnownVal str err1, KnownVal str err2, Semigroup str) => KnownVal str (err1 'TL.:$$: err2) where+  fromType _ = fromType (Proxy @err1) <> fromString "\n" <> fromType (Proxy @err2)

@@ -28,6 +28,7 @@ --------------------------------------------------------------------------------  module Fcf.Data.Text+    {-# WARNING "This still uses the OldText implementaion, which will be replaced with NewText implementation." #-}     ( Text (..)      -- * Creation

@@ -1,10 +1,22 @@  module Test.Alg where -import           Test.Alg.List as L (spec)+import           Test.Alg.List     as L (spec)+import           Test.Alg.Morphism as M (spec)+import           Test.Alg.Nat      as N (spec)+import           Test.Alg.Other    as O (spec)+import           Test.Alg.Sort     as So (spec)+import           Test.Alg.Symbol   as Sy (spec)+import           Test.Alg.Tree     as T (spec) import           Test.Hspec (describe, Spec)  spec :: Spec-spec = describe "Data"  +spec = describe "Alg" $ do   L.spec+  M.spec+  N.spec+  O.spec+  So.spec+  Sy.spec+  T.spec 

@@ -0,0 +1,85 @@+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE TypeApplications       #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeInType             #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# OPTIONS_GHC -Wall                       #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{- +In this module, we test mainly Fcf.Alg.Morphism module. In couple of +places, we use the "spec" and Reflect. ++Many of the tests are such that if the answer is not correct, the+whole test module refuses to compile.  Please do try to change some +of the values to see. ++Note that in a way, the spec tests are not needed. If testing just +the type level behaviour, the module would refuse to compile if +test is not ok (and thus, guard the quality earlier than what the +test framework can do).  ++Anyhow, as these also work as examples, it is probably ok to have different +ways of reaching the results. (E.g. to see, how to get the type level +values to value level.)++-}+module Test.Alg.Morphism where++import qualified GHC.TypeLits as TL++import           Data.Proxy+import           Data.Type.Equality ((:~:)(Refl))+import           Test.Hspec (describe, it, shouldBe, Spec)++import           Fcf.Core (Eval)+import           Fcf.Utils (If)+import           Fcf.Alg.List+import           Fcf.Alg.Morphism+import           Fcf.Data.Nat+import           Fcf.Data.Reflect (fromType)++--------------------------------------------------------------------------------++-- For the Ana and Hylo tests made below.+data NToOneCoA :: CoAlgebra (ListF Nat) Nat+type instance Eval (NToOneCoA b) =+  If (Eval (b < 1) )+      'NilF+      ('ConsF b ( b TL.- 1))+++-- This module won't compile, if the Refl doesn't give the correct answer.+--+-- > :kind! Eval (Ana NToOneCoA 3)+-- Eval (Ana NToOneCoA 3) :: Fix (ListF TL.Natural)+-- = 'Fix ('ConsF 3 ('Fix ('ConsF 2 ('Fix ('ConsF 1 ('Fix 'NilF))))))+_ = Refl :: Eval (Ana NToOneCoA 3)+  :~: 'Fix ('ConsF 3 ('Fix ('ConsF 2 ('Fix ('ConsF 1 ('Fix 'NilF))))))++-- > :kind! Eval (Second ((+) 1) '("a",3))+-- Eval (Second ((+) 1) '("a",3)) :: (TL.Symbol, TL.Natural)+-- = '("a", 4)+_ = Refl :: Eval (Second ((+) 1) '("a",3))+  :~: '("a", 4)+++-- > :kind! Eval (Hylo SumAlg NToOneCoA 5)+-- Eval (Hylo SumAlg NToOneCoA 5) :: TL.Natural+-- = 15++-- > :kind! Eval (First ((+) 1) '(3,"a"))+-- Eval (First ((+) 1) '(3,"a")) :: (TL.Natural, TL.Symbol)+-- = '(4, "a")++spec :: Spec+spec = describe "Morphism" $ do+  it "Hylo SumAlg" $ do+    let test :: forall r. (r ~ Eval (Hylo SumAlg NToOneCoA 5)) => Int+        test = fromType (Proxy @r)+    test `shouldBe` 15+  it "First" $ do+    let test :: forall r. (r ~ Eval (First ((+) 1) '(3,"a"))) => (Int, String)+        test = fromType (Proxy @r)+    test `shouldBe` (4,"a")

@@ -0,0 +1,66 @@+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE TypeApplications       #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeInType             #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# OPTIONS_GHC -Wall                       #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{- +In this module, we test mainly Fcf.Alg.Nat module. In couple of +places, we use the "spec" and Reflect. ++Many of the tests are such that if the answer is not correct, the+whole test module refuses to compile.  Please do try to change some +of the values to see. ++Note that in a way, the spec tests are not needed. If testing just +the type level behaviour, the module would refuse to compile if +test is not ok (and thus, guard the quality earlier than what the +test framework can do).  ++Anyhow, as these also work as examples, it is probably ok to have different +ways of reaching the results. (E.g. to see, how to get the type level +values to value level.)++-}++module Test.Alg.Nat where++import           Data.Proxy+import           Data.Type.Equality ((:~:)(Refl))+import           Test.Hspec (describe, it, shouldBe, Spec)++import           Fcf.Core (Eval)+import           Fcf.Alg.Nat+import           Fcf.Data.Reflect (fromType)++-- > :kind! Eval (2 == 2)+-- Eval (2 == 2) :: Bool+-- = 'True+_ = Refl :: Eval (2==2) :~: 'True++-- > :kind! Eval (2 == 3)+-- Eval (2 == 3) :: Bool+-- = 'False+_ = Refl :: Eval (2==3) :~: 'False+++-- > :kind! Eval (2 /= 2)+-- Eval (2 /= 2) :: Bool+-- = 'False+--+-- > :kind! Eval (2 /= 3)+-- Eval (2 /= 3) :: Bool+-- = 'True+spec :: Spec+spec = describe "Nat" $ do+  it "In-equality, false" $ do+    let test :: forall r. (r ~ Eval (2 /= 2)) => Bool+        test = fromType (Proxy @r)+    test `shouldBe` False+  it "In-equality, true" $ do+    let test :: forall r. (r ~ Eval (2 /= 3)) => Bool+        test = fromType (Proxy @r)+    test `shouldBe` True

@@ -0,0 +1,54 @@+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE TypeApplications       #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeInType             #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# OPTIONS_GHC -Wall                       #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{- +In this module, we test mainly Fcf.Alg.Other module. In couple of +places, we use the "spec" and Reflect. ++Many of the tests are such that if the answer is not correct, the+whole test module refuses to compile.  Please do try to change some +of the values to see. ++Note that in a way, the spec tests are not needed. If testing just +the type level behaviour, the module would refuse to compile if +test is not ok (and thus, guard the quality earlier than what the +test framework can do).  ++Anyhow, as these also work as examples, it is probably ok to have different +ways of reaching the results. (E.g. to see, how to get the type level +values to value level.)++-}+module Test.Alg.Other where++import           Data.Proxy+import           Data.Type.Equality ((:~:)(Refl))+import           Test.Hspec (describe, it, shouldBe, Spec)++import           Fcf.Core (Eval)+import           Fcf.Alg.Other+import           Fcf.Data.Reflect (fromType)++-- > :kind! Eval (PairMaybeToMaybePair '( 'Just "txt", 'Just 1))+-- Eval (PairMaybeToMaybePair '( 'Just "txt", 'Just 1)) :: Maybe+--                                                           (Symbol, TL.Natural)+-- = 'Just '("txt", 1)+_ = Refl :: Eval (PairMaybeToMaybePair '( 'Just "txt", 'Just 1)) +  :~: 'Just '("txt", 1)+++-- > :kind! Eval (Id "id")+-- Eval (Id "id") :: Symbol+-- = "id"+spec :: Spec+spec = describe "Other" $ do+  it "Id" $ do+    let test :: forall r. (r ~ Eval (Id "id")) => String+        test = fromType (Proxy @r)+    test `shouldBe` "id"

@@ -0,0 +1,56 @@+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE TypeApplications       #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeInType             #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# OPTIONS_GHC -Wall                       #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{- +In this module, we test mainly Fcf.Alg.Sort module. In couple of +places, we use the "spec" and Reflect. ++Many of the tests are such that if the answer is not correct, the+whole test module refuses to compile.  Please do try to change some +of the values to see. ++Note that in a way, the spec tests are not needed. If testing just +the type level behaviour, the module would refuse to compile if +test is not ok (and thus, guard the quality earlier than what the +test framework can do).  ++Anyhow, as these also work as examples, it is probably ok to have different +ways of reaching the results. (E.g. to see, how to get the type level +values to value level.)++-}++module Test.Alg.Sort where++import           Data.Proxy+import           Data.Type.Equality ((:~:)(Refl))+import           Test.Hspec (describe, it, shouldBe, Spec)++import           Fcf.Core (Eval)+import           Fcf.Alg.Sort+import qualified Fcf.Alg.Symbol as S ( type (<) )+import qualified Fcf.Data.Nat as N ( type (<) )+import           Fcf.Data.Reflect (fromType)++-- > :kind! Eval (Qsort (N.<) '[5,3,1,9,4,6,3])+-- Eval (Qsort (N.<) '[5,3,1,9,4,6,3]) :: [TL.Natural]+-- = '[1, 3, 3, 4, 5, 6, 9]+spec :: Spec+spec = describe "Sort" $ do+  it "QSort (<)" $ do+    let test :: forall r. (r ~ Eval (Qsort (N.<) '[5,3,1,9,4,6,3])) => [Int]+        test = fromType (Proxy @r)+    test `shouldBe` [1, 3, 3, 4, 5, 6, 9]++-- > :kind! Eval (Qsort (S.<) '[ "bb", "e", "a", "e", "d" ])+-- Eval (Qsort (S.<) '[ "bb", "e", "a", "e", "d" ]) :: [Symbol]+-- = '["a", "bb", "d", "e", "e"]+_ = Refl :: Eval (Qsort (S.<) '[ "bb", "e", "a", "e", "d" ])+  :~: '["a", "bb", "d", "e", "e"]+

@@ -0,0 +1,157 @@+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE TypeApplications       #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeInType             #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# OPTIONS_GHC -Wall                       #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{- +In this module, we test mainly Fcf.Alg.Symbol module. In couple of +places, we use the "spec" and Reflect. ++Many of the tests are such that if the answer is not correct, the+whole test module refuses to compile.  Please do try to change some +of the values to see. ++Note that in a way, the spec tests are not needed. If testing just +the type level behaviour, the module would refuse to compile if +test is not ok (and thus, guard the quality earlier than what the +test framework can do).  ++Anyhow, as these also work as examples, it is probably ok to have different +ways of reaching the results. (E.g. to see, how to get the type level +values to value level.)++-}++module Test.Alg.Symbol where++import           Data.Proxy+import           Data.Type.Equality ((:~:)(Refl))+import           Test.Hspec (describe, it, shouldBe, Spec)++import           Fcf.Core (Eval)+import           Fcf.Alg.Symbol+import           Fcf.Data.Reflect (fromType)++-- > :kind! Eval (Append "hmm" " ok")+-- Eval (Append "hmm" " ok") :: Symbol+-- = "hmm ok"+_ = Refl :: Eval (Append "hmm" " ok") :~: "hmm ok"++-- > :kind! Eval (Intercalate "+" '["aa", "bb", "cc"])+-- Eval (Intercalate "+" '["aa", "bb", "cc"]) :: Symbol+-- = "aa+bb+cc"+_ = Refl :: Eval (Intercalate "+" '["aa", "bb", "cc"]) :~: "aa+bb+cc"++-- > :kind! Eval (Intercalate "+" '["aa"])+-- Eval (Intercalate "+" '["aa"]) :: Symbol+-- = "aa"+_ = Refl :: Eval (Intercalate "+" '["aa"]) :~: "aa"++-- > :kind! Eval (Intercalate "+" '[])+-- Eval (Intercalate "+" '[]) :: Symbol+-- = ""+_ = Refl :: Eval (Intercalate "+" '[]) :~: ""++-- > :kind! Eval (IsSpace "a")+-- Eval (IsSpace "a") :: Bool+-- = 'False+_ = Refl :: Eval (IsSpace "a") :~: 'False+--+-- > :kind! Eval (IsSpace " ")+-- Eval (IsSpace " ") :: Bool+-- = 'True+_ = Refl :: Eval (IsSpace " ") :~: 'True++-- > :kind! Eval (IsNewLine "a")+-- Eval (IsNewLine "a") :: Bool+-- = 'False+_ = Refl :: Eval (IsNewLine "a") :~: 'False++-- > :kind! Eval (IsNewLine "\n")+-- Eval (IsNewLine "\n") :: Bool+-- = 'True+_ = Refl :: Eval (IsNewLine "\n") :~: 'True++-- > :kind! Eval (IsTab "a")+-- Eval (IsTab "a") :: Bool+-- = 'False+_ = Refl :: Eval (IsTab "a") :~: 'False+--+-- > :kind! Eval (IsTab "\t")+-- Eval (IsTab "\t") :: Bool+-- = 'True+_ = Refl :: Eval (IsTab "\t") :~: 'True++-- > :kind! Eval (IsSpaceDelim "a")+-- Eval (IsSpaceDelim "a") :: Bool+-- = 'False+_ = Refl :: Eval (IsSpaceDelim "a") :~: 'False+--+-- > :kind! Eval (IsSpaceDelim "\n")+-- Eval (IsSpaceDelim "\n") :: Bool+-- = 'True+_ = Refl :: Eval (IsSpaceDelim "\n") :~: 'True++-- > :kind! Eval (IsDigit "3")+-- Eval (IsDigit "3") :: Bool+-- = 'True+_ = Refl :: Eval (IsDigit "3") :~: 'True+--+-- > :kind! Eval (IsDigit "a")+-- Eval (IsDigit "a") :: Bool+-- = 'False+_ = Refl :: Eval (IsDigit "a") :~: 'False++-- > :kind! Eval (SymbolOrd "a" "b")+-- Eval (SymbolOrd "a" "b") :: Ordering+-- = 'LT+_ = Refl :: Eval (SymbolOrd "a" "b") :~: 'LT++--------------------------------------------------------------------------------++-- > :kind! Eval ("b" <= "a")+-- Eval ("b" <= "a") :: Bool+-- = 'False+--+-- > :kind! Eval ("b" >= "a")+-- Eval ("b" >= "a") :: Bool+-- = 'True+--+-- > :kind! Eval ("a" < "b")+-- Eval ("a" < "b") :: Bool+-- = 'True+--+-- > :kind! Eval ("b" > "a")+-- Eval ("b" > "a") :: Bool+-- = 'True+--+-- > :kind! Eval ("b" == "a")+-- Eval ("b" == "a") :: Bool+-- = 'False+spec :: Spec+spec = describe "Symbol" $ do+  it "<=" $ do+    let test :: forall r. (r ~ Eval ("b" <= "a")) => Bool+        test = fromType (Proxy @r)+    test `shouldBe` False+  it ">=" $ do+    let test :: forall r. (r ~ Eval ("b" >= "a")) => Bool+        test = fromType (Proxy @r)+    test `shouldBe` True+  it "<" $ do+    let test :: forall r. (r ~ Eval ("b" < "a")) => Bool+        test = fromType (Proxy @r)+    test `shouldBe` False+  it ">" $ do+    let test :: forall r. (r ~ Eval ("b" > "a")) => Bool+        test = fromType (Proxy @r)+    test `shouldBe` True+  it "==" $ do+    let test :: forall r. (r ~ Eval ("b" == "a")) => Bool+        test = fromType (Proxy @r)+    test `shouldBe` False+    

@@ -0,0 +1,129 @@+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE TypeApplications       #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeInType             #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# OPTIONS_GHC -Wall                       #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{- +In this module, we test mainly Fcf.Alg.Tree module. In couple of +places, we use the "spec" and Reflect. ++Many of the tests are such that if the answer is not correct, the+whole test module refuses to compile.  Please do try to change some +of the values to see. ++Note that in a way, the spec tests are not needed. If testing just +the type level behaviour, the module would refuse to compile if +test is not ok (and thus, guard the quality earlier than what the +test framework can do).  ++Anyhow, as these also work as examples, it is probably ok to have different +ways of reaching the results. (E.g. to see, how to get the type level +values to value level.)++-}++module Test.Alg.Tree where++import qualified GHC.TypeLits as TL++import           Data.Proxy+import           Data.Type.Equality ((:~:)(Refl))+import           Test.Hspec (describe, it, shouldBe, Spec)++import           Fcf.Data.Nat++import           Fcf.Alg.Morphism +import           Fcf.Alg.Tree+import           Fcf.Combinators (type (=<<))+import           Fcf.Core (Eval, Exp)+import           Fcf.Utils (If)+import           Fcf.Data.Reflect (fromType)+import           Fcf.Data.Tree++data BuildNode :: Nat -> Exp (Nat,[Nat])+type instance Eval (BuildNode x) =+    If (Eval ((2 TL.* x TL.+ 1) >= 8))+        '(x, '[])+        '(x, '[ 2 TL.* x, (2 TL.* x) TL.+ 1 ])++-- > :kind! Eval (Size =<< UnfoldTree BuildNode 1)+-- Eval (Size =<< UnfoldTree BuildNode 1) :: TL.Natural+-- = 7+_ = Refl :: Eval (Size =<< UnfoldTree BuildNode 1) :~: 7+++-- :kind! Eval (Ana BuildNodeCoA 1)+-- :kind! Eval (Hylo CountNodesAlg BuildNodeCoA 1)+++-- > :kind! Eval (Sizes =<< Ana BuildNodeCoA 1)+-- Eval (Sizes =<< Ana BuildNodeCoA 1) :: Fix+--                                          (AnnF (TreeF TL.Natural) TL.Natural)+-- = 'Fix+--     ('AnnF+--        '( 'NodeF+--             1+--             '[ 'Fix+--                  ('AnnF+--                     '( 'NodeF+--                          2+--                          '[ 'Fix ('AnnF '( 'NodeF 4 '[], 1)),+--                             'Fix ('AnnF '( 'NodeF 5 '[], 1))],+--                        3)),+--                'Fix+--                  ('AnnF+--                     '( 'NodeF+--                          3+--                          '[ 'Fix ('AnnF '( 'NodeF 6 '[], 1)),+--                             'Fix ('AnnF '( 'NodeF 7 '[], 1))],+--                        3))],+--           7))+_ = Refl :: Eval (Sizes =<< Ana BuildNodeCoA 1)+  :~: 'Fix+    ('AnnF+       '( 'NodeF+            1+            '[ 'Fix+                 ('AnnF+                    '( 'NodeF+                         2+                         '[ 'Fix ('AnnF '( 'NodeF 4 '[], 1)),+                            'Fix ('AnnF '( 'NodeF 5 '[], 1))],+                       3)),+               'Fix+                 ('AnnF+                    '( 'NodeF+                         3+                         '[ 'Fix ('AnnF '( 'NodeF 6 '[], 1)),+                            'Fix ('AnnF '( 'NodeF 7 '[], 1))],+                       3))],+          7))++-- Turning this off, because of the slowness. In practice, this would+-- also require turning on ghc-options (-freduction-depth=0). +-- Please, do try on ghci.+-- > :kind! Eval (FibHisto 100)+-- Eval (FibHisto 100) :: TL.Natural+-- = 354224848179261915075+-- _ = Refl :: Eval (FibHisto 100) :~: 354224848179261915075++-- > :kind! Eval (FibHylo 10)+-- Eval (FibHylo 10) :: TL.Natural+-- = 55+spec :: Spec+spec = describe "Tree" $ do+  it "FibHisto" $ do+    let test :: forall r. (r ~ Eval (FibHylo 10)) => Int+        test = fromType (Proxy @r)+    test `shouldBe` 55+  -- The following is very slow and would require turning on ghc-options+  -- (-freduction-depth=0).  +  -- it "FibHisto" $ do+  --   let test :: forall r. (r ~ Eval (FibHisto 100)) => Integer+  --       test = fromType (Proxy @r)+  --   test `shouldBe` 354224848179261915075+

@@ -14,9 +14,8 @@ import qualified Data.Map as DM import qualified Data.Set as DS import qualified Data.Tree as DT-#if __GLASGOW_HASKELL__ >= 902 import qualified Data.Text as DTxt-#endif+import qualified GHC.TypeLits as TL import           Data.Proxy import           Test.Hspec (describe, it, shouldBe, Spec) @@ -34,11 +33,13 @@  spec :: Spec spec = describe "Reflect" $ do+  specTrees   specMaybe   specEither   specMaybeEither   specStructures-  specTrees+  specShowTypeable+  specErrorMessage    specBool :: Spec specBool = describe "Bool" $ do@@ -123,31 +124,73 @@  specStructures :: Spec specStructures = describe "Maps and other structures" $ do-  it "NatMap" $ do-    let test :: forall r. (r ~ Eval (-                  FNM.Insert 3 "hih" =<< FNM.FromList '[ '(1,"haa"), '(2,"hoo")]-                )) -             => IM.IntMap String-        test = fromType (Proxy @r)-    test -      `shouldBe` -      IM.fromList [ (3, "hih"), (1, "haa"), (2, "hoo")]-  it "Map" $ do-    let test :: forall r. (r ~ Eval (-                  FNMC.Insert 3 "hih" =<< FNMC.FromList '[ '(1,"haa"), '(2,"hoo")]-                )) -             => DM.Map Int String-        test = fromType (Proxy @r)-    test -      `shouldBe` -      DM.fromList [ (3, "hih"), (1, "haa"), (2, "hoo")]-  it "Set" $ do-    let test :: forall r. (r ~ Eval (FS.FromList '[5, 9, 1, 8, 3, 5])) -             => DS.Set Int-        test = fromType (Proxy @r)-    test -      `shouldBe` -      DS.fromList [1, 3, 5, 8, 9]+  describe "[]" $ do+    it "[]" $ do+      let test :: forall r. (r ~ '[]) => [()]+          test = fromType (Proxy @r)+      test `shouldBe` []+    it "[(Bool,Int)]" $ do+      let test :: forall r. (r ~ '[ '( 'True,5), '( 'False,6)]) => [(Bool,Int)]+          test = fromType (Proxy @r)+      test `shouldBe` [(True,5),(False,6)]+  describe "IntMap" $ do+#if __GLASGOW_HASKELL__ >= 920+    it "IntMap char, from '[ '(Nat,Char) ]" $ do+      let test :: forall r. (r ~ '[ '(1,'H'), '(2,'e'), '(5,'o'), '(3,'b'), '(4,'l'), '(3,'l')]) => IM.IntMap Char+          test = fromType (Proxy @r)+      test `shouldBe` IM.fromList [(1,'H'),(2,'e'),(5,'o'),(4,'l'),(3,'l')]+#endif+    it "IntMap String, from NatMap" $ do+      let test :: forall r. (r ~ Eval (FNM.FromList '[ '(1,"H"), '(4,"b"), '(2,"e"), '(5,"o"), '(4,"l"), '(3,"l")])) => IM.IntMap String+          test = fromType (Proxy @r)+      test `shouldBe` IM.fromList [(2,"e"),(1,"H"),(4,"l"),(3,"l"),(5,"o")]+    it "IntMap String, with insert" $ do+      let test :: forall r. (r ~ Eval (+                    FNM.Insert 3 "hih" =<< FNM.FromList '[ '(1,"haa"), '(2,"hoo")]+                  )) +              => IM.IntMap String+          test = fromType (Proxy @r)+      test +        `shouldBe` +        IM.fromList [ (3, "hih"), (1, "haa"), (2, "hoo")]+  describe "Map" $ do+#if __GLASGOW_HASKELL__ >= 920+    it "Map Int char, from '[ '(Nat,Char) ]" $ do+      let test :: forall r. (r ~ '[ '(1,'H'), '(2,'e'), '(5,'o'), '(4,'l'), '(3,'b'), '(3,'l')]) => DM.Map Int Char+          test = fromType (Proxy @r)+      test `shouldBe` DM.fromList [(1,'H'),(2,'e'),(5,'o'),(4,'l'),(3,'l')]+#endif+    it "Map Int String, from MapC" $ do+      let test :: forall r. (r ~ Eval (FNMC.FromList '[ '(1,"H"), '(2,"e"), '(3,"c"), '(5,"o"), '(4,"l"), '(3,"l")])) => DM.Map Int String+          test = fromType (Proxy @r)+      test `shouldBe` DM.fromList [(2,"e"),(1,"H"),(4,"l"),(3,"l"),(5,"o")]+    it "Map Int String, with insert" $ do+      let test :: forall r. (r ~ Eval (+                    FNMC.Insert 3 "hih" =<< FNMC.FromList '[ '(1,"haa"), '(2,"hoo")]+                  )) +              => DM.Map Int String+          test = fromType (Proxy @r)+      test +        `shouldBe` +        DM.fromList [ (3, "hih"), (1, "haa"), (2, "hoo")]+  describe "Set" $ do+#if __GLASGOW_HASKELL__ >= 920+    it "Set char, from '[Char]" $ do+      let test :: forall r. (r ~ '[ 'H','e','o','l','l' ]) => DS.Set Char+          test = fromType (Proxy @r)+      test `shouldBe` DS.fromList ['H','e','o','l','l']+#endif+    it "Set String, from Set" $ do+      let test :: forall r. (r ~ Eval (FS.FromList '["H","e","o","l","l"])) => DS.Set String+          test = fromType (Proxy @r)+      test `shouldBe` DS.fromList ["e","H","l","l","o"]+    it "Set Int" $ do+      let test :: forall r. (r ~ Eval (FS.FromList '[5, 9, 1, 8, 3, 5])) +              => DS.Set Int+          test = fromType (Proxy @r)+      test +        `shouldBe` +        DS.fromList [1, 3, 5, 8, 9] #if __GLASGOW_HASKELL__ >= 902   it "text" $ do     let test :: forall r. (r ~ 'FTxt.Text "trial") => DTxt.Text@@ -254,3 +297,32 @@           [DT.Node (Right "six") []           ]         ]++specShowTypeable :: Spec+specShowTypeable = describe "Show Type represented at the Kind level" $ do+  it "Show Int" $ do+    fromType @String (Proxy @Int)+      `shouldBe`+      "Int"+  it "Show Set of Types" $ do+    let test :: forall r. (r ~ Eval (FS.FromList '[Int, Maybe String, (), [Integer], IO ()])) +             => DS.Set String+        test = fromType (Proxy @r)+    test +      `shouldBe` +      DS.fromList ["Int", "Maybe [Char]", "()", "[Integer]", "IO ()"]++specErrorMessage :: Spec+specErrorMessage = describe "show GHC.TypeLits.ErrorMessage" $ do+  it "text error" $ do+    (fromType @DTxt.Text $ Proxy @('TL.Text "I am error"))+      `shouldBe`+      DTxt.pack "I am error"+  it "ShowType 'True" $ do+    (fromType @DTxt.Text $ Proxy @('TL.ShowType '()))+      `shouldBe`+      DTxt.pack "'()"+  it "with Kinds" $ do+    (fromType @DTxt.Text $ Proxy @('TL.Text "Kind: " 'TL.:<>: 'TL.ShowType 'True 'TL.:$$: 'TL.Text "Type: " 'TL.:<>: 'TL.ShowType Bool))+      `shouldBe`+      DTxt.pack "Kind: 'True\nType: Bool"