fcf-containers 0.8.0 → 0.8.1

raw patch · 19 files changed

+1210/−429 lines, 19 filesdep +hspecdep −mtlPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: hspec

Dependencies removed: mtl

API changes (from Hackage documentation)

Files

• CHANGELOG.md +15/−0
• README.md +6/−1
• fcf-containers.cabal +9/−4
• flake.lock +44/−0
• flake.nix +69/−0
• shell.nix +0/−9
• src/Fcf/Alg/List.hs +16/−22
• src/Fcf/Control/Monad.hs +149/−106
• src/Fcf/Data/Reflect.hs +66/−172
• src/Fcf/Data/Set.hs +30/−38
• src/Fcf/Data/Tuple.hs +17/−0
• test/Test/Alg.hs +10/−0
• test/Test/Alg/List.hs +171/−0
• test/Test/Control.hs +9/−0
• test/Test/Control/Monad.hs +140/−0
• test/Test/Data.hs +7/−2
• test/Test/Data/Reflect.hs +215/−58
• test/Test/Data/Set.hs +221/−0
• test/test.hs +16/−17

@@ -1,4 +1,19 @@ +# 0.8.1++20230410++Thank you to Skyfold (Martin P.)++- Generalized KnownVal instances+- Initialized the HSpec use and test directory organization+- Added flake definitions+- Updated stack version (not tested with stack)+- Removed shell.nix+- Fcf.Data.Set doctests removed and replaced with Test.Data.Set+- Fcf.Alg.List doctests removed and replaced with Test.Alg.List++ # 0.8.0  20230226

@@ -64,6 +64,10 @@  ## Example +The  +[test directory](https://github.com/gspia/fcf-containers/blob/master/test)+contains a lot of useful examples.+ 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.@@ -174,6 +178,7 @@  Source also contains a lot of examples, see [fcf-containers](https://github.com/gspia/fcf-containers/tree/master/src/Fcf).-+The examples will be left near the code, even thou the doctest runs will be +removed and replaced with real tests at the test-directory.  Happy :kinding!

@@ -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.0+Version:             0.8.1 Build-type:          Simple Author:              gspia Maintainer:          iahogsp@gmail.com@@ -15,7 +15,7 @@ License-file:        LICENSE Category:            Other Copyright:           gspia (c) 2020--Extra-source-files:  README.md, TODO.md, CHANGELOG.md, default.nix, shell.nix+Extra-source-files:  README.md, TODO.md, CHANGELOG.md, default.nix, flake.nix, flake.lock Tested-With:         GHC ==9.2.4 || ==9.0.2 || ==8.10.7  @@ -47,7 +47,6 @@                    , containers                    , first-class-families >= 0.8 && < 0.9                    , ghc-prim-                   , mtl                    , text   ghc-options:      -Wall   default-language:  Haskell2010@@ -95,12 +94,18 @@   hs-source-dirs:      test   main-is:             test.hs   default-language:    Haskell2010-  other-modules:       Test.Data+  other-modules:       Test.Alg+                     , Test.Alg.List+                     , Test.Data                      , Test.Data.Reflect+                     , Test.Data.Set+                     , Test.Control+                     , Test.Control.Monad   build-depends:       base     , first-class-families     , fcf-containers+    , hspec     , containers     , text 

@@ -0,0 +1,44 @@+{+  "nodes": {+    "nix-filter": {+      "locked": {+        "lastModified": 1666547822,+        "narHash": "sha256-razwnAybPHyoAyhkKCwXdxihIqJi1G6e1XP4FQOJTEs=",+        "owner": "numtide",+        "repo": "nix-filter",+        "rev": "1a3b735e13e90a8d2fd5629f2f8363bd7ffbbec7",+        "type": "github"+      },+      "original": {+        "owner": "numtide",+        "ref": "master",+        "repo": "nix-filter",+        "type": "github"+      }+    },+    "nixpkgs": {+      "locked": {+        "lastModified": 1674990008,+        "narHash": "sha256-4zOyp+hFW2Y7imxIpZqZGT8CEqKmDjwgfD6BzRUE0mQ=",+        "owner": "nixos",+        "repo": "nixpkgs",+        "rev": "d2bbcbe6c626d339b25a4995711f07625b508214",+        "type": "github"+      },+      "original": {+        "owner": "nixos",+        "ref": "nixpkgs-unstable",+        "repo": "nixpkgs",+        "type": "github"+      }+    },+    "root": {+      "inputs": {+        "nix-filter": "nix-filter",+        "nixpkgs": "nixpkgs"+      }+    }+  },+  "root": "root",+  "version": 7+}

@@ -0,0 +1,69 @@+{+  description = "Data structures and algorithms for first-class-families";++  inputs = {+    nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable";+    nix-filter.url = "github:numtide/nix-filter/master";+  };++  outputs = { self, nixpkgs, nix-filter }: +    let+      pkgs = import nixpkgs { system = "x86_64-linux"; };++      # filter = import nix-filter { };++      ghcVersion = "925";++      src = nix-filter.lib {+        root = ./.;+        include = [+          (nix-filter.lib.inDirectory "src")+          (nix-filter.lib.inDirectory "examples")+          (nix-filter.lib.inDirectory "test")+          (nix-filter.lib.matchExt "hs")+          ./fcf-containers.cabal+          ./cabal.project+          ./LICENSE+        ];+      };++      fcf-containers = hself: hself.callCabal2nix "fcf-containers" src {};++      myHaskellPackages = pkgs.haskell.packages."ghc${ghcVersion}".override {+        overrides = hself: hsuper: {+          # fcf-containers = hself.callCabal2nix "fcf-containers" sources.fcf-containers {};+          # fcf-containers = (import sources.fcf-containers {});+          fcf-containers = fcf-containers hself;+          # ListLike = pkgs.haskell.lib.dontCheck hsuper.ListLike;+          # type-of-html = pkgs.haskell.lib.doBenchmark (hself.callPackage ./nix/type-of-html.nix {inherit src;});+          # type-of-html = hself.callCabal2nix "type-of-html" src {};+          # optics-core = hsuper.optics-core.overrideAttrs(old: {+          #   configureFlags = "-f explicit-generic-labels";+          #   patches = [./optics-core.patch];+          # });+        };+      };++      shell = myHaskellPackages.shellFor {+        packages = p: [+          p.fcf-containers+        ];+        buildInputs = with pkgs.haskell.packages."ghc${ghcVersion}"; [+          myHaskellPackages.cabal-install+          ghcid+          (pkgs.haskell-language-server.override { supportedGhcVersions = [ "${ghcVersion}" ]; })+          hlint+          # implicit-hie+          # cabal2nix+        ];+        withHoogle = true;+        doBenchmark = true;+      };++    in+      {+        library = fcf-containers;+        # packages.x86_64-linux.default = ;+        devShell.x86_64-linux = shell;+      };+}

@@ -1,9 +0,0 @@-{ nixpkgs ? import <nixpkgs> {}-/* , compiler ? "ghc822" */-} : -let-  inherit (nixpkgs) pkgs;-  /* drv = import ./. { inherit compiler; }; */-  drv = import ./. { };-in-if pkgs.lib.inNixShell then drv.env else drv

@@ -19,6 +19,8 @@ This module also contains other list-related functions (that might move to other place some day). +To see examples, please do take a look of the respective test module.+ -}  --------------------------------------------------------------------------------@@ -39,13 +41,6 @@  -------------------------------------------------------------------------------- --- For the doctests:---- $setup--- >>> import           Fcf.Combinators----------------------------------------------------------------------------------- -- | Base functor for a list of type @[a]@. data ListF a b = ConsF a b | NilF @@ -65,7 +60,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (ListToFix '[1,2,3])+-- > :kind! Eval (ListToFix '[1,2,3]) -- Eval (ListToFix '[1,2,3]) :: Fix (ListF TL.Natural) -- = 'Fix ('ConsF 1 ('Fix ('ConsF 2 ('Fix ('ConsF 3 ('Fix 'NilF)))))) data ListToFix :: [a] -> Exp (Fix (ListF a))@@ -76,7 +71,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (Cata LenAlg =<< ListToFix '[1,2,3])+-- > :kind! Eval (Cata LenAlg =<< ListToFix '[1,2,3]) -- Eval (Cata LenAlg =<< ListToFix '[1,2,3]) :: TL.Natural -- = 3 data LenAlg :: Algebra (ListF a) Nat@@ -87,7 +82,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (Cata SumAlg =<< ListToFix '[1,2,3,4])+-- > :kind! Eval (Cata SumAlg =<< ListToFix '[1,2,3,4]) -- Eval (Cata SumAlg =<< ListToFix '[1,2,3,4]) :: TL.Natural -- = 10 data SumAlg :: Algebra (ListF Nat) Nat@@ -98,7 +93,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4])+-- > :kind! Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4]) -- Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4]) :: TL.Natural -- = 24 data ProdAlg :: Algebra (ListF Nat) Nat@@ -111,7 +106,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (ListToParaFix '[1,2,3])+-- > :kind! Eval (ListToParaFix '[1,2,3]) -- Eval (ListToParaFix '[1,2,3]) :: Fix --                                    (ListF (TL.Natural, [TL.Natural])) -- = 'Fix@@ -129,7 +124,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2])+-- > :kind! Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2]) -- Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2]) :: [TL.Natural] -- = '[5, 1, 3, 2] data DedupAlg :: RAlgebra (ListF (a,[a])) [a]@@ -145,7 +140,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (Sliding 3 '[1,2,3,4,5,6])+-- > :kind! Eval (Sliding 3 '[1,2,3,4,5,6]) -- Eval (Sliding 3 '[1,2,3,4,5,6]) :: [[TL.Natural]] -- = '[ '[1, 2, 3], '[2, 3, 4], '[3, 4, 5], '[4, 5, 6], '[5, 6], '[6]] data Sliding :: Nat -> [a] -> Exp [[a]]@@ -177,7 +172,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (Evens =<< RunInc 8)+-- > :kind! Eval (Evens =<< RunInc 8) -- Eval (Evens =<< RunInc 8) :: [TL.Natural] -- = '[2, 4, 6, 8] data Evens :: [a] -> Exp [a]@@ -199,7 +194,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (RunInc 8)+-- > :kind! Eval (RunInc 8) -- Eval (RunInc 8) :: [TL.Natural] -- = '[1, 2, 3, 4, 5, 6, 7, 8] data RunInc :: Nat -> Exp [Nat]@@ -212,7 +207,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (Sum '[1,2,3])+-- > :kind! Eval (Sum '[1,2,3]) -- Eval (Sum '[1,2,3]) :: TL.Natural -- = 6 data Sum :: [Nat] -> Exp Nat@@ -233,7 +228,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (MToN 1 3)+-- > :kind! Eval (MToN 1 3) -- Eval (MToN 1 3) :: [TL.Natural] -- = '[1, 2, 3] data MToN :: Nat -> Nat -> Exp [Nat]@@ -245,7 +240,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (ToList 1)+-- > :kind! Eval (ToList 1) -- Eval (ToList 1) :: [TL.Natural] -- = '[1] data ToList :: a -> Exp [a]@@ -256,13 +251,12 @@ -- -- === __Example__ ----- >>> :kind! Eval (Equal '[1,2,3] '[1,2,3])+-- > :kind! Eval (Equal '[1,2,3] '[1,2,3]) -- Eval (Equal '[1,2,3] '[1,2,3]) :: Bool -- = 'True ----- >>> :kind! Eval (Equal '[1,2,3] '[1,3,2])+-- > :kind! Eval (Equal '[1,2,3] '[1,3,2]) -- Eval (Equal '[1,2,3] '[1,3,2]) :: Bool -- = 'False data Equal :: [a] -> [a] -> Exp Bool type instance Eval (Equal as bs) = Eval (And =<< ZipWith TyEq as bs)-

@@ -22,10 +22,12 @@  module Fcf.Control.Monad where -import           Control.Monad.Identity+import           Data.Functor.Identity import           GHC.TypeNats as TN  import           Fcf hiding (type (<*>))+import           Fcf.Class.Monoid (type (<>), MEmpty)+import           Fcf.Data.Tuple  -------------------------------------------------------------------------------- @@ -40,8 +42,6 @@  type instance Eval (Map f ('Identity a)) = 'Identity (Eval (f a)) -- -------------------------------------------------------------------------------- -- Common methods for both Applicative and Monad @@ -57,6 +57,9 @@ type instance Eval (Return a) = 'Just a type instance Eval (Return a) = 'Right a type instance Eval (Return a) = 'Identity a+type instance Eval (Return a) = '(MEmpty, a)+type instance Eval (Return a) = '(MEmpty, MEmpty, a)+type instance Eval (Return a) = '(MEmpty, MEmpty, MEmpty, a)   --------------------------------------------------------------------------------@@ -71,6 +74,9 @@ --  - [] --  - Maybe --  - Either+--  - (,)+--  - (,,)+--  - (,,,) -- -- === __Example__ --@@ -98,29 +104,29 @@ type instance Eval ((f ': fs) <*> (a ': as)) =     Eval ((++) (Eval (Star_ f (a ': as))) (Eval ((<*>) fs (a ':as)))) --- | Helper for the [] applicative instance.-data Star_ :: (a -> Exp b) -> f a -> Exp (f b)-type instance Eval (Star_ _ '[]) = '[]-type instance Eval (Star_ f (a ': as)) = Eval (f a) ': Eval (Star_ f as)----- Example-data Plus1 :: Nat -> Exp Nat-type instance Eval (Plus1 n) = n TN.+ 1---- Example-data Plus2 :: Nat -> Exp Nat-type instance Eval (Plus2 n) = n TN.+ 2--+-- Maybe type instance Eval ('Nothing <*> _) = 'Nothing type instance Eval ('Just f <*> m) = Eval (Map f m) -+-- Either type instance Eval ('Left e <*> _) = 'Left e type instance Eval ('Right f <*> m) = Eval (Map f m) +-- | For tuples, the 'Monoid' constraint determines how the first values merge.+-- For example, 'Symbol's concatenate:+--+-- >>> :kind! Eval ('("hello", (Fcf.+) 15) <*> '("world!", 2002))+-- Eval ('("hello", (Fcf.+) 15) <*> '("world!", 2002)) :: (TL.Symbol,+--                                                         Natural)+-- = '("helloworld!", 2017)+type instance Eval ('(u, f) <*> '(v, x)) = '(u <> v, Eval (f x)) +-- ((,,) a b)+type instance Eval ('(a, b, f) <*> '(a', b', x)) = '(a <> a', b <> b', Eval (f x))++-- ((,,,) a b)+type instance Eval ('(a, b, c, f) <*> '(a', b', c', x)) = '(a <> a', b <> b', c <> c', Eval (f x))+ -- | Type level LiftA2. -- -- === __Example__@@ -131,31 +137,33 @@ -- -- data LiftA2 :: (a -> b -> Exp c) -> f a -> f b -> Exp (f c)--- Could a single default implementation work here? Looks like it would need--- a function that turns (a -> b -> c) to (b -> c).--- E.g. something like:--- type instance Eval (LiftA2 f fa fb) = Eval ( (<*>) (Map (f fa)) fb)--type instance Eval (LiftA2 f 'Nothing _) = 'Nothing-type instance Eval (LiftA2 f _ 'Nothing) = 'Nothing-type instance Eval (LiftA2 f ('Just a) ('Just b)) = 'Just (Eval (f a b))--type instance Eval (LiftA2 f ('Left e) _) = 'Left e-type instance Eval (LiftA2 f ('Right _) ('Left e)) = 'Left e-type instance Eval (LiftA2 f ('Right a) ('Right b)) = 'Right (Eval (f a b))-+type instance Eval (LiftA2 f fa fb) = Eval (Eval (Map (App2 f) fa) <*> fb) -type instance Eval (LiftA2 f '[] _) = '[]-type instance Eval (LiftA2 f (a ': as) '[]) = '[]-type instance Eval (LiftA2 f (a ': as) (b ':bs)) =-    Eval ((++) (Eval (LiftA2_ f a (b ': bs))) (Eval (LiftA2 f as (b ':bs))))+-- | Type level LiftA3.+--+-- === __Example__+-- +-- >>> :kind! Eval (LiftA3 Tuple3 '[1,2] '[3,4] '[5,6])+-- Eval (LiftA3 Tuple3 '[1,2] '[3,4] '[5,6]) :: [(Natural, Natural,+--                                                Natural)]+-- = '[ '(1, 3, 5), '(1, 3, 6), '(1, 4, 5), '(1, 4, 6), '(2, 3, 5),+--      '(2, 3, 6), '(2, 4, 5), '(2, 4, 6)]+--+-- >>> :kind! Eval (LiftA3 Tuple3 ('Right 5) ('Right 6) ('Left "fail"))+-- Eval (LiftA3 Tuple3 ('Right 5) ('Right 6) ('Left "fail")) :: Either+--                                                                TL.Symbol (Natural, Natural, c)+-- = 'Left "fail"+--+data LiftA3 :: (a -> b -> c -> Exp d) -> f a -> f b -> f c -> Exp (f d)+type instance Eval (LiftA3 f fa fb fc) = Eval (Eval (Eval (Map (App3 f) fa) <*> fb) <*> fc) --- Helper for list LiftA2 instance.-data LiftA2_ :: (a -> b -> Exp c) -> a -> f b -> Exp (f c)-type instance Eval (LiftA2_ f a '[]) = '[]-type instance Eval (LiftA2_ f a (b ': bs)) =-    Eval (f a b) ': Eval (LiftA2_ f a bs)+-- | Type level LiftA4.+data LiftA4 :: (a -> b -> c -> d -> Exp e) -> f a -> f b -> f c -> f d -> Exp (f e)+type instance Eval (LiftA4 f fa fb fc fd) = Eval (Eval (Eval (Eval (Map (App4 f) fa) <*> fb) <*> fc) <*> fd) +-- | Type level LiftA5.+data LiftA5 :: (a -> b -> c -> d -> e -> Exp g) -> f a -> f b -> f c -> f d -> f e -> Exp (f g)+type instance Eval (LiftA5 f fa fb fc fd fe) = Eval (Eval (Eval (Eval (Eval (Map (App5 f) fa) <*> fb) <*> fc) <*> fd) <*> fe)  -------------------------------------------------------------------------------- -- Monad@@ -171,6 +179,9 @@ --  - [] --  - Maybe --  - Either+--  - (,)+--  - (,,)+--  - (,,,) -- -- === __Example__ --@@ -202,45 +213,16 @@ type instance Eval ('[] >>= _) = '[] type instance Eval ((x ': xs) >>= f) = Eval ((f @@ x) ++  Eval (xs >>= f)) ---- For the example. Turn an input number to list of two numbers of a bit--- larger numbers.-data Plus2M :: Nat -> Exp [Nat]-type instance Eval (Plus2M n) = '[n TN.+ 2, n TN.+3]---- Part of an example-data PureXPlusY :: Nat -> Nat -> Exp [Nat]-type instance Eval (PureXPlusY x y) = Eval (Return ((TN.+) x y))---- Part of an example-data XPlusYs :: Nat -> [Nat] -> Exp [Nat]-type instance Eval (XPlusYs x ys) = Eval (ys >>= PureXPlusY x)---- | An example implementing------ sumM xs ys = do---     x <- xs---     y <- ys---     return (x + y)------ or------ sumM xs ys = xs >>= (\x -> ys >>= (\y -> pure (x+y)))------ Note the use of helper functions. This is a bit awkward, a type level--- lambda would be nice.-data XsPlusYsMonadic :: [Nat] -> [Nat] -> Exp [Nat]-type instance Eval (XsPlusYsMonadic xs ys) = Eval (xs >>= Flip XPlusYs ys)---+-- (,)+type instance Eval ('(u, a) >>= k) = Eval ('(u, Id) <*> Eval (k a)) --- data Sumnd :: [Nat] -> [Nat] -> Exp [Nat]--- type instance Eval (Sumnd xs ys) = xs >>=+-- (,,)+type instance Eval ('(u, v, a) >>= k) = Eval ('(u, v, Id) <*> Eval (k a)) --- data Sum2 :: Nat -> Nat -> Exp Nat--- type instance Eval (Sum2 x y) = x TN.+ y+-- (,,,)+type instance Eval ('(u, v, w, a) >>= k) = Eval ('(u, v, w, Id) <*> Eval (k a)) +-- | Type level >>  -- -- === __Example__ --@@ -252,21 +234,8 @@ -- Eval ( 'Nothing >> 'Just 2) :: Maybe Natural -- = 'Nothing ----- data (>>) :: m a -> m b -> Exp (m b)---- Maybe-type instance Eval ('Nothing >> b) = 'Nothing-type instance Eval ('Just a >> b) = b---- Either-type instance Eval ('Left a >> _) = 'Left a-type instance Eval ('Right _ >> b) = b---- Lists--- TODO, are the instances ok?-type instance Eval ('[] >> _) = '[]-type instance Eval ((x ': xs) >> b) = b+type instance Eval (m >> k) = Eval (m >>= ConstFn k)  -------------------------------------------------------------------------------- -- MapM@@ -314,10 +283,6 @@ data FoldlM :: (b -> a -> Exp (m b)) -> b -> t a -> Exp (m b) type instance Eval (FoldlM f z0 xs) = Eval ((Eval (Foldr (FoldlMHelper f) Return xs)) z0) --- | Helper for 'FoldlM'-data FoldlMHelper :: (b -> a -> Exp (m b)) -> a -> (b -> Exp (m b)) -> Exp (b -> Exp (m b))-type instance Eval (FoldlMHelper f a b) = Flip (>>=) b <=< Flip f a- -------------------------------------------------------------------------------- -- Traversable @@ -340,13 +305,6 @@ type instance Eval (Traverse f lst) =     Eval (Foldr (ConsHelper f) (Eval (Return '[])) lst) --- | Helper for [] traverse-data ConsHelper :: (a -> Exp (f b)) -> a -> f [b] -> Exp (f [b])-type instance Eval (ConsHelper f x ys) = Eval (LiftA2 (Pure2 '(:)) (Eval (f x)) ys)--- The following would need an extra import line:--- type instance Eval (ConsHelper f x ys) = Eval (LiftA2 Cons (Eval (f x)) ys)-- -- Maybe type instance Eval (Traverse f 'Nothing) = Eval (Return 'Nothing) type instance Eval (Traverse f ('Just x)) = Eval (Map (Pure1 'Just) (Eval (f x)))@@ -355,10 +313,8 @@ type instance Eval (Traverse f ('Left e)) = Eval (Return ('Left e)) type instance Eval (Traverse f ('Right x)) = Eval (Map (Pure1 'Right) (Eval (f x))) ---- | Id function correspondes to term level 'id'-function.-data Id :: a -> Exp a-type instance Eval (Id a) = a+-- ((,) a)+type instance Eval (Traverse f '(x, y)) = Eval (Map (Tuple2 x) (Eval (f y)))   -- | Sequence@@ -385,4 +341,91 @@ data Sequence :: t (f a) -> Exp (f (t a)) type instance Eval (Sequence tfa) = Eval (Traverse Id tfa) +--------------------------------------------------------------------------------+-- Utility +-- | Id function correspondes to term level 'id'-function.+data Id :: a -> Exp a+type instance Eval (Id a) = a++--------------------------------------------------------------------------------+-- Helper Functions++-- | Needed by LiftA2 instance to partially apply function+data App2 :: (a -> b -> c) -> a -> Exp (b -> c)+type instance Eval (App2 f a) = f a++-- | Needed by LiftA3 instance to partially apply function+data App3 :: (a -> b -> c -> d) -> a -> Exp (b -> Exp (c -> d))+type instance Eval (App3 f a) = Pure2 f a++-- | Needed by LiftA4 instance to partially apply function+data App4 :: (a -> b -> c -> d -> e) -> a -> Exp (b -> Exp (c -> Exp (d -> e)))+type instance Eval (App4 f a) = App3 (f a)++-- | Needed by LiftA5 instance to partially apply function+data App5 :: (a -> b -> c -> d -> e -> g) -> a -> Exp (b -> Exp (c -> Exp (d -> Exp (e -> g))))+type instance Eval (App5 f a) = App4 (f a)++-- | Helper for the [] applicative instance.+data Star_ :: (a -> Exp b) -> f a -> Exp (f b)+type instance Eval (Star_ _ '[]) = '[]+type instance Eval (Star_ f (a ': as)) =+    Eval (f a) ': Eval (Star_ f as)++-- | Helper for 'FoldlM'+data FoldlMHelper :: (b -> a -> Exp (m b)) -> a -> (b -> Exp (m b)) -> Exp (b -> Exp (m b))+type instance Eval (FoldlMHelper f a b) = Flip (>>=) b <=< Flip f a++-- | Helper for [] traverse+data ConsHelper :: (a -> Exp (f b)) -> a -> f [b] -> Exp (f [b])+type instance Eval (ConsHelper f x ys) = Eval (LiftA2 (Pure2 '(:)) (Eval (f x)) ys)+-- The following would need an extra import line:+-- type instance Eval (Cons_f f x ys) = Eval (LiftA2 Cons (Eval (f x)) ys)+++--------------------------------------------------------------------------------+-- For Examples++-- | For Applicative documentation example+data Plus1 :: Nat -> Exp Nat+type instance Eval (Plus1 n) = n TN.+ 1++-- | For Applicative documentation example+data Plus2 :: Nat -> Exp Nat+type instance Eval (Plus2 n) = n TN.+ 2++-- | For the example. Turn an input number to list of two numbers of a bit+-- larger numbers.+data Plus2M :: Nat -> Exp [Nat]+type instance Eval (Plus2M n) = '[n TN.+ 2, n TN.+3]++-- | Part of an example+data PureXPlusY :: Nat -> Nat -> Exp [Nat]+type instance Eval (PureXPlusY x y) = Eval (Return ((TN.+) x y))++-- | Part of an example+data XPlusYs :: Nat -> [Nat] -> Exp [Nat]+type instance Eval (XPlusYs x ys) = Eval (ys >>= PureXPlusY x)++-- | An example implementing+--+-- sumM xs ys = do+--     x <- xs+--     y <- ys+--     return (x + y)+--+-- or+--+-- sumM xs ys = xs >>= (\x -> ys >>= (\y -> pure (x+y)))+--+-- Note the use of helper functions. This is a bit awkward, a type level+-- lambda would be nice.+data XsPlusYsMonadic :: [Nat] -> [Nat] -> Exp [Nat]+type instance Eval (XsPlusYsMonadic xs ys) = Eval (xs >>= Flip XPlusYs ys)++-- data Sumnd :: [Nat] -> [Nat] -> Exp [Nat]+-- type instance Eval (Sumnd xs ys) = xs >>=++-- data Sum2 :: Nat -> Nat -> Exp Nat+-- type instance Eval (Sum2 x y) = x TN.+ y

@@ -7,7 +7,6 @@ {-# LANGUAGE TypeFamilies           #-} {-# LANGUAGE TypeInType             #-} {-# LANGUAGE TypeOperators          #-}-{-# LANGUAGE UndecidableInstances   #-} {-# OPTIONS_GHC -Wall                       #-} {-# OPTIONS_GHC -Werror=incomplete-patterns #-} @@ -30,13 +29,14 @@  import qualified GHC.TypeLits as TL import           GHC.TypeLits (Nat, Symbol, KnownNat, KnownSymbol)+import           Data.String (fromString, IsString) import           Data.Proxy-import qualified Data.Map.Strict as MS+-- import qualified Data.Map.Strict as MS+import qualified Data.Map as DM import qualified Data.IntMap.Strict as IMS import qualified Data.Set as S-#if __GLASGOW_HASKELL__ >= 902-import qualified Data.Text as Txt-#endif+-- #if __GLASGOW_HASKELL__ >= 902+-- #endif import qualified Data.Tree as T  -- import qualified Fcf.Core as C (Eval)@@ -87,218 +87,112 @@  -------------------------------------------------------------------------------- -class KnownVal typeval val where-    fromType :: Proxy typeval -> val--instance KnownNat n => KnownVal (n :: Nat) Integer where-    fromType _ = TL.natVal (Proxy @n)+class KnownVal val kind where+    fromType :: Proxy kind -> val -instance KnownNat n => KnownVal (n :: Nat) Int where+instance (KnownNat n, Num a) => KnownVal a (n :: Nat) where     fromType _ = fromInteger $ TL.natVal (Proxy @n) -instance KnownSymbol s => KnownVal (s :: Symbol) String where-    fromType _ = TL.symbolVal (Proxy @s)-------------------------------------------------------------------------------------- List instances--instance KnownVal ('[] :: [Nat]) [Integer] where-    fromType _ = []--instance (KnownNat n, KnownVal ns [Integer]) => KnownVal (n : ns :: [Nat]) [Integer] where-    fromType _ = TL.natVal (Proxy @n) : fromType (Proxy @ns)---instance KnownVal ('[] :: [Nat]) [Int] where-    fromType _ = []--instance (KnownNat n, KnownVal ns [Int]) => KnownVal (n : ns :: [Nat]) [Int] where-    fromType _ = fromInteger (TL.natVal (Proxy @n)) : fromType (Proxy @ns)+instance KnownVal Bool 'True where fromType _ = True+instance KnownVal Bool 'False where fromType _ = False +instance (IsString str, KnownSymbol s) => KnownVal str (s :: Symbol )where+    fromType _ = fromString $ TL.symbolVal (Proxy @s) -instance KnownVal ('[] :: [Symbol]) [String] where-    fromType _ = []+#if __GLASGOW_HASKELL__ >= 902 -instance (KnownSymbol sym, KnownVal syms [String])-    => KnownVal (sym : syms :: [Symbol]) [String]+-- | Text instance.+--+-- === __Example__+--+-- >>> import qualified Data.Text as Txt+-- >>> :{+-- afun :: forall r. (r ~ 'FTxt.Text "hmm") => Txt.Text+-- afun = fromType (Proxy @r)+-- :}+--+-- >>> afun+-- "hmm"+instance (IsString str, KnownSymbol sym) => KnownVal str ('FTxt.Text sym)   where-    fromType _ = TL.symbolVal (Proxy @sym) : fromType (Proxy @syms)+    fromType _ = fromString $ fromType $ Proxy @sym  +#endif -instance KnownVal ('[] :: [(Nat,Nat)]) [(Int,Int)] where-    fromType _ = []--- This helps with NatMap instances+-------------------------------------------------------------------------------- -instance (KnownNat n, KnownNat m, KnownVal nms [(Int,Int)])-    => KnownVal ( '(n,m) : nms :: [(Nat,Nat)]) [(Int,Int)]-  where-    fromType _ =-        (fromInteger (TL.natVal (Proxy @n)), fromInteger (TL.natVal (Proxy @m)))-        : fromType (Proxy @nms)--- This helps with NatMap instances+-- List instances -instance KnownVal ('[] :: [(Nat,Symbol)]) [(Int,String)] where+instance KnownVal [a] '[] where     fromType _ = []--- This helps with NatMap instances -instance (KnownNat n, KnownSymbol m, KnownVal nms [(Int,String)])-    => KnownVal ( '(n,m) : nms :: [(Nat,Symbol)]) [(Int,String)]-  where-    fromType _ =-        (fromInteger (TL.natVal (Proxy @n)), TL.symbolVal (Proxy @m))-        : fromType (Proxy @nms)--- This helps with NatMap instances+instance (KnownVal typ x, KnownVal [typ] xs) => KnownVal [typ] (x ': xs) where+    fromType _ = fromType (Proxy @x) : fromType (Proxy @xs)  --------------------------------------------------------------------------------  -- Trees---- instances for Forests, that is, lists of Trees.-instance KnownVal '[] [T.Tree Int] where fromType _ = []---- instances for Forests-instance (KnownVal t (T.Tree Int), KnownVal trees [T.Tree Int])-    => KnownVal (t : trees) [T.Tree Int]-  where-    fromType _ = fromType @t Proxy : fromType @trees Proxy---- instance for Trees (using forest definition).-instance (KnownNat n, KnownVal trees [T.Tree Int])-    => KnownVal ('FT.Node (n :: Nat) trees) (T.Tree Int)-  where-    fromType _ = T.Node (fromType @n Proxy) (fromType @trees Proxy)---instance KnownVal '[] [T.Tree Integer] where fromType _ = []--instance (KnownVal t (T.Tree Integer), KnownVal trees [T.Tree Integer])-    => KnownVal (t : trees) [T.Tree Integer]-  where-    fromType _ = fromType @t Proxy : fromType @trees Proxy--instance (KnownNat n, KnownVal trees [T.Tree Integer])-    => KnownVal ('FT.Node (n :: Nat) trees) (T.Tree Integer)-  where-    fromType _ = T.Node (fromType @n Proxy) (fromType @trees Proxy)---instance KnownVal '[] [T.Tree String] where fromType _ = []--instance (KnownVal t (T.Tree String), KnownVal trees [T.Tree String])-    => KnownVal (t : trees) [T.Tree String]-  where-    fromType _ = fromType @t Proxy : fromType @trees Proxy--instance (KnownSymbol n, KnownVal trees [T.Tree String])-    => KnownVal ('FT.Node (n :: Symbol) trees) (T.Tree String)+--+instance (KnownVal typ k, KnownVal (T.Forest typ) trees) => KnownVal (T.Tree typ) ('FT.Node k trees)   where-    fromType _ = T.Node (fromType @n Proxy) (fromType @trees Proxy)-+    fromType _ = T.Node (fromType (Proxy @k)) (fromType (Proxy @trees))  --------------------------------------------------------------------------------  -- NatMaps / IntMaps--instance (KnownVal (pairs :: [(Nat,Nat)]) [(Int,Int)])-    => KnownVal ('NM.NatMap pairs) (IMS.IntMap Int)-  where-    fromType _ = IMS.fromList (fromType @pairs Proxy)--instance (KnownVal (pairs :: [(Nat,Integer)]) [(Int,Integer)])-    => KnownVal ('NM.NatMap pairs) (IMS.IntMap Integer)-  where-    fromType _ = IMS.fromList (fromType @pairs Proxy)--instance (KnownVal (pairs :: [(Nat,Symbol)]) [(Int,String)])-    => KnownVal ('NM.NatMap pairs) (IMS.IntMap String)+--+instance (KnownVal [(Int,val)] pairs) => KnownVal (IMS.IntMap val) ('NM.NatMap pairs)   where-    fromType _ = IMS.fromList (fromType @pairs Proxy)-+    fromType _ = IMS.fromList (fromType (Proxy @pairs))  --------------------------------------------------------------------------------  -- Maps -instance (KnownVal (pairs :: [(Nat,Nat)]) [(Int,Int)])-    => KnownVal ('MC.MapC pairs) (MS.Map Int Int)-  where-    fromType _ = MS.fromList (fromType @pairs Proxy)--instance (KnownVal (pairs :: [(Nat,Integer)]) [(Int,Integer)])-    => KnownVal ('MC.MapC pairs) (MS.Map Int Integer)-  where-    fromType _ = MS.fromList (fromType @pairs Proxy)--instance (KnownVal (pairs :: [(Nat,Symbol)]) [(Int,String)])-    => KnownVal ('MC.MapC pairs) (MS.Map Int String)-  where-    fromType _ = MS.fromList (fromType @pairs Proxy)---instance (KnownVal (pairs :: [(Symbol,Nat)]) [(String,Int)])-    => KnownVal ('MC.MapC pairs) (MS.Map String Int)-  where-    fromType _ = MS.fromList (fromType @pairs Proxy)--instance (KnownVal (pairs :: [(Symbol,Integer)]) [(String,Integer)])-    => KnownVal ('MC.MapC pairs) (MS.Map String Integer)-  where-    fromType _ = MS.fromList (fromType @pairs Proxy)--instance (KnownVal (pairs :: [(Symbol,Symbol)]) [(String,String)])-    => KnownVal ('MC.MapC pairs) (MS.Map String String)+instance (Ord key, KnownVal [(key,val)] pairs) => KnownVal (DM.Map key val) ('MC.MapC pairs)   where-    fromType _ = MS.fromList (fromType @pairs Proxy)-+    fromType _ = DM.fromList (fromType (Proxy @pairs))  --------------------------------------------------------------------------------  -- Set- -instance (KnownVal (mems :: [Nat]) [Int]) => KnownVal ('FS.Set mems) (S.Set Int)-  where-    fromType _ = S.fromList (fromType @mems Proxy) -instance (KnownVal (mems :: [Nat]) [Integer]) => KnownVal ('FS.Set mems) (S.Set Integer)-  where-    fromType _ = S.fromList (fromType @mems Proxy)--instance (KnownVal (mems :: [Symbol]) [String]) => KnownVal ('FS.Set mems) (S.Set String)+instance (Ord typ, KnownVal [typ] kind) => KnownVal (S.Set typ) ('FS.Set kind)   where-    fromType _ = S.fromList (fromType @mems Proxy)+    fromType _ = S.fromList (fromType (Proxy @kind))+ +-------------------------------------------------------------------------------- +-- Either ---------------------------------------------------------------------------------+instance (KnownVal a1 a) => KnownVal (Either a1 b1) ('Left a) where+    fromType _ = Left (fromType @a1 (Proxy @a)) -#if __GLASGOW_HASKELL__ >= 902+instance (KnownVal b1 b) => KnownVal (Either a1 b1) ('Right b) where+    fromType _ = Right (fromType @b1 (Proxy @b)) --- Text+-------------------------------------------------------------------------------- --- instance (KnownVal (sym :: Symbol) String) => KnownVal ('FTxt.Text sym) Txt.Text---   where---     fromType _ = Txt.pack $ fromType @sym Proxy+-- Maybe +instance (KnownVal a1 a) => KnownVal (Maybe a1) ('Just a) where+    fromType _ = Just (fromType @a1 (Proxy @a)) --- | Text instance.------ === __Example__------ >>> :{--- afun :: forall r. (r ~ 'FTxt.Text "hmm") => Txt.Text--- afun = fromType @r Proxy--- :}------ >>> afun--- "hmm"-instance KnownSymbol sym => KnownVal ('FTxt.Text sym) Txt.Text-  where-    fromType _ = Txt.pack $ fromType @sym Proxy+instance KnownVal (Maybe a1) 'Nothing where+    fromType _ = Nothing +-------------------------------------------------------------------------------- +-- Tuples -#else+instance (KnownVal a1 a, KnownVal b1 b) => KnownVal (a1,b1) '(a,b) where+    fromType _ = (fromType @a1 (Proxy @a), fromType @b1 (Proxy @b)) -#endif+instance (KnownVal a1 a, KnownVal b1 b, KnownVal c1 c) => KnownVal (a1,b1,c1) '(a,b,c) where+    fromType _ = (fromType @a1 (Proxy @a), fromType @b1 (Proxy @b), fromType @c1 (Proxy @c)) +instance (KnownVal a1 a, KnownVal b1 b, KnownVal c1 c, KnownVal d1 d) => KnownVal (a1,b1,c1,d1) '(a,b,c,d) where+    fromType _ = (fromType @a1 (Proxy @a), fromType @b1 (Proxy @b), fromType @c1 (Proxy @c), fromType @d1 (Proxy @d)) +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))

@@ -73,16 +73,6 @@  -------------------------------------------------------------------------------- --- For the doctests:---- $setup--- >>> import qualified GHC.TypeLits as TL--- >>> import           Fcf.Data.Nat--- >>> import           Fcf.Data.Symbol--- >>> import           Fcf.Alg.Sort----------------------------------------------------------------------------------- -- | Set-definition. newtype Set a = Set [a] @@ -93,7 +83,7 @@ -- -- === __Example__ ----- >>> :kind! (Eval Empty :: Set Nat)+-- > :kind! (Eval Empty :: Set Nat) -- (Eval Empty :: Set Nat) :: Set TL.Natural -- = 'Set '[] --@@ -105,7 +95,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (Singleton 1)+-- > :kind! Eval (Singleton 1) -- Eval (Singleton 1) :: Set TL.Natural -- = 'Set '[1] data Singleton :: v -> Exp (Set v)@@ -116,11 +106,11 @@ -- -- === __Example__ ----- >>> :kind! Eval (Insert 3 =<< FromList '[1, 2])+-- > :kind! Eval (Insert 3 =<< FromList '[1, 2]) -- Eval (Insert 3 =<< FromList '[1, 2]) :: Set TL.Natural -- = 'Set '[3, 1, 2] ----- >>> :kind! Eval (Insert 2 =<< FromList '[1, 2])+-- > :kind! Eval (Insert 2 =<< FromList '[1, 2]) -- Eval (Insert 2 =<< FromList '[1, 2]) :: Set TL.Natural -- = 'Set '[1, 2] data Insert :: v -> Set v -> Exp (Set v)@@ -133,11 +123,11 @@ -- -- === __Example__ ----- >>> :kind! Eval (Delete 5 =<< FromList '[5, 3])+-- > :kind! Eval (Delete 5 =<< FromList '[5, 3]) -- Eval (Delete 5 =<< FromList '[5, 3]) :: Set TL.Natural -- = 'Set '[3] ----- >>> :kind! Eval (Delete 7 =<< FromList '[5, 3])+-- > :kind! Eval (Delete 7 =<< FromList '[5, 3]) -- Eval (Delete 7 =<< FromList '[5, 3]) :: Set TL.Natural -- = 'Set '[5, 3] data Delete :: v -> Set v -> Exp (Set v)@@ -148,10 +138,11 @@ -- -- === __Example__ ----- >>> :kind! Eval (Member 5 =<< FromList '[5, 3])+-- > :kind! Eval (Member 5 =<< FromList '[5, 3]) -- Eval (Member 5 =<< FromList '[5, 3]) :: Bool -- = 'True--- >>> :kind! Eval (Member 7 =<< FromList '[5, 3])+--+-- > :kind! Eval (Member 7 =<< FromList '[5, 3]) -- Eval (Member 7 =<< FromList '[5, 3]) :: Bool -- = 'False data Member :: v -> Set v -> Exp Bool@@ -161,10 +152,11 @@ -- -- === __Example__ ----- >>> :kind! Eval (NotMember 5 =<< FromList '[5, 3])+-- > :kind! Eval (NotMember 5 =<< FromList '[5, 3]) -- Eval (NotMember 5 =<< FromList '[5, 3]) :: Bool -- = 'False--- >>> :kind! Eval (NotMember 7 =<< FromList '[5, 3])+--+-- > :kind! Eval (NotMember 7 =<< FromList '[5, 3]) -- Eval (NotMember 7 =<< FromList '[5, 3]) :: Bool -- = 'True data NotMember :: v -> Set v -> Exp Bool@@ -176,10 +168,11 @@ -- -- === __Example__ ----- >>> :kind! Eval (Null =<< FromList '[5, 3])+-- > :kind! Eval (Null =<< FromList '[5, 3]) -- Eval (Null =<< FromList '[5, 3]) :: Bool -- = 'False--- >>> :kind! Eval (Null =<< Empty)+-- +-- > :kind! Eval (Null =<< Empty) -- Eval (Null =<< Empty) :: Bool -- = 'True data Null :: Set v -> Exp Bool@@ -191,7 +184,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (Size =<< FromList '[5, 3])+-- > :kind! Eval (Size =<< FromList '[5, 3]) -- Eval (Size =<< FromList '[5, 3]) :: TL.Natural -- = 2 data Size :: Set v -> Exp TL.Nat@@ -202,19 +195,19 @@ -- -- === __Example__ ----- >>> :kind! Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4]))+-- > :kind! Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4])) -- Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4])) :: Bool -- = 'True ----- >>> :kind! Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4]))+-- > :kind! Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4])) -- Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4])) :: Bool -- = 'True ----- >>> :kind! Eval (IsSubsetOf ('Set '[0,2,1,3,4]) ('Set '[0,1,2,3,4]))+-- > :kind! Eval (IsSubsetOf ('Set '[0,2,1,3,4]) ('Set '[0,1,2,3,4])) -- Eval (IsSubsetOf ('Set '[0,2,1,3,4]) ('Set '[0,1,2,3,4])) :: Bool -- = 'True ----- >>> :kind! Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4]))+-- > :kind! Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4])) -- Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4])) :: Bool -- = 'False data IsSubsetOf :: Set a -> Set a -> Exp Bool@@ -226,11 +219,11 @@ -- -- === __Example__ ----- >>> :kind! Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4]))+-- > :kind! Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4])) -- Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4])) :: Bool -- = 'False ----- >>> :kind! Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4]))+-- > :kind! Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4])) -- Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4])) :: Bool -- = 'True data IsProperSubsetOf :: Set a -> Set a -> Exp Bool@@ -244,7 +237,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) )+-- > :kind! Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) ) -- Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) ) :: Set --                                                                        TL.Natural -- = 'Set '[7, 5, 3]@@ -263,7 +256,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))+-- > :kind! Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) -- Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) :: Set --                                                                            TL.Natural -- = 'Set '[3]@@ -280,7 +273,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))+-- > :kind! Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) -- Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) :: Set --                                                                              TL.Natural -- = 'Set '[5]@@ -333,7 +326,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (PowerSet =<< FromList '["a", "b", "c"])+-- > :kind! Eval (PowerSet =<< FromList '["a", "b", "c"]) -- Eval (PowerSet =<< FromList '["a", "b", "c"]) :: Set --                                                    (Set TL.Symbol) -- = 'Set@@ -341,7 +334,7 @@ --        'Set '["a"], 'Set '["a", "b"], 'Set '["a", "c"], --        'Set '["a", "b", "c"]] ----- >>> :kind! Eval (PowerSet =<< FromList '[Int, Char, Maybe Int])+-- > :kind! Eval (PowerSet =<< FromList '[Int, Char, Maybe Int]) -- Eval (PowerSet =<< FromList '[Int, Char, Maybe Int]) :: Set --                                                           (Set (*)) -- = 'Set@@ -361,7 +354,7 @@ -- -- === __Example__ ----- >>> :kind! Eval (FromList '[1, 2])+-- > :kind! Eval (FromList '[1, 2]) -- Eval (FromList '[1, 2]) :: Set TL.Natural -- = 'Set '[1, 2] data FromList :: [v] -> Exp (Set v)@@ -371,15 +364,14 @@ -- -- === __Example__ ----- >>> :kind! Eval (ToList =<< PowerSet =<< FromList '[1,2,3])+-- > :kind! Eval (ToList =<< PowerSet =<< FromList '[1,2,3]) -- Eval (ToList =<< PowerSet =<< FromList '[1,2,3]) :: [Set --                                                        TL.Natural] -- = '[ 'Set '[], 'Set '[3], 'Set '[2], 'Set '[2, 3], 'Set '[1], --      'Set '[1, 2], 'Set '[1, 3], 'Set '[1, 2, 3]] ----- >>> :kind! Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3])+-- > :kind! Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3]) -- Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3]) :: [[TL.Natural]] -- = '[ '[], '[1], '[1, 2], '[1, 2, 3], '[1, 3], '[2], '[2, 3], '[3]] data ToList :: Set v -> Exp [v] type instance Eval (ToList ('Set lst)) = lst-

@@ -40,3 +40,20 @@ -- = '(2, 1) data Swap :: (a, b) -> Exp (b, a) type instance Eval (Swap '(a,b)) = '(b,a)++-- | 2-tuple to allow for partial application of 2-tuple at the type level+data Tuple2 :: a -> b -> Exp (a, b)+type instance Eval (Tuple2 a b) = '(a,b)++-- | 3-tuple to allow for partial application of 3-tuple at the type level+data Tuple3 :: a -> b -> c -> Exp (a, b, c)+type instance Eval (Tuple3 a b c) = '(a,b,c)++-- | 4-tuple to allow for partial application of 4-tuple at the type level+data Tuple4 :: a -> b -> c -> d -> Exp (a, b, c, d)+type instance Eval (Tuple4 a b c d) = '(a,b,c,d)++-- | 5-tuple to allow for partial application of 4-tuple at the type level+data Tuple5 :: a -> b -> c -> d -> e -> Exp (a, b, c, d, e)+type instance Eval (Tuple5 a b c d e) = '(a,b,c,d,e)+

@@ -0,0 +1,10 @@++module Test.Alg where++import           Test.Alg.List as L (spec)+import           Test.Hspec (describe, Spec)++spec :: Spec+spec = describe "Data"  +  L.spec+

@@ -0,0 +1,171 @@+{-# 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.List 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.List where++import           Data.Proxy+import           Data.Type.Equality ((:~:)(Refl))+import           Test.Hspec (describe, it, shouldBe, Spec)++import           Fcf.Core (Eval)+import           Fcf.Combinators (type (=<<))+import           Fcf.Alg.List+import           Fcf.Alg.Morphism+import           Fcf.Data.Reflect (fromType)++--------------------------------------------------------------------------------++-- This module won't compile, if the Refl doesn't give the correct answer.+--+-- > :kind! Eval (ListToFix '[1,2,3])+-- Eval (ListToFix '[1,2,3]) :: Fix (ListF TL.Natural)+-- = 'Fix ('ConsF 1 ('Fix ('ConsF 2 ('Fix ('ConsF 3 ('Fix 'NilF))))))+_ = Refl :: Eval (ListToFix '[1,2,3])+  :~: 'Fix ('ConsF 1 ('Fix ('ConsF 2 ('Fix ('ConsF 3 ('Fix 'NilF))))))+++-- This module won't compile, if the Refl doesn't give the correct answer.+--  +-- > :kind! Eval (ListToParaFix '[1,2,3])+-- Eval (ListToParaFix '[1,2,3]) :: Fix+--                                    (ListF (TL.Natural, [TL.Natural]))+-- = 'Fix+--     ('ConsF+--        '(1, '[2, 3])+--        ('Fix ('ConsF '(2, '[3]) ('Fix ('ConsF '(3, '[]) ('Fix 'NilF))))))+_ = Refl :: Eval (ListToParaFix '[1,2,3])+  :~: 'Fix ('ConsF+       '(1, '[2, 3])+       ('Fix ('ConsF '(2, '[3]) ('Fix ('ConsF '(3, '[]) ('Fix 'NilF))))))+++-- This module won't compile, if the Refl doesn't give the correct answer.+--  +-- > :kind! Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2])+-- Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2]) :: [TL.Natural]+-- = '[5, 1, 3, 2]+_ = Refl :: Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2])+  :~: '[5, 1, 3, 2]+++-- This module won't compile, if the Refl doesn't give the correct answer.+--  +-- > :kind! Eval (Sliding 3 '[1,2,3,4,5,6])+-- Eval (Sliding 3 '[1,2,3,4,5,6]) :: [[TL.Natural]]+-- = '[ '[1, 2, 3], '[2, 3, 4], '[3, 4, 5], '[4, 5, 6], '[5, 6], '[6]]+_ = Refl :: Eval (Sliding 3 '[1,2,3,4,5,6])+  :~: '[ '[1, 2, 3], '[2, 3, 4], '[3, 4, 5], '[4, 5, 6], '[5, 6], '[6]]+++-- This module won't compile, if the Refl doesn't give the correct answer.+--  +-- > :kind! Eval (Evens =<< RunInc 8)+-- Eval (Evens =<< RunInc 8) :: [TL.Natural]+-- = '[2, 4, 6, 8]+_ = Refl :: Eval (Evens =<< RunInc 8)+  :~: '[2, 4, 6, 8]+++-- This module won't compile, if the Refl doesn't give the correct answer.+--  +-- > :kind! Eval (RunInc 8)+-- Eval (RunInc 8) :: [TL.Natural]+-- = '[1, 2, 3, 4, 5, 6, 7, 8]+_ = Refl :: Eval (RunInc 8)+  :~: '[1, 2, 3, 4, 5, 6, 7, 8]+++-- This module won't compile, if the Refl doesn't give the correct answer.+--  +-- > :kind! Eval (MToN 1 3)+-- Eval (MToN 1 3) :: [TL.Natural]+-- = '[1, 2, 3]+_ = Refl :: Eval (MToN 1 3)+  :~: '[1, 2, 3]++-- This module won't compile, if the Refl doesn't give the correct answer.+--  +-- > :kind! Eval (ToList 1)+-- Eval (ToList 1) :: [TL.Natural]+-- = '[1]+_ = Refl :: Eval (ToList 1)+  :~: '[1]++  +--------------------------------------------------------------------------------++-- > :kind! Eval (Cata LenAlg =<< ListToFix '[1,2,3])+-- Eval (Cata LenAlg =<< ListToFix '[1,2,3]) :: TL.Natural+-- = 3++-- > :kind! Eval (Cata SumAlg =<< ListToFix '[1,2,3,4])+-- Eval (Cata SumAlg =<< ListToFix '[1,2,3,4]) :: TL.Natural+-- = 10++-- > :kind! Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4])+-- Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4]) :: TL.Natural+-- = 24++-- > :kind! Eval (Sum '[1,2,3])+-- Eval (Sum '[1,2,3]) :: TL.Natural+-- = 6++-- > :kind! Eval (Equal '[1,2,3] '[1,2,3])+-- Eval (Equal '[1,2,3] '[1,2,3]) :: Bool+-- = 'True++-- > :kind! Eval (Equal '[1,2,3] '[1,3,2])+-- Eval (Equal '[1,2,3] '[1,3,2]) :: Bool+-- = 'False++spec :: Spec+spec = describe "List" $ do+  it "Cata LenAlg" $ do+    let test :: forall r. (r ~ Eval (Cata LenAlg =<< ListToFix '[1,2,3])) => Int+        test = fromType (Proxy @r)+    test `shouldBe` 3+  it "Cata SumAlg" $ do+    let test :: forall r. (r ~ Eval (Cata SumAlg =<< ListToFix '[1,2,3,4])) => Int+        test = fromType (Proxy @r)+    test `shouldBe` 10+  it "Cata ProdAlg" $ do+    let test :: forall r. (r ~ Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4])) => Int+        test = fromType (Proxy @r)+    test `shouldBe` 24+  it "Sum" $ do+    let test :: forall r. (r ~ Eval (Sum '[1,2,3])) => Int+        test = fromType (Proxy @r)+    test `shouldBe` 6+  it "Equal, True" $ do+    let test :: forall r. (r ~ Eval (Equal '[1,2,3] '[1,2,3])) => Bool+        test = fromType (Proxy @r)+    test `shouldBe` True+  it "Equal, False" $ do+    let test :: forall r. (r ~ Eval (Equal '[1,2,3] '[1,3,2])) => Bool+        test = fromType (Proxy @r)+    test `shouldBe` False+

@@ -0,0 +1,9 @@++module Test.Control where++import           Test.Control.Monad as M (spec)+import           Test.Hspec (describe, Spec)++spec :: Spec+spec = describe "Control" $ do+  M.spec

@@ -0,0 +1,140 @@+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE TypeApplications       #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE RankNTypes             #-}+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE TupleSections          #-}+{-# LANGUAGE AllowAmbiguousTypes    #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# OPTIONS_GHC -Wall                       #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++module Test.Control.Monad where++import           Data.Functor ((<&>))+import           Data.Proxy+import           Control.Applicative+import           Test.Hspec (describe, it, shouldBe, Spec)+import           GHC.TypeLits (Nat, Symbol)++import           Fcf hiding (type (<*>))+import           Fcf.Data.Tuple+import           Fcf.Data.List (Cons)+import           Fcf.Control.Monad+import           Fcf.Class.Monoid (type (.<>))+import           Fcf.Data.Reflect (fromType)++-- data TraversableTest = TraversableTest Symbol [(Symbol, Nat)]++data SafeMinus :: Nat -> Nat -> Exp (Either Symbol Nat)+type instance Eval (SafeMinus a b) = If (Eval (a >= b)) ('Right (Eval (a - b))) ('Left "Nat cannot be negative")+++spec :: Spec+spec = describe "Monad" $ do+  it "liftA2 (,) instance" $ do+    let test :: forall r. (r ~ Eval (LiftA2 Tuple2 '("hello ", 5) '("world", 6))) => (String, (Int, Int))+        test = fromType (Proxy @r)+    test +      `shouldBe` +      liftA2 (,) ("hello ", 5) ("world", 6)+  it "<*> (,) instance" $ do+    let test :: forall r. (r ~ Eval ('("hello ", (+) 15) <*> '("world!", 2002))) => (String,Int)+        test = fromType (Proxy @r)+    test +      `shouldBe` +      ("hello ", (+) 15) <*> ("world!", 2002)+  it ">>= (,) instance" $ do+    let test :: forall r. (r ~ Eval ('("age", 5) >>= (Return <=< (+) 1))) => (String,Int)+        test = fromType (Proxy @r)+    test +      `shouldBe` +      (("age",5) <&> (+) 1)+      -- Above was suggested by hlint for the following:+      -- (("age",5) >>= return . (+) 1)+  it "liftA3 (,,) instance" $ do+    let test :: forall r. (r ~ Eval (LiftA3 Tuple3 '("hello ", "<", 6) '("world", " ", 8) '("!", ">", 10))) => (String, String, (Int, Int, Int))+        test = fromType (Proxy @r)+    test +      `shouldBe` +      liftA3 (,,) ("hello ","<",6) ("world"," ",8) ("!",">",10)+  it ">>= (,,) instance" $ do+    let test :: forall r. (r ~ Eval ('("he","wo",19) >>= (Tuple3 "llo" "rld" <=< Flip (-) 1))) => (String,String,Int)+        test = fromType (Proxy @r)+    test +      `shouldBe` +      (("he","wo",19) >>= ("llo","rld",) . flip (-) 1)+  it "liftA4 Either instance test Left" $ do+    let test :: forall r. (r ~ Eval (LiftA4 Tuple4 ('Right 5) ('Right 6) ('Right 7) ('Left "fail"))) => Either String (Int,Int,Int,Int)+        test = fromType (Proxy @r)+    test +      `shouldBe` +      (,,,) <$> Right 5 <*> Right 6 <*> Right 7 <*> Left "fail"+  it "liftA4 Either instance test Right" $ do+    let test :: forall r. (r ~ Eval (LiftA4 Tuple4 ('Right 5) ('Right 6) ('Right 7) ('Right 0))) => Either String (Int,Int,Int,Int)+        test = fromType (Proxy @r)+    test +      `shouldBe` +      (,,,) <$> Right 5 <*> Right 6 <*> Right 7 <*> Right 0+  it "Traversable Either instance, test with MapM" $ do+    let typeLevelFunc :: forall (list :: [(Symbol,Nat)]) r. +            (r ~ Eval +              (Map +                (Flip Cons '[] <=< Tuple2 "test") +                (MapM+                  (MapM (Flip SafeMinus 1))+                  @@ list+                )+              )+            ) => Proxy r+        typeLevelFunc = Proxy @r+    let safeMinus a b = if a >= b then Right (a - b) else Left "Nat cannot be negative"+    let valTest :: [(String,Int)] -> Either String [(String, [(String, Int)])]+        valTest list = fmap (flip (:) [] . ("test",)) (mapM (mapM (`safeMinus` 1)) list)+    fromType (typeLevelFunc @'[ '("key1",1), '("key2",2)])+      `shouldBe` +      valTest [("key1",1),("key2",2)]+    fromType (typeLevelFunc @'[ '("key1",0), '("key2",2)])+      `shouldBe` +      valTest [("key1",0),("key2",2)]+  it "liftA5 [] instance" $ do+    let test :: forall r. (r ~ Eval (LiftA5 Tuple5 '[1,5] '[2,4] '[6,7,8] '[9,11,10] '[0] )) => [(Int,Int,Int,Int,Int)]+        test = fromType (Proxy @r)+    test +      `shouldBe` +      (,,,,) <$> [1,5] <*> [2,4] <*> [6,7,8] <*> [9,11,10] <*> [0]+  it "<*> [] instance" $ do+    let test :: forall r. (r ~ Eval ('[(+) 1,(+) 2] <*> '[3,4])) => [Int]+        test = fromType (Proxy @r)+    test +      `shouldBe` +      [(+) 1,(+) 2] <*> [3,4]+  it ">>= [] instance" $ do+    let test :: forall r. (r ~ Eval ('[5,6,7] >>= Plus2M)) => [Int]+        test = fromType (Proxy @r)+    test +      `shouldBe` +      ([5,6,7] >>= (\n -> [n + 2, n + 3]))+  it ">>= Maybe instance test Just" $ do+    let test :: forall r. (r ~ Eval ('Just "hello" >>= (Return <=< Flip (.<>) " world"))) => Maybe String+        test = fromType (Proxy @r)+    test +      `shouldBe` +      (Just "hello" <&> flip (<>) " world")+      -- Above was suggested by hlint for the following:+      -- (Just "hello" >>= (return . flip (<>) " world"))+  it ">>= Maybe instance test Nothing" $ do+    let test :: forall r. (r ~ Eval ('Nothing >>= (Return <=< Flip (.<>) " world"))) => Maybe String+        test = fromType (Proxy @r)+    test +      `shouldBe` +      (Nothing <&> flip (<>) " world")+      -- Above was suggested by hlint for the following:+      -- (Nothing >>= (return . flip (<>) " world"))+  it ">> Maybe instance" $ do+    let test :: forall r. (r ~ Eval ('Just 5 >> 'Just "hello world")) => Maybe String+        test = fromType (Proxy @r)+    test +      `shouldBe` +      (Just (5 :: Int) >> Just "hello world")

@@ -1,7 +1,12 @@  module Test.Data where -import           Test.Data.Reflect as R (tests)+import           Test.Data.Reflect as R (spec)+import           Test.Data.Set as S (spec)+import           Test.Hspec (describe, Spec) -tests = R.tests+spec :: Spec+spec = describe "Data" $ do +  R.spec+  S.spec 

@@ -1,10 +1,10 @@ {-# LANGUAGE CPP                    #-} {-# LANGUAGE ScopedTypeVariables    #-}-{-# LANGUAGE TypeApplications       #-} {-# LANGUAGE TypeFamilies           #-}-{-# LANGUAGE TypeInType             #-}+{-# LANGUAGE TypeApplications       #-}+{-# LANGUAGE RankNTypes             #-}+{-# LANGUAGE DataKinds              #-} {-# LANGUAGE TypeOperators          #-}-{-# LANGUAGE UndecidableInstances   #-} {-# OPTIONS_GHC -Wall                       #-} {-# OPTIONS_GHC -Werror=incomplete-patterns #-} @@ -18,6 +18,7 @@ import qualified Data.Text as DTxt #endif import           Data.Proxy+import           Test.Hspec (describe, it, shouldBe, Spec)  import           Fcf (Eval, type (=<<)) import qualified Fcf.Data.Set as FS@@ -29,71 +30,227 @@ import qualified Fcf.Data.Tree as FT import           Fcf.Data.Reflect -tests :: Bool-tests = -     testNatMap-  && testMap-  && testSet-#if __GLASGOW_HASKELL__ >= 902-  && testText-#endif-  && testTree+-------------------------------------------------------------------------------- -testNatMap -  :: forall r. (r ~ Eval (FNM.Insert 3 "hih" =<< FNM.FromList '[ '(1,"haa"), '(2,"hoo")])) -  => Bool-testNatMap = result == expected-  where-    result   = fromType @r Proxy :: IM.IntMap String-    expected = IM.fromList [ (3, "hih"), (1, "haa"), (2, "hoo")]+spec :: Spec+spec = describe "Reflect" $ do+  specMaybe+  specEither+  specMaybeEither+  specStructures+  specTrees+  +specBool :: Spec+specBool = describe "Bool" $ do+  it "Bool, True" $ do+    let test :: forall r. (r ~ 'True) => Bool+        test = fromType (Proxy @r)+    test `shouldBe` True+  it "Bool, False" $ do+    let test :: forall r. (r ~ 'False) => Bool+        test = fromType (Proxy @r)+    test `shouldBe` False -testMap -  :: forall r. (r ~ Eval (FNMC.Insert 3 "hih" =<< FNMC.FromList '[ '(1,"haa"), '(2,"hoo")])) -  => Bool-testMap = result == expected-  where-    result   = fromType @r Proxy :: DM.Map Int String-    expected = DM.fromList [ (3, "hih"), (1, "haa"), (2, "hoo")]+specMaybe :: Spec+specMaybe = describe "Maybe" $ do+  it "Maybe Int, Just" $ do+    let test :: forall r. (r ~ 'Just 5) +             => Maybe Int+        test = fromType (Proxy @r)+    test `shouldBe` Just 5+  it "Maybe Int, Nothing" $ do+    let test :: forall r. (r ~ 'Nothing) +             => Maybe Int+        test = fromType (Proxy @r)+    test `shouldBe` Nothing+  it "Maybe String, Just" $ do+    let test :: forall r. (r ~ 'Just "just") +             => Maybe String+        test = fromType (Proxy @r)+    test `shouldBe` Just "just"+  it "Maybe String, Nothing" $ do+    let test :: forall r. (r ~ 'Nothing) +             => Maybe String+        test = fromType (Proxy @r)+    test `shouldBe` Nothing -testSet-  :: forall r. (r ~ Eval (FS.FromList '[5, 9, 1, 8, 3, 5]))-  => Bool-testSet = result == expected-  where-    result   = fromType @r Proxy :: DS.Set Int-    expected = DS.fromList [1, 3, 5, 8, 9]-  +specEither :: Spec+specEither = describe "Either" $ do+  it "Either Int String, Left" $ do+    let test :: forall r. (r ~ 'Left 5) +             => Either Int String+        test = fromType (Proxy @r)+    test `shouldBe` Left 5+  it "Either Int String, Right" $ do+    let test :: forall r. (r ~ 'Right "right") +             => Either Int String+        test = fromType (Proxy @r)+    test `shouldBe` Right "right"+  it "Either Int (Either Int String), Right Right" $ do+    let test :: forall r. (r ~ 'Right ('Right "right"))+             => Either Int (Either Int String)+        test = fromType (Proxy @r)+    test `shouldBe` Right (Right "right")+  it "Either (Either Int String) String, Left Left" $ do+    let test :: forall r. (r ~ 'Left ('Left 5)) +             => Either (Either Int String) String+        test = fromType (Proxy @r)+    test `shouldBe` Left (Left 5) -type ExT1r =+specMaybeEither :: Spec+specMaybeEither = describe "Maybe Either and Either Maybe" $ do+  it "Either Int (Maybe String), Right Just" $ do+    let test :: forall r. (r ~ 'Right ('Just "right just"))+             => Either Int (Maybe String)+        test = fromType (Proxy @r)+    test `shouldBe` Right (Just "right just")+  it "Either Int (Maybe String), Right Nothing" $ do+    let test :: forall r. (r ~ 'Right 'Nothing)+             => Either Int (Maybe String)+        test = fromType (Proxy @r)+    test `shouldBe` Right Nothing+  it "Maybe (Either Int String), Just Right" $ do+    let test :: forall r. (r ~ 'Just ('Right "just right"))+             => Maybe (Either Int String)+        test = fromType (Proxy @r)+    test `shouldBe` Just (Right "just right")+  it "Maybe (Either Int String), Nothing" $ do+    let test :: forall r. (r ~ 'Nothing)+             => Maybe (Either Int String)+        test = fromType (Proxy @r)+    test `shouldBe` Nothing+++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]+#if __GLASGOW_HASKELL__ >= 902+  it "text" $ do+    let test :: forall r. (r ~ 'FTxt.Text "trial") => DTxt.Text+        test = fromType (Proxy @r)+    test +      `shouldBe` +      DTxt.pack "trial"+#endif++type ExTr1 =     'FT.Node 1         '[ 'FT.Node 2            '[ 'FT.Node 3 '[ 'FT.Node 4 '[]]]         , 'FT.Node 5 '[ 'FT.Node 6 '[]]         ] --- type ExTr2 =---     'Node ('Just 1)---         '[ 'Node ('Just 2)---             '[ 'Node ('Just 3)---                 '[ 'Node ('Just 4) '[]]---              ]---          , 'Node ('Just 5)---             '[ 'Node ('Just 6) '[]---              ]---          ]+type ExTr2 =+    'FT.Node ('Just 1)+        '[ 'FT.Node ('Just 2)+            '[ 'FT.Node ('Just 3)+                '[ 'FT.Node ('Just 4) '[]]+             ]+         , 'FT.Node ('Just 5)+            '[ 'FT.Node ('Just 6) '[]+             ]+         ] +type ExTr3 =+    'FT.Node ('Just 1)+        '[ 'FT.Node ('Just 2)+            '[ 'FT.Node ('Just 3)+                '[ 'FT.Node ('Just 4) '[]]+             ]+         , 'FT.Node ('Just 5)+            '[ 'FT.Node 'Nothing '[]+             ]+         ] -testTree :: forall r. (r ~ ExT1r) => Bool-testTree = result == expected-  where-    result   = fromType @r Proxy :: DT.Tree Int-    expected = DT.Node 1 [DT.Node 2 [DT.Node 3 [DT.Node 4 []]], DT.Node 5 [DT.Node 6 []]]-    +type ExTr4 =+    'FT.Node ('Left 1)+        '[ 'FT.Node ('Right "two")+            '[ 'FT.Node ('Left 3)+                '[ 'FT.Node ('Right "four") '[]]+             ]+         , 'FT.Node ('Left 5)+            '[ 'FT.Node ('Right "six") '[]+             ]+         ]     -#if __GLASGOW_HASKELL__ >= 902-testText :: forall r. (r ~ 'FTxt.Text "trial") => Bool-testText = result == expected-  where-    result   = fromType @r Proxy :: DTxt.Text-    expected = DTxt.pack "trial"-#endif+specTrees :: Spec+specTrees = describe "Tree structures" $ do+  it "tree 1" $ do+    let test :: forall r. (r ~ ExTr1) +             => DT.Tree Int+        test = fromType (Proxy @r)+    test +      `shouldBe` +      DT.Node 1 [DT.Node 2 [DT.Node 3 [DT.Node 4 []]], DT.Node 5 [DT.Node 6 []]]+  it "tree 2" $ do+    let test :: forall r. (r ~ ExTr2) +             => DT.Tree (Maybe Int)+        test = fromType (Proxy @r)+    test +      `shouldBe` +      DT.Node (Just 1) +        [ DT.Node (Just 2) +          [ DT.Node (Just 3) +            [ DT.Node (Just 4) []+            ]+          ]+        , DT.Node (Just 5) +          [DT.Node (Just 6) []+          ]+        ]+  it "tree 3" $ do+    let test :: forall r. (r ~ ExTr3) +             => DT.Tree (Maybe Int)+        test = fromType (Proxy @r)+    test +      `shouldBe` +      DT.Node (Just 1) +        [ DT.Node (Just 2) +          [ DT.Node (Just 3) +            [ DT.Node (Just 4) []+            ]+          ]+        , DT.Node (Just 5) +          [DT.Node Nothing []+          ]+        ]+  it "tree 4" $ do+    let test :: forall r. (r ~ ExTr4) +             => DT.Tree (Either Int String)+        test = fromType (Proxy @r)+    test +      `shouldBe` +      DT.Node (Left 1) +        [ DT.Node (Right "two") +          [ DT.Node (Left 3) +            [ DT.Node (Right "four") []+            ]+          ]+        , DT.Node (Left 5) +          [DT.Node (Right "six") []+          ]+        ]

@@ -0,0 +1,221 @@+{-# LANGUAGE CPP                    #-}+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeApplications       #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE RankNTypes             #-}+{-# LANGUAGE DataKinds              #-}+{-# OPTIONS_GHC -Wall                       #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++module Test.Data.Set where++import           Data.Proxy+import           Data.Type.Equality ((:~:)(Refl))+import           Test.Hspec (describe, it, shouldBe, Spec)+import qualified Data.Set as DS++import           Fcf (Eval, type (=<<), Map)+import           Fcf.Data.Nat+import           Fcf.Data.Set+import           Fcf.Data.Reflect (fromType)+import           Fcf.Alg.Sort++--------------------------------------------------------------------------------++-- > :kind! Eval (Size =<< FromList '[5, 3])+-- Eval (Size =<< FromList '[5, 3]) :: TL.Natural+-- = 2++spec :: Spec+spec = describe "Set" $ do+  it "PowerSet" $ do+    let test :: forall r. (r ~ Eval (PowerSet  =<< FromList '[1,2,9,5])) => DS.Set (DS.Set Int)+        test = fromType (Proxy @r)+    test +      `shouldBe` +      DS.powerSet (DS.fromList [1,2,9,5])+  it "Size" $ do+    let test :: forall r. (r ~ Eval (Size  =<< FromList '[5,3])) => Int+        test = fromType (Proxy @r)+    test `shouldBe` 2++--------------------------------------------------------------------------------++-- This module won't compile, if the Refl doesn't give the correct answer.+--+-- > :kind! (Eval Empty :: Set Nat)+-- (Eval Empty :: Set Nat) :: Set TL.Natural+-- = 'Set '[]+_ = Refl :: (Eval Empty :: Set Nat)+  :~: 'Set '[]+++-- This module won't compile, if the Refl doesn't give the correct answer.+--+-- > :kind! Eval (Singleton 1)+-- Eval (Singleton 1) :: Set TL.Natural+-- = 'Set '[1]+_ = Refl :: Eval (Singleton 1)+  :~: 'Set '[1]+++-- > :kind! Eval (Insert 3 =<< FromList '[1, 2])+-- Eval (Insert 3 =<< FromList '[1, 2]) :: Set TL.Natural+-- = 'Set '[3, 1, 2]+_ = Refl :: Eval (Insert 3 =<< FromList '[1, 2])+  :~: 'Set '[3, 1, 2]++-- > :kind! Eval (Insert 2 =<< FromList '[1, 2])+-- Eval (Insert 2 =<< FromList '[1, 2]) :: Set TL.Natural+-- = 'Set '[1, 2]+_ = Refl :: Eval (Insert 2 =<< FromList '[1, 2])+  :~: 'Set '[1, 2]++-- > :kind! Eval (Delete 5 =<< FromList '[5, 3])+-- Eval (Delete 5 =<< FromList '[5, 3]) :: Set TL.Natural+-- = 'Set '[3]+_ = Refl :: Eval (Delete 5 =<< FromList '[5, 3])+  :~: 'Set '[3]++-- > :kind! Eval (Delete 7 =<< FromList '[5, 3])+-- Eval (Delete 7 =<< FromList '[5, 3]) :: Set TL.Natural+-- = 'Set '[5, 3]+_ = Refl :: Eval (Delete 7 =<< FromList '[5, 3])+  :~: 'Set '[5, 3]++-- > :kind! Eval (Member 5 =<< FromList '[5, 3])+-- Eval (Member 5 =<< FromList '[5, 3]) :: Bool+-- = 'True+_ = Refl :: Eval (Member 5 =<< FromList '[5, 3])+  :~: 'True++-- > :kind! Eval (Member 7 =<< FromList '[5, 3])+-- Eval (Member 7 =<< FromList '[5, 3]) :: Bool+-- = 'False+_ = Refl :: Eval (Member 7 =<< FromList '[5, 3])+  :~: 'False++-- > :kind! Eval (NotMember 5 =<< FromList '[5, 3])+-- Eval (NotMember 5 =<< FromList '[5, 3]) :: Bool+-- = 'False+_ = Refl :: Eval (NotMember 5 =<< FromList '[5, 3])+  :~: 'False+++-- > :kind! Eval (NotMember 7 =<< FromList '[5, 3])+-- Eval (NotMember 7 =<< FromList '[5, 3]) :: Bool+-- = 'True+_ = Refl :: Eval (NotMember 7 =<< FromList '[5, 3])+  :~: 'True++-- > :kind! Eval (Null =<< FromList '[5, 3])+-- Eval (Null =<< FromList '[5, 3]) :: Bool+-- = 'False+_ = Refl :: Eval (Null =<< FromList '[5, 3])+  :~: 'False++-- > :kind! Eval (Null =<< Empty)+-- Eval (Null =<< Empty) :: Bool+-- = 'True+_ = Refl :: Eval (Null =<< Empty)+  :~: 'True++-- > :kind! Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4]))+-- Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4])) :: Bool+-- = 'True+_ = Refl :: Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4]))+  :~: 'True++-- > :kind! Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4]))+-- Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4])) :: Bool+-- = 'True+_ = Refl :: Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4]))+  :~: 'True++-- > :kind! Eval (IsSubsetOf ('Set '[0,2,1,3,4]) ('Set '[0,1,2,3,4]))+-- Eval (IsSubsetOf ('Set '[0,2,1,3,4]) ('Set '[0,1,2,3,4])) :: Bool+-- = 'True+_ = Refl :: Eval (IsSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4]))+  :~: 'True++-- > :kind! Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4]))+-- Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4])) :: Bool+-- = 'False+_ = Refl :: Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4]))+  :~: 'False++-- > :kind! Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4]))+-- Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4])) :: Bool+-- = 'False+_ = Refl :: Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4]))+  :~: 'False++-- > :kind! Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4]))+-- Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4])) :: Bool+-- = 'True+_ = Refl :: Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4]))+  :~: 'True++-- > :kind! Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) )+-- Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) ) :: Set+--                                                                        TL.Natural+-- = 'Set '[7, 5, 3]+_ = Refl ::  Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) )+  :~: 'Set '[7, 5, 3]++-- > :kind! Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))+-- Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) :: Set+--                                                                            TL.Natural+-- = 'Set '[3]+_ = Refl :: Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))+  :~: 'Set '[3]++-- > :kind! Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))+-- Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) :: Set+--                                                                              TL.Natural+-- = 'Set '[5]+_ = Refl :: Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) +  :~: 'Set '[5]++-- > :kind! Eval (PowerSet =<< FromList '["a", "b", "c"])+-- Eval (PowerSet =<< FromList '["a", "b", "c"]) :: Set+--                                                    (Set TL.Symbol)+-- = 'Set+--     '[ 'Set '[], 'Set '["c"], 'Set '["b"], 'Set '["b", "c"],+--        'Set '["a"], 'Set '["a", "b"], 'Set '["a", "c"],+--        'Set '["a", "b", "c"]]+--+-- > :kind! Eval (PowerSet =<< FromList '[Int, Char, Maybe Int])+-- Eval (PowerSet =<< FromList '[Int, Char, Maybe Int]) :: Set+--                                                           (Set (*))+-- = 'Set+--     '[ 'Set '[], 'Set '[Maybe Int], 'Set '[Char],+--        'Set '[Char, Maybe Int], 'Set '[Int], 'Set '[Int, Char],+--        'Set '[Int, Maybe Int], 'Set '[Int, Char, Maybe Int]]+_ = Refl :: Eval (PowerSet =<< FromList '[Int, Char, Maybe Int])+  :~: 'Set+    '[ 'Set '[], 'Set '[Maybe Int], 'Set '[Char],+       'Set '[Char, Maybe Int], 'Set '[Int], 'Set '[Int, Char],+       'Set '[Int, Maybe Int], 'Set '[Int, Char, Maybe Int]]++-- > :kind! Eval (FromList '[1, 2])+-- Eval (FromList '[1, 2]) :: Set TL.Natural+-- = 'Set '[1, 2]+_ = Refl :: Eval (FromList '[1, 2])+  :~: 'Set '[1, 2]++-- > :kind! Eval (ToList =<< PowerSet =<< FromList '[1,2,3])+-- Eval (ToList =<< PowerSet =<< FromList '[1,2,3]) :: [Set+--                                                        TL.Natural]+-- = '[ 'Set '[], 'Set '[3], 'Set '[2], 'Set '[2, 3], 'Set '[1],+--      'Set '[1, 2], 'Set '[1, 3], 'Set '[1, 2, 3]]+_ = Refl :: Eval (ToList =<< PowerSet =<< FromList '[1,2,3])+  :~: '[ 'Set '[], 'Set '[3], 'Set '[2], 'Set '[2, 3], 'Set '[1],+         'Set '[1, 2], 'Set '[1, 3], 'Set '[1, 2, 3]]++-- > :kind! Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3])+-- Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3]) :: [[TL.Natural]]+-- = '[ '[], '[1], '[1, 2], '[1, 2, 3], '[1, 3], '[2], '[2, 3], '[3]]+_ = Refl :: Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3])+  :~: '[ '[], '[1], '[1, 2], '[1, 2, 3], '[1, 3], '[2], '[2, 3], '[3]]

@@ -1,34 +1,33 @@ {-# LANGUAGE     DataKinds,     KindSignatures,+    TypeFamilies,+    UndecidableInstances,     TypeOperators #-}  --------------------------------------------------------------------------------  import           Data.Type.Equality ((:~:)(Refl))-import           GHC.TypeLits (Nat)-import           Fcf+import           GHC.TypeLits (Nat, Symbol)+import           Fcf hiding (type (<*>))  --------------------------------------------------------------------------------  import           Fcf.Data.Set+import           Fcf.Control.Monad+import           Fcf.Data.Tuple+import           Fcf.Class.Monoid+import           Fcf.Data.List  -------------------------------------------------------------------------------- -import           Test.Data (tests)------ Compile-time tests--_ = Refl :: Eval (ToList =<< PowerSet  =<< FromList '[1,2])-        :~: '[ 'Set '[], 'Set '[2], 'Set '[1], 'Set '[1,2]]---- Dummy+import           Test.Alg as A (spec)+import           Test.Data as D (spec)+import           Test.Control as C (spec)+import           Test.Hspec (hspec, parallel)  main :: IO ()-main = -  if tests -    then pure ()-    else error "Tests not ok."-+main = hspec $ parallel $ do+  D.spec+  C.spec+  A.spec