fcf-containers (empty) → 0.1.0
raw patch · 15 files changed
+1794/−0 lines, 15 filesdep +Globdep +basedep +doctest
Dependencies added: Glob, base, doctest, first-class-families
Files
- CHANGELOG.md +5/−0
- LICENSE +30/−0
- README.md +79/−0
- TODO.md +55/−0
- default.nix +54/−0
- examples/Orbits.hs +120/−0
- fcf-containers.cabal +74/−0
- shell.nix +9/−0
- src/Fcf/Alg/List.hs +182/−0
- src/Fcf/Alg/Morphism.hs +137/−0
- src/Fcf/Alg/Tree.hs +181/−0
- src/Fcf/Data/MapC.hs +495/−0
- src/Fcf/Data/Set.hs +221/−0
- src/Fcf/Data/Tree.hs +136/−0
- test/doctest.hs +16/−0
+ CHANGELOG.md view
@@ -0,0 +1,5 @@++# 0.1.0.0++Initial version on 20200129. The next version probably comes out quickly after +this one.
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2020, gspia++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of gspia nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,79 @@+# fcf-containers++Fcf-containers mimicks the containers package but for type-level computations. +That is, we provide e.g. trees and maps. In addition to that, this package +contains some other type-level computation utilities. ++These methods are based on the idea given in the+[first-class-families](https://github.com/Lysxia/first-class-families) -package,+or Fcf shortly. Fcf is the main dependency of fcf-containers. As some of the+methods fit badly under the name "fcf-containers", they might end up into +the Fcf or some other package to be created. So stay tuned, be patient, check +the [TODO.md](https://github.com/gspia/fcf-containers/blob/master/TODO.md) +and send those PR's :)+++Motivation for calculating things on type-level or on compile-time +include++- increase the safety measures of runtime methods,+- pre-calculate complex things once on compile time and not every time the+ executable is run, +- provide users a way to choose between different algorithms for solving+ a problem based on problem instance properties (e.g. local vs network,+ or small vs large) known in advance.+ +Why fcf-like? The kind of signatures used for functions might be easier to +read for some people and the ability to apply partially a function is nice +tool to have.+ +If you have other motivations, please do let us know! ++Note: some of the claims on the items in the above list are such that I +believe/hope but really don't know at the moment nor do I know how check them. +E.g. the matter of compile time vs run time. Yes, types are erased at compile +time but do they still leave something into executables: simple check by +comparing outputs of the orbit example and another program that has one method +to print integer 42 and main, reveals that sizes are almost the same, but not +exactly.+++There are lot of open interesting questions. See +[TODO.md](https://github.com/gspia/fcf-containers/blob/master/TODO.md) file. E.g. how combine +these techniques with singletons-lib and related techniques. ++++## Installation and building ++First, get the repo with `git clone` and `cd` into the directory. ++```+nix-shell +cabal build +cabal test +```++The doc-tests both document and work as main testing mechanism for this lib. ++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++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.++```+cabal run orbits +```++The `ghci` and `:kind!` command in there are your friends!++Source also contains a lot of examples, see+[fcf-containers](https://github.com/gspia/fcf-containers/tree/master/src/Fcf).+++Happy :kinding!
+ TODO.md view
@@ -0,0 +1,55 @@+# TODO++## Examples:++E.g. add examples using the other data structures.++## Data structures:++Add the missing methods and doctests.++- Set+- NatMap+- Graphs+- MapB (Map data structure) but implemented with the balanced trees+- MapC + ++## Morphisms:+ +- Para with examples+- Histo with examples+- Apo with examples+- Futu with examples+- and other + +Also, consider moving morphisms into another package. ++At the moment, this lib provides `<DataStructure>ToFix`-functions. It would be +really nice to have one method that could be overloaded, called e.g. `ToFix`. +This would allow us to implement the morphisms similarly as in the term-level +libs without a need for the user to do fixing. Doable?++The current definition of `Fix` might be too simple for other morphisms.+++## Other things++Start using module exports.++Some of the names are really really bad/horrible. Suggestions are wellcome.+And there might be a need to some internal reorganisations of the methods between+modules.++Further, there are several methods that might have a better fit in the Fcf-lib.+(And some will be on the next published version of fcf and thus will be removed+from this fcf-containers.)++How to check if everything is really done compile time? Or alternatively, how+to check, which parts are done on compile time and what is left to run time.++Error messages... yeah, try it, you get what you write :) At the moment this+can be quite confusing occasionally. Is there a way to improve these?++Examples on how to use these with singletons? Maybe in another package?+
+ default.nix view
@@ -0,0 +1,54 @@+{ + # compiler ? "ghc881" +} :+let+ config = {+ packageOverrides = pkgs: rec {+ haskellPackages = pkgs.haskellPackages.override {+ /* overrides = haskellPackagesNew: haskellPackagesOld: rec { */+ overrides = self: super: rec {+ /* aeson = haskellPackagesNew.callPackage ./aeson.nix { }; */+ ghc = super.ghc // { withPackages = super.ghc.withHoogle; };+ ghcWithPackages = self.ghc.withPackages;+ first-class-families = self.callCabal2nix "first-class-families" + # ~/gito/first-class-families {}; + (pkgs.fetchFromGitHub { # 0.6+ owner = "Lysxia";+ repo = "first-class-families";+ rev = "2fb77468d3b0ce64dc5371bed1b636d60219975c";+ sha256 = "1jvn11nbb7271hhy7q21cyn4r238pfzj00aabd39gwhi0g2gzqbf";+ }) {};+ };+ };+ };+ allowUnfree = true;+ };+ nixpkgs = import <nixpkgs> { inherit config; };+ pkgs = nixpkgs.pkgs;+ hpkgs = pkgs.haskellPackages;+ # hpkgs = pkgs.haskell.packages.${compiler};++ adjust-for-ghc = drv: {+ executableSystemDepends = [+ hpkgs.ghcid+ hpkgs.cabal-install+ ];+ buildDepends = [+ hpkgs.hlint+ # hpkgs.ghc-mod+ # hpkgs.hasktags+ # hpkgs.haskdogs # stack config set system-ghc --global true + # hpkgs.hindent+ # hpkgs.hsimport+ # hpkgs.pointfree+ # hpkgs.pointful+ # hpkgs.stylish-haskell+ ];+ };++ adjust = adjust-for-ghc;++ exe-code-base = hpkgs.callCabal2nix "fcf-containers" ./. {};+ exe-code = pkgs.haskell.lib.overrideCabal exe-code-base adjust;+in+ exe-code
+ examples/Orbits.hs view
@@ -0,0 +1,120 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|++Example on how to do compile-time (ie type-level) computations and how+to get the results into use on term-level (ie runtime).++The original problem is described in +[aoc 19 d6](https://adventofcode.com/2019/day/6). We use the described+example input data in a bit different form. See the link for the+original data and answer.++-}++--------------------------------------------------------------------------------++import qualified GHC.TypeLits as TL++import Data.Proxy++import Fcf+import Fcf.Data.Nat+import Fcf.Data.List as L++import Fcf.Alg.Morphism+import Fcf.Alg.List+import Fcf.Alg.Tree++--------------------------------------------------------------------------------+++-- | Type-level variable containing all the required information.+data OrbitInput :: Exp [(TL.Symbol, TL.Symbol)]+type instance Eval OrbitInput =+ '[ '("COM", "B")+ , '("B", "C")+ , '("C", "D")+ , '("D", "E")+ , '("E", "F")+ , '("B", "G")+ , '("G", "H")+ , '("D", "I")+ , '("E", "J")+ , '("J", "K")+ , '("K", "L")]++-- helper, we might could do without this one+-- This is used to check that two symbols are same.+data EqPlanet :: TL.Symbol -> TL.Symbol -> Exp Bool+type instance Eval (EqPlanet a b) = Eval (TyEq 'EQ (TL.CmpSymbol a b))++-- | :kind! Eval (FindDescs "COM" =<< OrbitInput)+data FindDescs :: TL.Symbol -> [(TL.Symbol, TL.Symbol)] -> Exp [TL.Symbol]+type instance Eval (FindDescs p lst) = + Eval (Map Snd =<< (Filter (EqPlanet p <=< Fst) lst))++-- | This is not used in the final solution but worked as a step towards it.+-- +-- :kind! Eval (Ana BuildOrbTreeCoA "COM")+data BuildOrbTreeCoA :: CoAlgebra (TreeF TL.Symbol) TL.Symbol+type instance Eval (BuildOrbTreeCoA nd) =+ If (Eval (L.Null (Eval (FindDescs nd =<< OrbitInput))))+ ('NodeF nd '[])+ ('NodeF nd (Eval (FindDescs nd =<< OrbitInput)))++-- | +-- We need to store the depth of the node along the tree. We use the depth when+-- counting paths from root to every node.+--+-- :kind! Eval (Ana BuildOrbTreeCoA2 '(0,"COM"))+data BuildOrbTreeCoA2 :: CoAlgebra (TreeF (Nat,TL.Symbol)) (Nat,TL.Symbol)+type instance Eval (BuildOrbTreeCoA2 '(d,nd)) =+ If (Eval (L.Null (Eval (FindDescs nd =<< OrbitInput))))+ ('NodeF '(d,nd) '[])+ ('NodeF '(d,nd) (Eval (MkPairLst (1 TL.+ d) =<< FindDescs nd =<< OrbitInput)))++-- helper, we might could do without this one+data MkPair :: Nat -> TL.Symbol -> Exp (Nat,TL.Symbol)+type instance Eval (MkPair n s) = '(n,s)++-- helper, we might could do without this one+data MkPairLst :: Nat -> [TL.Symbol] -> Exp [(Nat,TL.Symbol)]+type instance Eval (MkPairLst n lst) = Eval (Map (MkPair n) lst)+++-- | Count paths from root to every node.+-- +-- If it is a leaf, the number of paths from root to it is the depth.+-- If it is an internal node, the number of paths to the subtree rooted +-- by it is sum of pathnums of subtrees plus the depth (paths to this one).+data CountPathsAlg :: Algebra (TreeF (Nat,TL.Symbol)) Nat+type instance Eval (CountPathsAlg ('NodeF '(d,_) '[])) = d+type instance Eval (CountPathsAlg ('NodeF '(d,_) (b ': bs))) = d TL.+ (Eval (Sum (b ': bs)))+++-- | We initialize this with the known starting node and the depth of it, which +-- is 0.+--+-- :kind! Eval OrbitSolution+data OrbitSolution :: Exp Nat+type instance Eval OrbitSolution =+ Eval (Hylo CountPathsAlg BuildOrbTreeCoA2 '(0,"COM"))++-- | Helper to bring in the result of the type-level computation.+-- +-- It is a nice exercise to solve this using Tree, UnfoldTree and FoldTree.+showResult :: forall n. (n ~ Eval OrbitSolution) => String+showResult = show $ TL.natVal @n Proxy++main :: IO ()+main = putStrLn $ "Number of orbits is " <> showResult
+ fcf-containers.cabal view
@@ -0,0 +1,74 @@+Name: fcf-containers+Synopsis: Data structures and algorithms for first-class-families+Description:+ Package fcf-containers provides type-level functions and data structures+ that operate on type-level computations. Specifically, we mimick the+ 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.1.0+Build-type: Simple+Author: gspia+Maintainer: iahogsp@gmail.com+License: BSD3+License-file: LICENSE+Category: Other+Copyright: gspia (c) 2020-+Extra-source-files: README.md, TODO.md, CHANGELOG.md, default.nix, shell.nix+Cabal-version: 1.24++library+ hs-source-dirs: src+ exposed-modules: Fcf.Data.MapC+ , Fcf.Data.Tree+ , Fcf.Data.Set+ , Fcf.Alg.List+ , Fcf.Alg.Tree+ , Fcf.Alg.Morphism+ build-depends: base >= 4.9 && < 4.13+ , first-class-families >= 0.6 && < 0.7+ ghc-options: -Wall+ default-language: Haskell2010+ -- ghc-options:+ -- -O2+++Executable orbits+ hs-source-dirs: examples,src+ main-is: Orbits.hs+ default-language: Haskell2010+ other-modules: Fcf.Alg.Morphism+ , Fcf.Alg.List+ , Fcf.Alg.Tree+ , Fcf.Data.Tree+ build-depends: base+ , first-class-families+ -- ghc-options:+ -- -ddump-simpl+ -- -O2++-- test-suite fcf-test+-- type: exitcode-stdio-1.0+-- hs-source-dirs: test+-- main-is: test.hs+-- default-language: Haskell2010+-- build-depends:+-- base+-- , first-class-families++test-suite fcf-doctest+ type: exitcode-stdio-1.0+ hs-source-dirs: test+ main-is: doctest.hs+ default-language: Haskell2010+ if impl(ghc >= 8.6)+ build-depends:+ base,+ doctest,+ Glob+ else+ buildable: False++source-repository head+ type: git+ location: https://github.com/gspia/fcf-containers
+ shell.nix view
@@ -0,0 +1,9 @@+{ 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
+ src/Fcf/Alg/List.hs view
@@ -0,0 +1,182 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|+Module : Fcf.Alg.List+Description : ListF structure working with Algebras, ColAlgebras, and other stuff+Copyright : (c) gspia 2020-+License : BSD+Maintainer : gspia++= Fcf.Alg.List++Type-level 'ListF' to be used with Cata, Ana and Hylo.++This module also contains other list-related functions (that might move to+other place some day).++-}++--------------------------------------------------------------------------------++module Fcf.Alg.List where++import qualified GHC.TypeLits as TL++import Fcf+import Fcf.Data.Nat++import Fcf.Alg.Morphism++--------------------------------------------------------------------------------++-- | Base functor for a list of type @[a]@.+data ListF a b = ConsF a b | NilF++-- We need a functor instance for Cata and Ana to work.+type instance Eval (Map f 'NilF) = 'NilF+type instance Eval (Map f ('ConsF a b)) = 'ConsF a (Eval (f b))+++-- | ListToFix can be used to turn a norma type-level list into the base+-- functor type ListF, to be used with e.g. Cata. For examples in use, see+-- 'LenAlg' and 'SumAlg'.+-- +-- Ideally, we would have one ToFix type-level function for which we could+-- give type instances for different type-level types, like lists, trees+-- etc. See TODO.md.+data ListToFix :: [a] -> Exp (Fix (ListF a))+type instance Eval (ListToFix '[]) = 'Fix 'NilF+type instance Eval (ListToFix (a ': as)) = 'Fix ('ConsF a (Eval (ListToFix as)))++-- | Example algebra to calculate list length.+-- +-- >>> :kind! Eval (Cata LenAlg =<< ListToFix '[1,2,3])+-- Eval (Cata LenAlg =<< ListToFix '[1,2,3]) :: Nat+-- = 3+data LenAlg :: Algebra (ListF a) Nat+type instance Eval (LenAlg 'NilF) = 0+type instance Eval (LenAlg ('ConsF a b)) = 1 TL.+ b++-- | Example algebra to calculate the sum of Nats in a list.+-- +-- >>> :kind! Eval (Cata SumAlg =<< ListToFix '[1,2,3,4])+-- Eval (Cata SumAlg =<< ListToFix '[1,2,3,4]) :: Nat+-- = 10+data SumAlg :: Algebra (ListF Nat) Nat+type instance Eval (SumAlg 'NilF) = 0+type instance Eval (SumAlg ('ConsF a b)) = a TL.+ b++-- | Example algebra to calculate the prod of Nats in a list.+--+-- >>> :kind! Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4])+-- Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4]) :: Nat+-- = 24+data ProdAlg :: Algebra (ListF Nat) Nat+type instance Eval (ProdAlg 'NilF) = 1+type instance Eval (ProdAlg ('ConsF a b)) = a TL.* b++--------------------------------------------------------------------------------++-- | Sum a Nat-list.+--+-- __Example__+--+-- >>> :kind! Eval (Sum '[1,2,3])+-- Eval (Sum '[1,2,3]) :: Nat+-- = 6+data Sum :: [Nat] -> Exp Nat+type instance Eval (Sum ns) = Eval (Foldr (+) 0 ns)++--------------------------------------------------------------------------------++-- | Partition+-- +-- __Example__+-- +-- >>> :kind! Eval (Fcf.Alg.List.Partition ((>=) 35) '[ 20, 30, 40, 50])+-- Eval (Fcf.Alg.List.Partition ((>=) 35) '[ 20, 30, 40, 50]) :: ([Nat],+-- [Nat])+-- = '( '[20, 30], '[40, 50])+data Partition :: (a -> Exp Bool) -> [a] -> Exp ([a],[a])+type instance Eval (Partition p lst) = Eval (Foldr (PartHelp p) '( '[], '[]) lst)++data PartHelp :: (a -> Exp Bool) -> a -> ([a],[a]) -> Exp ([a],[a])+type instance Eval (PartHelp p a '(xs,ys)) =+ If (Eval (p a))+ '(a ': xs, ys)+ '(xs, a ': ys)++++-- | Type-level `Elem` for lists.+--+-- === __Example__+--+-- >>> :kind! Eval (Elem 1 '[1,2,3])+-- Eval (Elem 1 '[1,2,3]) :: Bool+-- = 'True+-- >>> :kind! Eval (Elem 1 '[2,3])+-- Eval (Elem 1 '[2,3]) :: Bool+-- = 'False+--+-- Note: Once Fcf releases a new version, I'll remove this, TODO+data Elem :: a -> [a] -> Exp Bool+type instance Eval (Elem a as) = Eval (IsJust =<< FindIndex (TyEq a) as)++-- | Concat for lists.+--+-- === __Example__+--+-- >>> :kind! Eval (Concat ( '[ '[1,2], '[3,4], '[5,6]]))+-- Eval (Concat ( '[ '[1,2], '[3,4], '[5,6]])) :: [Nat]+-- = '[1, 2, 3, 4, 5, 6]+-- >>> :kind! Eval (Concat ( '[ '[Int, Maybe Int], '[Maybe String, Either Double Int]]))+-- Eval (Concat ( '[ '[Int, Maybe Int], '[Maybe String, Either Double Int]])) :: [*]+-- = '[Int, Maybe Int, Maybe String, Either Double Int]+--+-- Note: Once Fcf releases a new version, I'll remove this, TODO+data Concat :: [[a]] -> Exp [a]+type instance Eval (Concat lsts) = Eval (Foldr (++) '[] lsts)+++-- | ConcatMap for lists.+--+-- Note: Once Fcf releases a new version, I'll remove this, TODO+data ConcatMap :: (a -> Exp [b]) -> [a] -> Exp [b]+type instance Eval (ConcatMap f lst) = Eval (Concat (Eval (Map f lst)))++-- | Type-level Unfoldr.+--+-- === __Example__+--+-- >>> data ToThree :: Nat -> Exp (Maybe (Nat, Nat))+-- >>> :{+-- type instance Eval (ToThree b) =+-- If (Eval (b Fcf.>= 4))+-- 'Nothing+-- ('Just '(b, b TL.+ 1))+-- :}+--+-- >>> :kind! Eval (Unfoldr ToThree 0)+-- Eval (Unfoldr ToThree 0) :: [Nat]+-- = '[0, 1, 2, 3]+--+-- Note: Once Fcf releases a new version, I'll remove this, TODO+data Unfoldr :: (b -> Exp (Maybe (a, b))) -> b -> Exp [a]+type instance Eval (Unfoldr f c) = Eval (UnfoldrCase f (f @@ c))++-- Helper for the Unfoldr.+-- Note: Once Fcf releases a new version, I'll remove this, TODO+data UnfoldrCase :: (b -> Exp (Maybe (a, b))) -> Maybe (a, b) -> Exp [a]+type instance Eval (UnfoldrCase f ('Just ab)) =+ Eval (Fst ab) ': Eval (Unfoldr f (Eval (Snd ab)))+type instance Eval (UnfoldrCase _ 'Nothing) = '[]++
+ src/Fcf/Alg/Morphism.hs view
@@ -0,0 +1,137 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|+Module : Fcf.Alg.Morphism+Description : Algebra, ColAlgebra, and other stuff+Copyright : (c) gspia 2020-+License : BSD+Maintainer : gspia++= Fcf.Alg.Morphism++Type-level 'Cata' and 'Ana' can be used to do complex computation that live only+on type-level or on compile-time. As an example, see the sorting algorithm+in Fcf.Alg.Tree -module.++This module also provides some other type-level functions that probably will+find other place after a while. E.g. 'First' and 'Second' and their instances+on Either and tuple.++-}++--------------------------------------------------------------------------------++module Fcf.Alg.Morphism where++import Fcf++--------------------------------------------------------------------------------++-- 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'.+data Fix f = Fix (f (Fix f))++-- | Commonly used name describing the method 'Cata' eats.+type Algebra f a = f a -> Exp a++-- | Commonly used name describing the method 'Ana' eats.+type CoAlgebra f a = a -> Exp (f a)++--------------------------------------------------------------------------------+++-- | Write the function to give a 'Fix', and feed it in together with an+-- 'Algebra'.+-- +-- Check Fcf.Alg.List to see example algebras in use.+data Cata :: Algebra f a -> Fix f -> Exp a+type instance Eval (Cata alg ('Fix b)) = alg @@ (Eval (Map (Cata alg) b))++-- | Ana can also be used to build a 'Fix' structure.+--+-- __Example__+-- +-- >>> 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)+-- Eval (Ana NToOneCoA 3) :: Fix (ListF Nat)+-- = 'Fix ('ConsF 3 ('Fix ('ConsF 2 ('Fix ('ConsF 1 ('Fix 'NilF))))))+data Ana :: CoAlgebra f a -> a -> Exp (Fix f)+type instance Eval (Ana coalg a) = 'Fix (Eval (Map (Ana coalg) (Eval (coalg a))))+++-- | +-- Hylomorphism uses first 'Ana' to build a structure (unfold) and then 'Cata'+-- to process the structure (fold).+-- +-- __Example__+-- +-- >>> 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)+-- Eval (Hylo SumAlg NToOneCoA 5) :: Nat+-- = 15+data Hylo :: Algebra f a -> CoAlgebra f b -> b -> Exp a+type instance Eval (Hylo alg coalg a) = Eval (Cata alg =<< Ana coalg a)++--------------------------------------------------------------------------------++-- | Type-level First. Tuples @(,)@ and @Either@ have First-instances.+-- +-- __Example__+-- +-- >>> :kind! Eval (First ((+) 1) '(3,"a"))+-- Eval (First ((+) 1) '(3,"a")) :: (Nat, TL.Symbol)+-- = '(4, "a")+data First :: (a -> Exp b) -> f a c -> Exp (f b c)++-- (,)+type instance Eval (First f '(a,b)) = '(f @@ a, b)++-- Either+type instance Eval (First f ('Left a)) = 'Left (f @@ a)+type instance Eval (First f ('Right b)) = 'Right b++-- | Type-level Second. Tuples @(,)@ and @Either@ have Second-instances.+-- +-- __Example__+-- +-- >>> :kind! Eval (Second ((+) 1) '("a",3))+-- Eval (Second ((+) 1) '("a",3)) :: (TL.Symbol, Nat)+-- = '("a", 4)+data Second :: (c -> Exp d) -> f a c -> Exp (f a d)++-- (,)+type instance Eval (Second f '(a,b)) = '(a, f @@ b)++-- Either+type instance Eval (Second f ('Left a)) = 'Left a+type instance Eval (Second f ('Right b)) = 'Right (f @@ b)+
+ src/Fcf/Alg/Tree.hs view
@@ -0,0 +1,181 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|+Module : Fcf.Alg.Tree+Description : Tree-structures working with Algebras, ColAlgebras, and other stuff+Copyright : (c) gspia 2020-+License : BSD+Maintainer : gspia++= Fcf.Alg.Tree++Type-level 'TreeF' and 'BTreeF' to be used with Cata, Ana and Hylo. This also+provides some algorithms: general purpose sorting with 'Qsort', 'Size' of an+Tree, Fibonaccis.++-}++--------------------------------------------------------------------------------++module Fcf.Alg.Tree where++import qualified GHC.TypeLits as TL++import Fcf+import Fcf.Data.Nat++import Fcf.Alg.List+import Fcf.Alg.Morphism +import Fcf.Data.Tree++--------------------------------------------------------------------------------++-- | 'TreeF' is functor for 'Tree's. 'TreeF' has Map-instance (on structure).+data TreeF a b = NodeF a [b]++-- provide Map instances for TreeF.+type instance Eval (Map f ('NodeF a '[])) = 'NodeF a '[]+type instance Eval (Map f ('NodeF a (b ': bs))) = 'NodeF a (Eval (Map f (b ': bs)))++-- | A function to transform a Tree into fixed structure that can be used+-- by Cata and Ana.+-- +-- See the implementation of 'Size' for an example.+data TreeToFix :: Tree a -> Exp (Fix (TreeF a))+type instance Eval (TreeToFix ('Node a '[])) = 'Fix ('NodeF a '[])+type instance Eval (TreeToFix ('Node a (b ': bs))) =+ 'Fix ('NodeF a (Eval (Map TreeToFix (b ': bs))))++--------------------------------------------------------------------------------++-- | Sum the nodes of TreeF containing Nats. +-- +-- See the implementation of 'Fib' for an example.+data SumNodesAlg :: Algebra (TreeF Nat) Nat+type instance Eval (SumNodesAlg ('NodeF x '[])) = x+type instance Eval (SumNodesAlg ('NodeF x (b ': bs))) = x TL.+ (Eval (Sum (b ': bs)))++-- | Count the nodes of TreeF. +-- +-- See the 'Size' for an example.+data CountNodesAlg :: Algebra (TreeF a) Nat+type instance Eval (CountNodesAlg ('NodeF x '[])) = 1+type instance Eval (CountNodesAlg ('NodeF x (b ': bs))) = 1 TL.+ (Eval (Sum (b ': bs)))+++-- | Size of the Tree is the number of nodes in it.+-- +-- __Example__+--+-- Size is defined as @ Cata CountNodesAlg =<< TreeToFix tr @+-- and can be used with the following. +--+-- >>> 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) :: Nat+-- = 7+data Size :: Tree a -> Exp Nat+type instance Eval (Size tr) = Eval (Cata CountNodesAlg =<< TreeToFix tr)+++-- | CoAlgebra to build TreeF's.+-- This is an example from containers-package. See 'Size' and example in there.+--+-- :kind! Eval (Ana BuildNodeCoA 1)+-- :kind! Eval (Hylo CountNodesAlg BuildNodeCoA 1)+data BuildNodeCoA :: CoAlgebra (TreeF Nat) Nat+type instance Eval (BuildNodeCoA n) =+ If (Eval (((2 TL.* n) TL.+ 1) >= 8))+ ('NodeF n '[])+ ('NodeF n '[ 2 TL.* n, (2 TL.* n) TL.+ 1 ])+ ++-- | CoAlgebra for the Fib-function.+data BuildFibTreeCoA :: CoAlgebra (TreeF Nat) Nat+type instance Eval (BuildFibTreeCoA n) =+ If (Eval (n >= 2))+ ('NodeF 0 '[n TL.- 1, n TL.- 2])+ ('NodeF n '[])+++-- | Fibonaccis with Hylo, not efficient+-- +-- __Example__+--+-- >>> :kind! Eval (Fib 10)+-- Eval (Fib 10) :: Nat+-- = 55+data Fib :: Nat -> Exp Nat+type instance Eval (Fib n) = Eval (Hylo SumNodesAlg BuildFibTreeCoA n)+++--------------------------------------------------------------------------------++-- | BTreeF is a btree functor. At the moment, it is used to build sorting+-- algorithms.+data BTreeF a b = BEmptyF | BNodeF a b b++-- functor+type instance Eval (Map f 'BEmptyF) = 'BEmptyF+type instance Eval (Map f ('BNodeF a b1 b2)) = 'BNodeF a (Eval (f b1)) (Eval (f b2))+++-- helper+data PartHlp :: (a -> a -> Exp Bool) -> CoAlgebra (BTreeF a) [a]+type instance Eval (PartHlp _ '[]) = 'BEmptyF+type instance Eval (PartHlp smaller (h ': t)) =+ 'BNodeF h+ (Eval (Filter (smaller h) t))+ (Eval (Filter (Not <=< smaller h) t))++-- | Use this if you want to sort symbols into increasing order.+data SymbolCompareInc :: TL.Symbol -> TL.Symbol -> Exp Bool+type instance Eval (SymbolCompareInc n1 n2) = Eval (TyEq (TL.CmpSymbol n1 n2) 'LT)++-- | Use this if you want to sort symbols into decreasing order.+data SymbolCompareDec :: TL.Symbol -> TL.Symbol -> Exp Bool+type instance Eval (SymbolCompareDec n1 n2) = Eval (TyEq (TL.CmpSymbol n1 n2) 'GT)+ +-- helper+data Inord :: Algebra (BTreeF a) [a]+type instance Eval (Inord 'BEmptyF) = '[]+type instance Eval (Inord ('BNodeF v l r)) = Eval (l ++ (Eval ('[v] ++ r)))+++-- | Qsort - give the comparison function @a -> a -> Exp Bool@ comparing your +-- list elements and then Qsort will order the list.+-- +-- __Example__+--+-- >>> :kind! Eval (Qsort (<) '[5,3,1,9,4,6,3])+-- Eval (Qsort (<) '[5,3,1,9,4,6,3]) :: [Nat]+-- = '[1, 3, 3, 4, 5, 6, 9]+--+-- >>> :kind! Eval (Qsort SymbolCompareInc '[ "bb", "e", "a", "e", "d" ])+-- Eval (Qsort SymbolCompareInc '[ "bb", "e", "a", "e", "d" ]) :: [TL.Symbol]+-- = '["a", "bb", "d", "e", "e"]+data Qsort :: (a -> a -> Exp Bool) -> [a] -> Exp [a]+type instance Eval (Qsort cmp lst) = Eval (Hylo Inord (PartCmp cmp) lst)++-- Helper+--+-- We use the Flip version so that using <-comparison will give an inreasing +-- 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)++
+ src/Fcf/Data/MapC.hs view
@@ -0,0 +1,495 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|+Module : Fcf.Data.MapC+Description : Map (association) data-type for the type-level programming+Copyright : (c) gspia 2020-+License : BSD+Maintainer : gspia++= Fcf.Data.MapC++MapC provides an interface to mapping keys to values, which is similar to+that given by the containers-package. Note that the this module still misses+some of the methods that can be found in containers. If you need some, please+do open up an issue or better, make a PR.++Many of the examples are from containers-package.++We call this MapC because name Map is reserved to the map-function in+Fcf-package. The internal representation is type-level list. We hope that+one day the internal representation is based on balanced trees similar to the+one used in the containers.+++-}++--------------------------------------------------------------------------------++module Fcf.Data.MapC where++import qualified GHC.TypeLits as TL++import Fcf ( Eval, Exp, Fst, Snd, type (=<<), type (<=<), type (@@)+ , type (++), Not, If+ , Pure, TyEq, Length, Uncurry)+import qualified Fcf as Fcf (Map, Foldr, Filter)+-- import Fcf.Data.List (Elem) -- TODO: change on fcf 0.7+import Fcf.Alg.List (Elem) -- TODO: change on fcf 0.7++import Fcf.Alg.Morphism+import qualified Fcf.Alg.List as Fcf (Partition)++--------------------------------------------------------------------------------++-- For the doctests:++-- $setup+-- >>> import Fcf ( type (>=), Pure1, Pure2 )+-- >>> import Fcf.Data.Nat++--------------------------------------------------------------------------------+++-- | A type corresponding to Map in the containers. We call this MapC because+-- name Map is reserved to the map-function in Fcf-package.+-- +-- The representation is based on type-level lists. Please, do not use+-- that fact but rather use the exposed API. (We hope to change the +-- internal data type to balanced tree similar to the one used in containers.+-- See TODO.md.)+data MapC k v = MapC [(k,v)]++-- | Empty+-- +-- __Example__+-- +-- >>> :kind! (Eval Empty :: MapC Nat TL.Symbol)+-- (Eval Empty :: MapC Nat TL.Symbol) :: MapC Nat TL.Symbol+-- = 'MapC '[]+--+-- >>> :kind! (Eval Empty :: MapC Int String)+-- (Eval Empty :: MapC Int String) :: MapC Int [Char]+-- = 'MapC '[]+-- +-- See also the other examples in this module.+data Empty :: Exp (MapC k v)+type instance Eval Empty = 'MapC '[]++-- | Singleton+-- +-- __Example__+-- +-- >>> :kind! Eval (Singleton 1 "haa")+-- Eval (Singleton 1 "haa") :: MapC Nat TL.Symbol+-- = 'MapC '[ '(1, "haa")]+data Singleton :: k -> v -> Exp (MapC k v)+type instance Eval (Singleton k v) = 'MapC '[ '(k,v)]++-- | Use FromList to construct a MapC from type-level list.+--+-- __Example__+-- +-- >>> :kind! Eval (FromList '[ '(1,"haa"), '(2,"hoo")])+-- Eval (FromList '[ '(1,"haa"), '(2,"hoo")]) :: MapC Nat TL.Symbol+-- = 'MapC '[ '(1, "haa"), '(2, "hoo")]+data FromList :: [(k,v)] -> Exp (MapC k v)+type instance Eval (FromList lst) = 'MapC lst++-- | Insert+--+-- __Example__+--+-- >>> :kind! Eval (Insert 3 "hih" =<< FromList '[ '(1,"haa"), '(2,"hoo")])+-- Eval (Insert 3 "hih" =<< FromList '[ '(1,"haa"), '(2,"hoo")]) :: MapC +-- Nat TL.Symbol+-- = 'MapC '[ '(3, "hih"), '(1, "haa"), '(2, "hoo")]+data Insert :: k -> v -> MapC k v -> Exp (MapC k v)+type instance Eval (Insert k v ('MapC lst)) =+ If (Eval (Elem k =<< Fcf.Map Fst lst))+ ('MapC lst)+ ('MapC ( '(k,v) ': lst))+++-- | InsertWith+-- if old there, map+-- if no old, add+--+-- __Example__+-- +-- >>> :kind! Eval (InsertWith (Pure2 TL.AppendSymbol) 5 "xxx" (Eval (FromList '[ '(5,"a"), '(3,"b")])))+-- Eval (InsertWith (Pure2 TL.AppendSymbol) 5 "xxx" (Eval (FromList '[ '(5,"a"), '(3,"b")]))) :: MapC +-- Nat +-- TL.Symbol+-- = 'MapC '[ '(5, "xxxa"), '(3, "b")]+--+-- >>> :kind! Eval (InsertWith (Pure2 TL.AppendSymbol) 7 "xxx" (Eval (FromList '[ '(5,"a"), '(3,"b")])))+-- Eval (InsertWith (Pure2 TL.AppendSymbol) 7 "xxx" (Eval (FromList '[ '(5,"a"), '(3,"b")]))) :: MapC +-- Nat +-- TL.Symbol+-- = 'MapC '[ '(5, "a"), '(3, "b"), '(7, "xxx")]+--+-- >>> :kind! Eval (InsertWith (Pure2 TL.AppendSymbol) 5 "xxx" =<< Empty)+-- Eval (InsertWith (Pure2 TL.AppendSymbol) 5 "xxx" =<< Empty) :: MapC +-- Nat TL.Symbol+-- = 'MapC '[ '(5, "xxx")]+data InsertWith :: (v -> v -> Exp v) -> k -> v -> MapC k v -> Exp (MapC k v)+type instance Eval (InsertWith f k v ('MapC lst)) =+ If (Eval (Elem k =<< Fcf.Map Fst lst))+ ('MapC (Eval (Fcf.Map (InsWithHelp f k v) lst)))+ ('MapC (Eval (lst ++ '[ '(k,v)])))++-- helper+data InsWithHelp :: (v -> v -> Exp v) -> k -> v -> (k,v) -> Exp (k,v)+type instance Eval (InsWithHelp f k1 vNew '(k2,vOld)) =+ If (Eval (TyEq k1 k2))+ '(k1, Eval (f vNew vOld))+ '(k2, vOld)+++-- | Delete+-- +-- __Example__+-- +-- >>> :kind! Eval (Delete 5 (Eval (FromList '[ '(5,"a"), '(3,"b")])))+-- Eval (Delete 5 (Eval (FromList '[ '(5,"a"), '(3,"b")]))) :: MapC +-- Nat TL.Symbol+-- = 'MapC '[ '(3, "b")]+--+-- >>> :kind! Eval (Delete 7 (Eval (FromList '[ '(5,"a"), '(3,"b")])))+-- Eval (Delete 7 (Eval (FromList '[ '(5,"a"), '(3,"b")]))) :: MapC +-- Nat TL.Symbol+-- = 'MapC '[ '(5, "a"), '(3, "b")]+--+-- >>> :kind! Eval (Delete 7 (Eval Empty))+-- Eval (Delete 7 (Eval Empty)) :: MapC Nat v+-- = 'MapC '[]+data Delete :: k -> MapC k v -> Exp (MapC k v)+type instance Eval (Delete k ('MapC lst)) =+ 'MapC (Eval (Fcf.Filter (Not <=< TyEq k <=< Fst) lst))++-- | Adjust+-- +-- __Example__+-- +-- >>> :kind! Eval (Adjust (Pure1 (TL.AppendSymbol "new ")) 5 (Eval (FromList '[ '(5,"a"), '(3,"b")])))+-- Eval (Adjust (Pure1 (TL.AppendSymbol "new ")) 5 (Eval (FromList '[ '(5,"a"), '(3,"b")]))) :: MapC +-- Nat +-- TL.Symbol+-- = 'MapC '[ '(5, "new a"), '(3, "b")]+--+-- >>> :kind! Eval (Adjust (Pure1 (TL.AppendSymbol "new ")) 7 (Eval (FromList '[ '(5,"a"), '(3,"b")])))+-- Eval (Adjust (Pure1 (TL.AppendSymbol "new ")) 7 (Eval (FromList '[ '(5,"a"), '(3,"b")]))) :: MapC +-- Nat +-- TL.Symbol+-- = 'MapC '[ '(5, "a"), '(3, "b")]+--+-- >>> :kind! Eval (Adjust (Pure1 (TL.AppendSymbol "new ")) 7 (Eval Empty))+-- Eval (Adjust (Pure1 (TL.AppendSymbol "new ")) 7 (Eval Empty)) :: MapC +-- Nat TL.Symbol+-- = 'MapC '[]+data Adjust :: (v -> Exp v) -> k -> MapC k v -> Exp (MapC k v)+type instance Eval (Adjust f k ('MapC lst)) =+ 'MapC (Eval (AdjustHelp f k lst))++data AdjustHelp :: (v -> Exp v) -> k -> [(k,v)] -> Exp [(k,v)]+type instance Eval (AdjustHelp _f _k '[]) = '[]+type instance Eval (AdjustHelp f k ( '(k1,v) ': rst)) =+ If (Eval (TyEq k k1))+ ('(k, f @@ v) ': Eval (AdjustHelp f k rst))+ ('(k1,v) ': Eval (AdjustHelp f k rst))+++-- | Lookup+--+-- __Example__+-- +-- >>> :kind! Eval (Lookup 5 (Eval (FromList '[ '(5,"a"), '(3,"b")])))+-- Eval (Lookup 5 (Eval (FromList '[ '(5,"a"), '(3,"b")]))) :: Maybe +-- TL.Symbol+-- = 'Just "a"+--+-- >>> :kind! Eval (Lookup 7 (Eval (FromList '[ '(5,"a"), '(3,"b")])))+-- Eval (Lookup 7 (Eval (FromList '[ '(5,"a"), '(3,"b")]))) :: Maybe +-- TL.Symbol+-- = 'Nothing+data Lookup :: k -> MapC k v -> Exp (Maybe v)+type instance Eval (Lookup k ('MapC '[])) = 'Nothing+type instance Eval (Lookup k ('MapC ('(k1,v) ': rst))) =+ Eval (If (Eval (TyEq k k1))+ (Pure ('Just v))+ (Lookup k ('MapC rst))+ )++-- | Member+--+-- __Example__+-- +-- >>> :kind! Eval (Member 5 (Eval (FromList '[ '(5,"a"), '(3,"b")])))+-- Eval (Member 5 (Eval (FromList '[ '(5,"a"), '(3,"b")]))) :: Bool+-- = 'True+-- >>> :kind! Eval (Member 7 (Eval (FromList '[ '(5,"a"), '(3,"b")])))+-- Eval (Member 7 (Eval (FromList '[ '(5,"a"), '(3,"b")]))) :: Bool+-- = 'False+data Member :: k -> MapC k v -> Exp Bool+type instance Eval (Member k mp) =+ Eval (Elem k =<< Keys mp)++-- | NotMember+--+-- __Example__+-- +-- >>> :kind! Eval (NotMember 5 (Eval (FromList '[ '(5,"a"), '(3,"b")])))+-- Eval (NotMember 5 (Eval (FromList '[ '(5,"a"), '(3,"b")]))) :: Bool+-- = 'False+-- >>> :kind! Eval (NotMember 7 (Eval (FromList '[ '(5,"a"), '(3,"b")])))+-- Eval (NotMember 7 (Eval (FromList '[ '(5,"a"), '(3,"b")]))) :: Bool+-- = 'True+data NotMember :: k -> MapC k v -> Exp Bool+type instance Eval (NotMember k mp) =+ Eval (Not =<< Elem k =<< Keys mp)++-- | Null+--+-- __Example__+-- +-- >>> :kind! Eval (Null =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Null =<< FromList '[ '(5,"a"), '(3,"b")]) :: Bool+-- = 'False+-- >>> :kind! Eval (Null =<< Empty)+-- Eval (Null =<< Empty) :: Bool+-- = 'True+data Null :: MapC k v -> Exp Bool+type instance Eval (Null ('MapC '[])) = 'True+type instance Eval (Null ('MapC (_ ': _))) = 'False++-- | Size+--+-- __Example__+-- +-- >>> :kind! Eval (Size =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Size =<< FromList '[ '(5,"a"), '(3,"b")]) :: Nat+-- = 2+data Size :: MapC k v -> Exp TL.Nat+type instance Eval (Size ('MapC lst)) = Eval (Length lst)++-- | Union+--+-- __Example__+-- +-- >>> :kind! Eval (Union (Eval (FromList '[ '(5,"a"), '(3,"b")])) (Eval (FromList '[ '(5,"A"), '(7,"c")])) )+-- Eval (Union (Eval (FromList '[ '(5,"a"), '(3,"b")])) (Eval (FromList '[ '(5,"A"), '(7,"c")])) ) :: MapC +-- Nat +-- TL.Symbol+-- = 'MapC '[ '(7, "c"), '(5, "a"), '(3, "b")]+data Union :: MapC k v -> MapC k v -> Exp (MapC k v)+type instance Eval (Union ('MapC lst1) ('MapC lst2)) =+ 'MapC (Eval (Fcf.Foldr UComb lst1 lst2))++data UComb :: (k,v) -> [(k,v)] -> Exp [(k,v)]+type instance Eval (UComb '(k,v) lst) =+ If (Eval (Elem k =<< Fcf.Map Fst lst))+ lst+ ('(k,v) ': lst)+++-- | Difference+-- +-- __Example__+-- +-- >>> :kind! Eval (Difference (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")])))+-- Eval (Difference (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")]))) :: MapC +-- Nat +-- TL.Symbol+-- = 'MapC '[ '(3, "a")]+data Difference :: MapC k v -> MapC k v -> Exp (MapC k v)+type instance Eval (Difference mp1 mp2) =+ Eval (FilterWithKey (DiffNotMem mp2) mp1)++-- helper+data DiffNotMem :: MapC k v -> k -> v -> Exp Bool+type instance Eval (DiffNotMem mp k _) =+ Eval (Not =<< Elem k =<< Keys mp)+++-- | Intersection+--+-- __Example__+-- +-- >>> :kind! Eval (Intersection (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")])))+-- Eval (Intersection (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")]))) :: MapC +-- Nat +-- TL.Symbol+-- = 'MapC '[ '(5, "b")]+data Intersection :: MapC k v -> MapC k v -> Exp (MapC k v)+type instance Eval (Intersection mp1 mp2) =+ Eval (FilterWithKey (InterMem mp2) mp1)++-- helper+data InterMem :: MapC k v -> k -> v -> Exp Bool+type instance Eval (InterMem mp k _) = Eval (Elem k =<< Keys mp)+++-- | Disjoint+--+-- __Example__+-- +-- >>> :kind! Eval (Disjoint (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")])))+-- Eval (Disjoint (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")]))) :: Bool+-- = 'False+--+-- >>> :kind! Eval (Disjoint (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(2,"B"), '(7,"C")])))+-- Eval (Disjoint (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(2,"B"), '(7,"C")]))) :: Bool+-- = 'True+-- >>> :kind! Eval (Disjoint (Eval Empty) (Eval Empty))+-- Eval (Disjoint (Eval Empty) (Eval Empty)) :: Bool+-- = 'True+data Disjoint :: MapC k v -> MapC k v -> Exp Bool+type instance Eval (Disjoint mp1 mp2) =+ Eval (Null =<< Intersection mp1 mp2)+++-- Map +--+-- __Example__+--+-- >>> :kind! Eval (Fcf.Data.MapC.Map (Pure1 (TL.AppendSymbol "x")) =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Fcf.Data.MapC.Map (Pure1 (TL.AppendSymbol "x")) =<< FromList '[ '(5,"a"), '(3,"b")]) :: MapC Nat TL.Symbol+-- = 'MapC '[ '(5, "xa"), '(3, "xb")]+data Map :: (v -> Exp w) -> MapC k v -> Exp (MapC k w)+type instance Eval (Map f mp) =+ 'MapC (Eval (Fcf.Map (Second f) =<< Assocs mp))++-- MapWithKey +--+-- __Example__+-- +data MapWithKey :: (k -> v -> Exp w) -> MapC k v -> Exp (MapC k w)+type instance Eval (MapWithKey f mp) =+ 'MapC (Eval (Fcf.Map (Second (Uncurry f))+ =<< MWKhelp+ =<< Assocs mp))++data MWKhelp :: [(k,v)] -> Exp [(k,(k,v))]+type instance Eval (MWKhelp '[]) = '[]+type instance Eval (MWKhelp ('(k,v) ': rst)) = '(k, '(k,v)) : Eval (MWKhelp rst)+++-- | Foldr+--+-- Fold the values in the map using the given right-associative binary operator, +-- such that 'foldr f z == foldr f z . elems'.+--+-- Note: the order of values in MapC is not well defined at the moment.+--+-- __Example__+-- +-- >>> :kind! Eval (Fcf.Data.MapC.Foldr (Pure2 (TL.+)) 0 =<< (FromList '[ '(1,1), '(2,2)]))+-- Eval (Fcf.Data.MapC.Foldr (Pure2 (TL.+)) 0 =<< (FromList '[ '(1,1), '(2,2)])) :: Nat+-- = 3+data Foldr :: (v -> w -> Exp w) -> w -> MapC k v -> Exp w+type instance Eval (Foldr f w mp) = Eval (Fcf.Foldr f w =<< Elems mp)+++-- | Elems+--+-- __Example__+-- +-- >>> :kind! Eval (Elems =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Elems =<< FromList '[ '(5,"a"), '(3,"b")]) :: [TL.Symbol]+-- = '["a", "b"]+-- >>> :kind! Eval (Elems =<< Empty)+-- Eval (Elems =<< Empty) :: [v]+-- = '[]+data Elems :: MapC k v -> Exp [v]+type instance Eval (Elems ('MapC lst)) = Eval (Fcf.Map Snd lst)++-- | Keys+--+-- __Example__+-- +-- >>> :kind! Eval (Keys =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Keys =<< FromList '[ '(5,"a"), '(3,"b")]) :: [Nat]+-- = '[5, 3]+-- >>> :kind! Eval (Keys =<< Empty)+-- Eval (Keys =<< Empty) :: [k]+-- = '[]+data Keys :: MapC k v -> Exp [k]+type instance Eval (Keys ('MapC lst)) = Eval (Fcf.Map Fst lst)++-- | Assocs+--+-- __Example__+-- +-- >>> :kind! Eval (Assocs =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Assocs =<< FromList '[ '(5,"a"), '(3,"b")]) :: [(Nat, +-- TL.Symbol)]+-- = '[ '(5, "a"), '(3, "b")]+-- >>> :kind! Eval (Assocs =<< Empty)+-- Eval (Assocs =<< Empty) :: [(k, v)]+-- = '[]+data Assocs :: MapC k v -> Exp [(k,v)]+type instance Eval (Assocs ('MapC lst)) = lst++-- | ToList+--+-- __Example__+-- +-- >>> :kind! Eval (ToList =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (ToList =<< FromList '[ '(5,"a"), '(3,"b")]) :: [(Nat, +-- TL.Symbol)]+-- = '[ '(5, "a"), '(3, "b")]+-- >>> :kind! Eval (ToList =<< Empty)+-- Eval (ToList =<< Empty) :: [(k, v)]+-- = '[]+data ToList :: MapC k v -> Exp [(k,v)]+type instance Eval (ToList ('MapC lst)) = lst++-- | Filter+--+-- __Example__+-- +-- >>> :kind! Eval (Filter ((>=) 35) =<< FromList '[ '(5,50), '(3,30)])+-- Eval (Filter ((>=) 35) =<< FromList '[ '(5,50), '(3,30)]) :: MapC +-- Nat Nat+-- = 'MapC '[ '(3, 30)]+data Filter :: (v -> Exp Bool) -> MapC k v -> Exp (MapC k v)+type instance Eval (Filter f ('MapC lst)) =+ 'MapC (Eval (Fcf.Filter (f <=< Snd) lst))++-- | FilterWithKey+--+-- __Example__+--+-- >>> :kind! Eval (FilterWithKey (>=) (Eval (FromList '[ '(3,5), '(6,4)])))+-- Eval (FilterWithKey (>=) (Eval (FromList '[ '(3,5), '(6,4)]))) :: MapC +-- Nat Nat+-- = 'MapC '[ '(6, 4)]+data FilterWithKey :: (k -> v -> Exp Bool) -> MapC k v -> Exp (MapC k v)+type instance Eval (FilterWithKey f ('MapC lst)) =+ 'MapC (Eval (Fcf.Filter (Uncurry f) lst))++-- | Partition+--+-- __Example__+-- +-- >>> :kind! Eval (Partition ((>=) 35) =<< FromList '[ '(5,50), '(3,30)])+-- Eval (Partition ((>=) 35) =<< FromList '[ '(5,50), '(3,30)]) :: (MapC +-- Nat Nat, +-- MapC Nat Nat)+-- = '( 'MapC '[ '(3, 30)], 'MapC '[ '(5, 50)])+data Partition :: (v -> Exp Bool) -> MapC k v -> Exp (MapC k v, MapC k v)+type instance Eval (Partition f ('MapC lst)) =+ Eval (PartitionHlp (Eval (Fcf.Partition (f <=< Snd) lst)))++data PartitionHlp :: ([(k,v)],[(k,v)]) -> Exp (MapC k v, MapC k v)+type instance Eval (PartitionHlp '(xs,ys)) = '( 'MapC xs, 'MapC ys)++
+ src/Fcf/Data/Set.hs view
@@ -0,0 +1,221 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|+Module : Fcf.Data.Set+Description : Set data-structure for type-level programming+Copyright : (c) gspia 2020-+License : BSD+Maintainer : gspia++= Fcf.Data.Set++Set provides an interface which is similar to the that given by the+container-package. If a method is missing here that you need, please do open+up an issue or better, make a PR.++Many of the examples are from containers-package. The internal representation+is based on lists. We hope that a more efficient one will be used one day.++-}+++--------------------------------------------------------------------------------++module Fcf.Data.Set where++import qualified GHC.TypeLits as TL++import Fcf ( Eval, Exp, type (=<<), type (<=<)+ , Not, If+ , TyEq, Length)+-- import Fcf.Data.List as Fcf+import qualified Fcf as Fcf (Foldr, Filter)+import Fcf.Data.List (Elem)++--------------------------------------------------------------------------------++-- For the doctests:++-- $setup+-- >>> import qualified GHC.TypeLits as TL+-- >>> import Fcf.Data.Nat++--------------------------------------------------------------------------------++-- | Set-definition.+data Set a = Set [a]++-- | Empty+-- +-- __Example__+-- +-- >>> :kind! (Eval Empty :: Set Nat)+-- (Eval Empty :: Set Nat) :: Set Nat+-- = 'Set '[]+--+-- See also the other examples in this module.+data Empty :: Exp (Set v)+type instance Eval Empty = 'Set '[]++-- | Singleton+-- +-- __Example__+-- +-- >>> :kind! Eval (Singleton 1)+-- Eval (Singleton 1) :: Set Nat+-- = 'Set '[1]+data Singleton :: v -> Exp (Set v)+type instance Eval (Singleton v) = 'Set '[v]++-- | Use FromList to construct a Set from type-level list.+--+-- __Example__+-- +-- >>> :kind! Eval (FromList '[1, 2])+-- Eval (FromList '[1, 2]) :: Set Nat+-- = 'Set '[1, 2]+data FromList :: [v] -> Exp (Set v)+type instance Eval (FromList lst) = 'Set lst+++-- | Insert+--+-- __Example__+--+-- >>> :kind! Eval (Insert 3 =<< FromList '[1, 2])+-- Eval (Insert 3 =<< FromList '[1, 2]) :: Set Nat+-- = 'Set '[3, 1, 2]+--+-- >>> :kind! Eval (Insert 2 =<< FromList '[1, 2])+-- Eval (Insert 2 =<< FromList '[1, 2]) :: Set Nat+-- = 'Set '[1, 2]+data Insert :: v -> Set v -> Exp (Set v)+type instance Eval (Insert v ('Set lst)) =+ If (Eval (Elem v lst))+ ('Set lst)+ ('Set (v ': lst))++-- | Delete+-- +-- __Example__+-- +-- >>> :kind! Eval (Delete 5 =<< FromList '[5, 3])+-- Eval (Delete 5 =<< FromList '[5, 3]) :: Set Nat+-- = 'Set '[3]+--+-- >>> :kind! Eval (Delete 7 =<< FromList '[5, 3])+-- Eval (Delete 7 =<< FromList '[5, 3]) :: Set Nat+-- = 'Set '[5, 3]+data Delete :: v -> Set v -> Exp (Set v)+type instance Eval (Delete v ('Set lst)) =+ 'Set (Eval (Fcf.Filter (Not <=< TyEq v) lst))++-- | Member+--+-- __Example__+-- +-- >>> :kind! Eval (Member 5 =<< FromList '[5, 3])+-- Eval (Member 5 =<< FromList '[5, 3]) :: Bool+-- = 'True+-- >>> :kind! Eval (Member 7 =<< FromList '[5, 3])+-- Eval (Member 7 =<< FromList '[5, 3]) :: Bool+-- = 'False+data Member :: v -> Set v -> Exp Bool+type instance Eval (Member v ('Set lst)) = Eval (Elem v lst)++-- | NotMember+--+-- __Example__+-- +-- >>> :kind! Eval (NotMember 5 =<< FromList '[5, 3])+-- Eval (NotMember 5 =<< FromList '[5, 3]) :: Bool+-- = 'False+-- >>> :kind! Eval (NotMember 7 =<< FromList '[5, 3])+-- Eval (NotMember 7 =<< FromList '[5, 3]) :: Bool+-- = 'True+data NotMember :: v -> Set v -> Exp Bool+type instance Eval (NotMember k ('Set lst)) =+ Eval (Not =<< Elem k lst)++-- | Null+--+-- __Example__+-- +-- >>> :kind! Eval (Null =<< FromList '[5, 3])+-- Eval (Null =<< FromList '[5, 3]) :: Bool+-- = 'False+-- >>> :kind! Eval (Null =<< Empty)+-- Eval (Null =<< Empty) :: Bool+-- = 'True+data Null :: Set v -> Exp Bool+type instance Eval (Null ('Set '[])) = 'True+type instance Eval (Null ('Set (_ ': _))) = 'False++-- | Size+--+-- __Example__+-- +-- >>> :kind! Eval (Size =<< FromList '[5, 3])+-- Eval (Size =<< FromList '[5, 3]) :: Nat+-- = 2+data Size :: Set v -> Exp TL.Nat+type instance Eval (Size ('Set lst)) = Eval (Length lst)++-- | Union+--+-- __Example__+-- +-- >>> :kind! Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) )+-- Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) ) :: Set +-- Nat+-- = 'Set '[7, 5, 3]+data Union :: Set v -> Set v -> Exp (Set v)+type instance Eval (Union ('Set lst1) ('Set lst2)) =+ 'Set (Eval (Fcf.Foldr UComb lst1 lst2))++data UComb :: v -> [v] -> Exp [v]+type instance Eval (UComb v lst) =+ If (Eval (Elem v lst))+ lst+ (v ': lst)+++-- | Difference+-- +-- __Example__+-- +-- >>> :kind! Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))+-- Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) :: Set +-- Nat+-- = 'Set '[3]+data Difference :: Set v -> Set v -> Exp (Set v)+type instance Eval (Difference ('Set lst1) ('Set lst2)) =+ 'Set (Eval (Fcf.Filter (DiffNotMem lst2) lst1))++-- helper+data DiffNotMem :: [v] -> v -> Exp Bool+type instance Eval (DiffNotMem lst v) = Eval (Not =<< Elem v lst)+++-- | Intersection+--+-- __Example__+-- +-- >>> :kind! Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))+-- Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) :: Set +-- Nat+-- = 'Set '[5]+data Intersection :: Set v -> Set v -> Exp (Set v)+type instance Eval (Intersection ('Set lst1) ('Set lst2)) =+ 'Set (Eval (Fcf.Filter (InterMem lst2) lst1))++-- helper+data InterMem :: [v ]-> v -> Exp Bool+type instance Eval (InterMem lst v) = Eval (Elem v lst)
+ src/Fcf/Data/Tree.hs view
@@ -0,0 +1,136 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|+Module : Fcf.Data.Tree+Description : Tree data-structure for type-level programming+Copyright : (c) gspia 2020-+License : BSD+Maintainer : gspia++= Fcf.Data.Tree++Tree provides an interface which is similar to the that given by the+container-package. If a method is missing here that you need, please do open+up an issue or better, make a PR.++This module provides it's own but (almost) identical definitions of Tree+and Forest. The reason for not using the definitions given in the containers+is that since nothing else is needed from containers, we are able to have+less dependencies.++Many of the examples are from containers-package.++-}+++--------------------------------------------------------------------------------++module Fcf.Data.Tree where++import Fcf as Fcf+-- import Fcf.Data.List as Fcf -- TODO start using on fcf 0.7+import Fcf.Alg.List as Fcf (Unfoldr,ConcatMap) -- TODO remove on fcf 0.7++--------------------------------------------------------------------------------++-- For the doctests:++-- $setup+-- >>> import qualified GHC.TypeLits as TL+-- >>> import Fcf.Data.Nat++--------------------------------------------------------------------------------++-- | Same as in containers, except not used for any term-level computation +-- in this module.+data Tree a = Node a [Tree a]++-- | Same as in containers, except not used for any term-level computation +-- in this module.+type Forest a = [Tree a]++-- | Fold a type-level 'Tree'.+data FoldTree :: (a -> [b] -> Exp b) -> Tree a -> Exp b+type instance Eval (FoldTree f ('Node a '[])) = Eval (f a '[])+type instance Eval (FoldTree f ('Node a (x ': xs))) =+ Eval (f a (Eval (Map (FoldTree f) (x ': xs))))++++-- | Unfold for a 'Tree'.+--+-- __Example__+-- +-- >>> 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 (UnfoldTree BuildNode 1)+-- Eval (UnfoldTree BuildNode 1) :: Tree Nat+-- = 'Node+-- 1+-- '[ 'Node 2 '[ 'Node 4 '[], 'Node 5 '[]],+-- 'Node 3 '[ 'Node 6 '[], 'Node 7 '[]]]+data UnfoldTree :: (b -> Exp (a, [b])) -> b -> Exp (Tree a)+type instance Eval (UnfoldTree f b) =+ 'Node (Eval (Fst Fcf.=<< f b)) (Eval (UnfoldForest f (Eval (Snd =<< f b))))++-- | Unfold for a 'Forest'.+data UnfoldForest :: (b -> Exp (a, [b])) -> [b] -> Exp (Forest a)+type instance Eval (UnfoldForest f bs) = Eval (Map (UnfoldTree f) bs)+++-- | Flatten a 'Tree'.+--+-- __Example__+-- +-- >>> :kind! Eval (Flatten ('Node 1 '[ 'Node 2 '[ 'Node 3 '[ 'Node 4 '[]]], 'Node 5 '[ 'Node 6 '[]]]))+-- Eval (Flatten ('Node 1 '[ 'Node 2 '[ 'Node 3 '[ 'Node 4 '[]]], 'Node 5 '[ 'Node 6 '[]]])) :: [Nat]+-- = '[1, 2, 3, 4, 5, 6]+data Flatten :: Tree a -> Exp [a]+type instance Eval (Flatten ('Node a fs )) = a ': Eval (ConcatMap Flatten fs)++-- | Get the root node from a 'Tree'.+data GetRoot :: Tree a -> Exp a+type instance Eval (GetRoot ('Node a _)) = a++-- | Get the forest from a 'Tree'.+data GetForest :: Tree a -> Exp [Tree a]+type instance Eval (GetForest ('Node _ f)) = f++-- | Get the root nodes from a list of 'Tree's.+data GetRoots :: [Tree a] -> Exp [a]+type instance Eval (GetRoots trs) = Eval (Map GetRoot trs)++-- | Get the forests from a list of 'Tree's.+data GetForests :: [Tree a] -> Exp [Tree a]+type instance Eval (GetForests ts) = Eval (ConcatMap GetForest ts)++-- helper for the Levels-function+data SubFLevels :: [Tree a] -> Exp (Maybe ([a], [Tree a]))+type instance Eval (SubFLevels '[]) = 'Nothing+type instance Eval (SubFLevels (t ': ts)) =+ 'Just '( Eval (GetRoots (t ': ts)), Eval (GetForests (t ': ts)))++-- | Get the levels from a 'Tree'.+--+-- __Example__+-- +-- >>> :kind! Eval (Levels ('Node 1 '[ 'Node 2 '[ 'Node 3 '[ 'Node 4 '[]]], 'Node 5 '[ 'Node 6 '[]]]))+-- Eval (Levels ('Node 1 '[ 'Node 2 '[ 'Node 3 '[ 'Node 4 '[]]], 'Node 5 '[ 'Node 6 '[]]])) :: [[Nat]]+-- = '[ '[1], '[2, 5], '[3, 6], '[4]]+data Levels :: Tree a -> Exp [[a]]+type instance Eval (Levels tr) = Eval (Unfoldr SubFLevels '[tr])++
+ test/doctest.hs view
@@ -0,0 +1,16 @@+import System.FilePath.Glob (glob)+import Test.DocTest++exts :: [String]+exts =+ [ "-XDataKinds"+ , "-XKindSignatures"+ , "-XTypeFamilies"+ , "-XTypeOperators"+ , "-XUndecidableInstances"+ ]++main :: IO ()+main = do+ xs <- glob "src/**/*.hs"+ doctest (exts ++ xs)