fcf-containers 0.3.0 → 0.4.0

raw patch · 9 files changed

+911/−14 lines, 9 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +11/−0
• README.md +95/−2
• TODO.md +0/−2
• fcf-containers.cabal +2/−1
• src/Fcf/Alg/List.hs +115/−2
• src/Fcf/Alg/Morphism.hs +79/−1
• src/Fcf/Alg/Tree.hs +87/−5
• src/Fcf/Data/NatMap.hs +521/−0
• src/Fcf/Data/Text.hs +1/−1

@@ -1,4 +1,15 @@ +# 0.4.0++20200216++ - add Para+ - add Histo+ - add NatF+ - and examples + - correct the Text Length example+ - NatMap (mimick IntMap)+ # 0.3.0  20200209

@@ -25,7 +25,9 @@   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.+tool to have. The techniques that allows this are defunctionalization, +encoding the functions with empty data types and the use of open type family +to Eval the constructed expressions.    If you have other motivations, please do let us know!  @@ -70,7 +72,98 @@ cabal run orbits  ``` -The `ghci` and `:kind!` command in there are your friends!+There is also another example that show how to use MapC, see+[Haiku.hs](https://github.com/gspia/fcf-containers/blob/master/examples/Haiku.hs)++```+cabal run haiku +```+++## Random Notes++### Partiality and anonymous functions++In the end, everything has to be total. We just post-pone the totality checking+with defunctionalization in a way by trying to evaluate our functions as late+as possible with the `Eval` function. ++We don't have lambdas, but if you can write the helper function in point-free+form, it might can be used directly without any global function definition.+Remember, that `(<=<)` corresponds to term-level `(.)` and `(=<<)` to +term-level function  application `($)`. See also Maguire's book +(Thinking with Types).+++### Conflicting family instance declarations++Transforming term-level Haskell code is relatively straigthforward. Often, +local definitions in `where` and anonymous functions will be turned into +separate helper functions. ++Occasionally, the pattern matching is not quite enough. Please, consider++```+isPrefixOf              :: (Eq a) => [a] -> [a] -> Bool+isPrefixOf [] _         =  True+isPrefixOf _  []        =  False+isPrefixOf (x:xs) (y:ys)=  x == y && isPrefixOf xs ys+```++We could try to define it as +```+data IsPrefixOf :: [a] -> [a] -> Exp Bool+type instance Eval (IsPrefixOf '[] _) = 'True+type instance Eval (IsPrefixOf _ '[]) = 'False+type instance Eval (IsPrefixOf (x ': xs) (y ': ys)) =+         Eval ((Eval (TyEq x y)) && Eval (IsPrefixOf xs ys))+```++But ghc does not like this definition: the first two type instances are+conflicting together. Instead, in these situations we can use a helper type +family:++```+data IsPrefixOf :: [a] -> [a] -> Exp Bool+type instance Eval (IsPrefixOf xs ys) = IsPrefixOf_ xs ys++-- helper for IsPrefixOf+type family IsPrefixOf_ (xs :: [a]) (ys :: [a]) :: Bool where+    IsPrefixOf_ '[] _ = 'True+    IsPrefixOf_ _ '[] = 'False+    IsPrefixOf_ (x ': xs) (y ': ys) =+         Eval ((Eval (TyEq x y)) && IsPrefixOf_ xs ys)+```++### Using `If`++If possible, try to avoid using `Eval` in the if-branches. +For example, consider+```+    (If (Eval (s > 0) )+        ( 'Just '( a, s TL.- 1 ))+        'Nothing+    )+```+and+```+    (If (Eval (s > 0))+        (Eval (Pure ( 'Just '( a, s TL.- 1 ))))+        (Eval (Pure 'Nothing))+    )+```++Both compile and it is easy to end up in the latter form, especially if the +branch is more complex than in this example. ++The former, however, is much better as it doesn't have to evaluate both branches+and is thus more efficient.+++### Other+++The `ghci` and `:kind!` command are your friends!  Source also contains a lot of examples, see [fcf-containers](https://github.com/gspia/fcf-containers/tree/master/src/Fcf).

@@ -17,8 +17,6 @@  ## Morphisms:  -- Para with examples-- Histo with examples - Apo with examples - Futu with examples - and other 

@@ -6,7 +6,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.3.0+Version:             0.4.0 Build-type:          Simple Author:              gspia Maintainer:          iahogsp@gmail.com@@ -21,6 +21,7 @@ library   hs-source-dirs:    src   exposed-modules:   Fcf.Data.MapC+                   , Fcf.Data.NatMap                    , Fcf.Data.Tree                    , Fcf.Data.Set                    , Fcf.Data.Symbol

@@ -31,9 +31,9 @@  import           Fcf.Core (Eval, Exp, type (@@)) import           Fcf.Classes (Map)-import           Fcf.Combinators (type (=<<), type (<=<))+import           Fcf.Combinators (type (=<<), type (<=<), Pure) import           Fcf.Data.List (Foldr, Concat, TakeWhile, DropWhile, Reverse-                               , type (++), ZipWith)+                               , type (++), ZipWith, Elem, Take, Unfoldr) import           Fcf.Utils (If, TyEq) import           Fcf.Data.Bool (type (&&), type  (||), Not) import           Fcf.Data.Nat@@ -56,6 +56,7 @@ 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@@ -64,12 +65,20 @@ -- 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.+--+-- === __Example__+--+-- >>> :kind! Eval (ListToFix '[1,2,3])+-- Eval (ListToFix '[1,2,3]) :: Fix (ListF Nat)+-- = 'Fix ('ConsF 1 ('Fix ('ConsF 2 ('Fix ('ConsF 3 ('Fix 'NilF)))))) 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. -- +-- === __Example__+-- -- >>> :kind! Eval (Cata LenAlg =<< ListToFix '[1,2,3]) -- Eval (Cata LenAlg =<< ListToFix '[1,2,3]) :: Nat -- = 3@@ -79,6 +88,8 @@  -- | Example algebra to calculate the sum of Nats in a list. -- +-- === __Example__+-- -- >>> :kind! Eval (Cata SumAlg =<< ListToFix '[1,2,3,4]) -- Eval (Cata SumAlg =<< ListToFix '[1,2,3,4]) :: Nat -- = 10@@ -88,12 +99,114 @@  -- | Example algebra to calculate the prod of Nats in a list. --+-- === __Example__+-- -- >>> :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++--------------------------------------------------------------------------------++-- | Form a Fix-structure that can be used with Para.+-- +-- === __Example__+--+-- >>> :kind! Eval (ListToParaFix '[1,2,3])+-- Eval (ListToParaFix '[1,2,3]) :: Fix (ListF (Nat, [Nat]))+-- = 'Fix+--     ('ConsF+--        '(1, '[2, 3])+--        ('Fix ('ConsF '(2, '[3]) ('Fix ('ConsF '(3, '[]) ('Fix 'NilF))))))+data ListToParaFix :: [a] -> Exp (Fix (ListF (a,[a])))+type instance Eval (ListToParaFix '[]) = 'Fix 'NilF+type instance Eval (ListToParaFix (a ': as)) =+    'Fix ('ConsF '(a,as) (Eval (ListToParaFix as)))++-- | Example from recursion-package by Vanessa McHale.+-- +-- This removes duplicates from a list (by keeping the right-most one).+--+-- === __Example__+--+-- >>> :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]) :: [Nat]+-- = '[5, 1, 3, 2]+data DedupAlg :: RAlgebra (ListF (a,[a])) [a]+type instance Eval (DedupAlg 'NilF) = '[]+type instance Eval (DedupAlg ('ConsF '(a,as) '(_fxs, past))) = Eval+    (If (Eval (TyEq (Eval (Elem a past)) 'True ))+        (Pure past)+        (Pure (a ': as))+    )+++-- | Example from Recursion Schemes by example by Tim Williams.+--+-- === __Example__+--+-- >>> :kind! Eval (Sliding 3 '[1,2,3,4,5,6])+-- Eval (Sliding 3 '[1,2,3,4,5,6]) :: [[Nat]]+-- = '[ '[1, 2, 3], '[2, 3, 4], '[3, 4, 5], '[4, 5, 6], '[5, 6], '[6]]+data Sliding :: Nat -> [a] -> Exp [[a]]+type instance Eval (Sliding n lst) =+    Eval (Para (SlidingAlg n) =<< ListToParaFix lst)++-- | Tim Williams, Recursion Schemes by example, example for Para.+-- See 'Sliding'-function.+data SlidingAlg :: Nat -> RAlgebra (ListF (a, [a])) [[a]]+type instance Eval (SlidingAlg _ 'NilF) = '[]+type instance Eval (SlidingAlg n ('ConsF '(a,as) '(_fxs,past))) =+    Eval (Take n (a ': as)) ': past+++-- | Tim Williams, Recursion Schemes by example, example for Histo.+data EvensStrip :: ListF a (Ann (ListF a) [a]) -> Exp [a]+type instance Eval (EvensStrip 'NilF) = '[]+type instance Eval (EvensStrip ('ConsF x y)) = x ': Eval (Attr y)+++-- | Tim Williams, Recursion Schemes by example, example for Histo.+data EvensAlg :: ListF a (Ann (ListF a) [a]) -> Exp [a]+type instance Eval (EvensAlg 'NilF) = '[]+type instance Eval (EvensAlg ('ConsF _ rst )) = Eval (EvensStrip =<< Strip rst)++-- | This picks up the elements on even positions on a list and is an +-- example on how to use Histo. This example is+-- from Tim Williams, Recursion Schemes by example.+--+-- === __Example__+--+-- >>> :kind! Eval (Evens =<< RunInc 8)+-- Eval (Evens =<< RunInc 8) :: [Nat]+-- = '[2, 4, 6, 8]+data Evens :: [a] -> Exp [a]+type instance Eval (Evens lst) = Eval (Histo EvensAlg =<< ListToFix lst)++-- | For the ListRunAlg+data NumIter :: a -> Nat -> Exp (Maybe (a,Nat))+type instance Eval (NumIter a s) =+    (If (Eval (s > 0) )+        ( 'Just '( a, s TL.- 1 ))+        'Nothing+    )++-- | For the RunInc+data ListRunAlg :: Nat -> Exp (Maybe (Nat,Nat))+type instance Eval (ListRunAlg s) = Eval (NumIter s s )++-- | Construct a run (that is, a natuaral number sequence from 1 to arg).+--+-- === __Example__+--+-- >>> :kind! Eval (RunInc 8)+-- Eval (RunInc 8) :: [Nat]+-- = '[1, 2, 3, 4, 5, 6, 7, 8]+data RunInc :: Nat -> Exp [Nat]+type instance Eval (RunInc n) = Eval (Reverse =<< Unfoldr ListRunAlg n)+  -------------------------------------------------------------------------------- 

@@ -52,13 +52,17 @@ -- | Commonly used name describing the method 'Ana' eats. type CoAlgebra f a = a -> Exp (f a) +-- | Commonly used name describing the method 'Para' eats.+type RAlgebra f a = f (Fix f, a) -> Exp 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.+-- Check Fcf.Alg.List to see example algebras in use. There we have e.g.+-- ListToFix-function. data Cata :: Algebra f a -> Fix f -> Exp a type instance Eval (Cata alg ('Fix b)) = alg @@ (Eval (Map (Cata alg) b)) @@ -100,6 +104,80 @@ -- = 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)+++-- Helper for Para so that we can do fmap+data Fanout :: RAlgebra f a -> Fix f -> Exp ( Fix f, a)+type instance Eval (Fanout ralg ('Fix f)) = '( 'Fix f, Eval (Para ralg ('Fix f)))+++-- | Write a function to give a 'Fix', and feed it in together with an+-- 'RAlgebra'+--+-- Check Fcf.Alg.List to see example algebras in use. There we have e.g.+-- ListToParaFix-function.+data Para :: RAlgebra f a -> Fix f -> Exp a+type instance Eval (Para ralg ('Fix  a)) =  ralg @@ (Eval (Map (Fanout ralg) a))++--------------------------------------------------------------------------------++-- | Annotate (f r) with attribute a+-- (from Recursion Schemes by example, Tim Williams).+newtype AnnF f a r = AnnF (f r, a)++-- | Annotated fixed-point type. A cofree comonad+-- (from Recursion Schemes by example, Tim Williams).+type Ann f a = Fix (AnnF f a)++-- | Attribute of the root node+-- (from Recursion Schemes by example, Tim Williams).+data Attr :: Ann f a -> Exp a+type instance Eval (Attr ('Fix ( 'AnnF '(_, a)))) = a++-- | Strip attribute from root+-- (from Recursion Schemes by example, Tim Williams).+data Strip :: Ann f a -> Exp (f (Ann f a))+type instance Eval (Strip ('Fix ( 'AnnF '(x,_)))) = x++-- | Annotation constructor+-- (from Recursion Schemes by example, Tim Williams).+data AnnConstr :: (f (Ann f a), a) -> Exp (Fix (AnnF f a))+type instance Eval (AnnConstr fxp) = Eval (Pure ('Fix ('AnnF fxp)))++-- | Synthesized attributes are created in a bottom-up traversal+-- using a catamorphism+-- (from Recursion Schemes by example, Tim Williams).+-- +-- This is the algebra that is fed to the cata.+data SynthAlg :: (f a -> Exp a) -> f (Ann f a) -> Exp (Ann f a)+type instance Eval (SynthAlg alg faf) =+    Eval (AnnConstr '(faf, Eval (alg  =<< Map Attr faf)))++-- | Synthesized attributes are created in a bottom-up traversal+-- using a catamorphism+-- (from Recursion Schemes by example, Tim Williams).+-- +-- For the example, see "Fcf.Data.Alg.Tree.Sizes".+data Synthesize :: (f a -> Exp a) -> Fix f -> Exp (Ann f a)+type instance Eval (Synthesize f fx) = Eval (Cata (SynthAlg f) fx)++--------------------------------------------------------------------------------++-- | Histo takes annotation algebra and takes a Fix-structure+-- (from Recursion Schemes by example, Tim Williams).+-- +-- This is a helper for 'Histo' as it is implemented with 'Cata'.+data HistoAlg :: (f (Ann f a) -> Exp a) -> f (Ann f a) -> Exp (Ann f a)+type instance Eval (HistoAlg alg faf) =+    Eval (AnnConstr '(faf, Eval (alg faf)))++-- | Histo takes annotation algebra and takes a Fix-structure+-- (from Recursion Schemes by example, Tim Williams).+-- +-- Examples can be found from "Fcf.Data.Alg.Tree" and "Fcf.Data.Alg.List"+-- modules.+data Histo :: (f (Ann f a) -> Exp a) -> Fix f -> Exp a+type instance Eval (Histo alg fx) = Eval (Attr =<< Cata (HistoAlg alg) fx)  -------------------------------------------------------------------------------- 

@@ -116,11 +116,11 @@ --  -- __Example__ ----- >>> :kind! Eval (Fib 10)--- Eval (Fib 10) :: Nat+-- >>> :kind! Eval (FibHylo 10)+-- Eval (FibHylo 10) :: Nat -- = 55-data Fib :: Nat -> Exp Nat-type instance Eval (Fib n) = Eval (Hylo SumNodesAlg BuildFibTreeCoA n)+data FibHylo :: Nat -> Exp Nat+type instance Eval (FibHylo n) = Eval (Hylo SumNodesAlg BuildFibTreeCoA n)   --------------------------------------------------------------------------------@@ -129,7 +129,89 @@ -- algorithms. data BTreeF a b = BEmptyF | BNodeF a b b --- functor+-- | BTreeF is a 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))++--------------------------------------------------------------------------------++-- | A kind of foldable sum class. Pun may or may not be intended.+data FSum :: f a -> Exp a++-- | Instances to make TreeF to be a foldable sum. After this one, we can write+-- the 'Sizes' example.+type instance Eval (FSum ('NodeF a '[])) = 0+type instance Eval (FSum ('NodeF a (b ': bs))) = Eval (Sum (b ': bs))++-- | Sizes example from Recursion Schemes by example, Tim Williams. This annotes+-- each node with the size of its subtree.+--+-- __Example__+--+-- >>> :kind! Eval (Sizes =<< Ana BuildNodeCoA 1)+-- Eval (Sizes =<< Ana BuildNodeCoA 1) :: Fix (AnnF (TreeF Nat) Nat)+-- = 'Fix+--     ('AnnF+--        '( 'NodeF+--             1+--             '[ 'Fix+--                  ('AnnF+--                     '( 'NodeF+--                          2+--                          '[ 'Fix ('AnnF '( 'NodeF 4 '[], 1)),+--                             'Fix ('AnnF '( 'NodeF 5 '[], 1))],+--                        3)),+--                'Fix+--                  ('AnnF+--                     '( 'NodeF+--                          3+--                          '[ 'Fix ('AnnF '( 'NodeF 6 '[], 1)),+--                             'Fix ('AnnF '( 'NodeF 7 '[], 1))],+--                        3))],+--           7))+type instance Eval (Sizes fx) = Eval (Synthesize ( ( (+) 1) <=< FSum) fx)+data Sizes :: Fix f -> Exp (Ann f Nat)++--------------------------------------------------------------------------------+++-- | A NatF functor that can be used with different morphisms. This tree-module+-- is probably a wrong place to this one. Now it is here for the Fibonacci+-- example.+data NatF r = Succ r | Zero++-- | NatF has to have functor-instances so that morphisms will work.+type instance Eval (Map f 'Zero) = 'Zero+type instance Eval (Map f ('Succ r)) = 'Succ (Eval (f r))++-- | We want to be able to build NatF Fix-structures out of Nat's.+data NatToFix :: Nat -> Exp (Fix NatF)+type instance Eval (NatToFix n) = Eval+    (If (Eval (n < 1))+        (Pure ('Fix 'Zero))+        (RecNTF =<< n - 1)+    )++-- helper for 'NatToFix' -function+data RecNTF :: Nat -> Exp (Fix NatF)+type instance Eval (RecNTF n) = 'Fix ('Succ (Eval (NatToFix n)))++-- | Efficient Fibonacci algebra from Recursion Schemes by example, Tim Williams.+data FibAlgebra :: NatF (Ann NatF Nat) -> Exp Nat+type instance Eval (FibAlgebra 'Zero) = 0+type instance Eval (FibAlgebra ('Succ ('Fix ('AnnF '( 'Zero, _) )))) = 1+type instance Eval (FibAlgebra ('Succ ('Fix ('AnnF '( 'Succ ('Fix ('AnnF '( _, n))) , m) )))) = Eval (n + m)++-- | Efficient Fibonacci type-level function+-- (from Recursion Schemes by example, Tim Williams). Compare this to +-- 'FibHylo'.+--+-- __Example__+--+-- >>> :kind! Eval (FibHisto 100)+-- Eval (FibHisto 100) :: Nat+-- = 354224848179261915075+data FibHisto :: Nat -> Exp Nat+type instance Eval (FibHisto n) = Eval (Histo FibAlgebra =<< NatToFix n)+ 

@@ -0,0 +1,521 @@+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE PolyKinds              #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeInType             #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# OPTIONS_GHC -Wall                       #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|+Module      : Fcf.Data.NatMap+Description : NatMap data-type for the type-level programming (like IntMap)+Copyright   : (c) gspia 2020-+License     : BSD+Maintainer  : gspia++= Fcf.Data.NatNatMap++NatMap provides an interface to mapping keys (Nat's) to values, which is+similar to+NatIntMap 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.++-}++--------------------------------------------------------------------------------++module Fcf.Data.NatMap+    ( -- * NatMap type+      NatMap (..)++    -- * Query+    , Null+    , Size+    , Lookup+    , Member+    , NotMember+    , Disjoint+    , Elems+    , Keys+    , Assocs++    -- * Construction+    , Empty+    , Singleton+    , Insert+    , InsertWith+    , Delete++    -- * Combine+    , Union+    , Difference+    , Intersection++    -- * Modify+    , Adjust+    , Map+    , NatMapWithKey+    , Foldr+    , Filter+    , FilterWithKey+    , Partition++    -- * List+    , FromList+    , ToList++    )+  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)++import           Fcf.Data.Nat+import           Fcf.Alg.Morphism+import qualified Fcf.Alg.List as Fcf (Partition)++--------------------------------------------------------------------------------++-- For the doctests:++-- $setup+-- >>> import           Fcf (type (>=))+-- >>> import           Fcf.Data.Nat+-- >>> import           Fcf.Data.Symbol (Symbol,Append)++--------------------------------------------------------------------------------+++-- | A type corresponding to IntMap in the containers.+-- +-- 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 NatMap v = NatMap [(Nat,v)]++-- | Empty+-- +-- === __Example__+-- +-- >>> :kind! (Eval Empty :: NatMap Symbol)+-- (Eval Empty :: NatMap Symbol) :: NatMap Symbol+-- = 'NatMap '[]+--+-- >>> :kind! (Eval Empty :: NatMap String)+-- (Eval Empty :: NatMap String) :: NatMap [Char]+-- = 'NatMap '[]+-- +-- See also the other examples in this module.+data Empty :: Exp (NatMap v)+type instance Eval Empty = 'NatMap '[]++-- | Singleton+-- +-- === __Example__+-- +-- >>> :kind! Eval (Singleton 1 "haa")+-- Eval (Singleton 1 "haa") :: NatMap Symbol+-- = 'NatMap '[ '(1, "haa")]+data Singleton :: Nat -> v -> Exp (NatMap v)+type instance Eval (Singleton k v) = 'NatMap '[ '(k,v)]++-- | Use FromList to construct a NatMap from type-level list.+--+-- === __Example__+-- +-- >>> :kind! Eval (FromList '[ '(1,"haa"), '(2,"hoo")])+-- Eval (FromList '[ '(1,"haa"), '(2,"hoo")]) :: NatMap Symbol+-- = 'NatMap '[ '(1, "haa"), '(2, "hoo")]+data FromList :: [(Nat,v)] -> Exp (NatMap v)+type instance Eval (FromList lst) = 'NatMap lst++-- | Insert+--+-- === __Example__+--+-- >>> :kind! Eval (Insert 3 "hih" =<< FromList '[ '(1,"haa"), '(2,"hoo")])+-- Eval (Insert 3 "hih" =<< FromList '[ '(1,"haa"), '(2,"hoo")]) :: NatMap +--                                                                    Symbol+-- = 'NatMap '[ '(3, "hih"), '(1, "haa"), '(2, "hoo")]+data Insert :: Nat -> v -> NatMap v -> Exp (NatMap v)+type instance Eval (Insert k v ('NatMap lst)) =+    If (Eval (Elem k =<< Fcf.Map Fst lst))+        ('NatMap lst)+        ('NatMap ( '(k,v) ': lst))+++-- | InsertWith+-- if old there, map+-- if no old, add+--+-- === __Example__+-- +-- >>> :kind! Eval (InsertWith Append 5 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (InsertWith Append 5 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap+--                                                                           Symbol+-- = 'NatMap '[ '(5, "xxxa"), '(3, "b")]+--+-- >>> :kind! Eval (InsertWith Append 7 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (InsertWith Append 7 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap+--                                                                           Symbol+-- = 'NatMap '[ '(5, "a"), '(3, "b"), '(7, "xxx")]+--+-- >>> :kind! Eval (InsertWith Append 7 "xxx" =<< Empty)+-- Eval (InsertWith Append 7 "xxx" =<< Empty) :: NatMap Symbol+-- = 'NatMap '[ '(7, "xxx")]+data InsertWith :: (v -> v -> Exp v) -> Nat -> v -> NatMap v -> Exp (NatMap v)+type instance Eval (InsertWith f k v ('NatMap lst)) =+    If (Eval (Elem k =<< Fcf.Map Fst lst))+        ('NatMap (Eval (Fcf.Map (InsWithHelp f k v) lst)))+        ('NatMap (Eval (lst ++ '[ '(k,v)])))++-- helper+data InsWithHelp :: (v -> v -> Exp v) -> Nat -> v -> (Nat,v) -> Exp (Nat,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 =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Delete 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap+--                                                          Symbol+-- = 'NatMap '[ '(3, "b")]+--+-- >>> :kind! Eval (Delete 7 =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Delete 7 =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap+--                                                          Symbol+-- = 'NatMap '[ '(5, "a"), '(3, "b")]+--+-- >>> :kind! Eval (Delete 7 =<< Empty)+-- Eval (Delete 7 =<< Empty) :: NatMap v+-- = 'NatMap '[]+data Delete :: Nat -> NatMap v -> Exp (NatMap v)+type instance Eval (Delete k ('NatMap lst)) =+    'NatMap (Eval (Fcf.Filter (Not <=< TyEq k <=< Fst) lst))++-- | Adjust+-- +-- === __Example__+-- +-- >>> :kind! Eval (Adjust (Append "new ") 5 =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Adjust (Append "new ") 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap+--                                                                          Symbol+-- = 'NatMap '[ '(5, "new a"), '(3, "b")]+--+-- >>> :kind! Eval (Adjust (Append "new ") 7 =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Adjust (Append "new ") 7 =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap+--                                                                          Symbol+-- = 'NatMap '[ '(5, "a"), '(3, "b")]+--+-- >>> :kind! Eval (Adjust (Append "new ") 7 =<< Empty)+-- Eval (Adjust (Append "new ") 7 =<< Empty) :: NatMap Symbol+-- = 'NatMap '[]+data Adjust :: (v -> Exp v) -> Nat -> NatMap v -> Exp (NatMap v)+type instance Eval (Adjust f k ('NatMap lst)) =+    'NatMap (Eval (AdjustHelp f k lst))++data AdjustHelp :: (v -> Exp v) -> k -> [(Nat,v)] -> Exp [(Nat,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 =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Lookup 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Maybe Symbol+-- = 'Just "a"+--+-- >>> :kind! Eval (Lookup 7 =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Lookup 7 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Maybe Symbol+-- = 'Nothing+data Lookup :: Nat -> NatMap v -> Exp (Maybe v)+type instance Eval (Lookup k ('NatMap '[])) = 'Nothing+type instance Eval (Lookup k ('NatMap ('(k1,v) ': rst))) =+     Eval (If (Eval (TyEq k k1))+            (Pure ('Just v))+            (Lookup k ('NatMap rst))+          )++-- | Member+--+-- === __Example__+-- +-- >>> :kind! Eval (Member 5 =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Member 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Bool+-- = 'True+-- >>> :kind! Eval (Member 7 =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Member 7 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Bool+-- = 'False+data Member :: Nat -> NatMap v -> Exp Bool+type instance Eval (Member k mp) =+    Eval (Elem k =<< Keys mp)++-- | NotMember+--+-- === __Example__+-- +-- >>> :kind! Eval (NotMember 5 =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (NotMember 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Bool+-- = 'False+-- >>> :kind! Eval (NotMember 7 =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (NotMember 7 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Bool+-- = 'True+data NotMember :: Nat -> NatMap 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 :: NatMap v -> Exp Bool+type instance Eval (Null ('NatMap '[])) = 'True+type instance Eval (Null ('NatMap (_ ': _))) = 'False++-- | Size+--+-- === __Example__+-- +-- >>> :kind! Eval (Size =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Size =<< FromList '[ '(5,"a"), '(3,"b")]) :: Nat+-- = 2+data Size :: NatMap v -> Exp Nat+type instance Eval (Size ('NatMap 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")])) ) :: NatMap +--                                                                                                      Symbol+-- = 'NatMap '[ '(7, "c"), '(5, "a"), '(3, "b")]+data Union :: NatMap v -> NatMap v -> Exp (NatMap v)+type instance Eval (Union ('NatMap lst1) ('NatMap lst2)) =+    'NatMap (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")]))) :: NatMap +--                                                                                                          Symbol+-- = 'NatMap '[ '(3, "a")]+data Difference :: NatMap v -> NatMap v -> Exp (NatMap v)+type instance Eval (Difference mp1 mp2) =+    Eval (FilterWithKey (DiffNotMem mp2) mp1)++-- helper+data DiffNotMem :: NatMap 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")]))) :: NatMap +--                                                                                                            Symbol+-- = 'NatMap '[ '(5, "b")]+data Intersection :: NatMap v -> NatMap v -> Exp (NatMap v)+type instance Eval (Intersection mp1 mp2) =+    Eval (FilterWithKey (InterMem mp2) mp1)++-- helper+data InterMem :: NatMap v -> Nat -> 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 :: NatMap v -> NatMap v -> Exp Bool+type instance Eval (Disjoint mp1 mp2) =+    Eval (Null =<< Intersection mp1 mp2)+++-- | Map+--+-- === __Example__+--+-- >>> :kind! Eval (Fcf.Data.NatMap.Map (Append "x") =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Fcf.Data.NatMap.Map (Append "x") =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap +--                                                                                  Symbol+-- = 'NatMap '[ '(5, "xa"), '(3, "xb")]+data Map :: (v -> Exp w) -> NatMap v -> Exp (NatMap w)+type instance Eval (Map f mp) =+    'NatMap (Eval (Fcf.Map (Second f) =<< Assocs mp))++-- | NatMapWithKey+--+-- === __Example__+-- +data NatMapWithKey :: (Nat -> v -> Exp w) -> NatMap v -> Exp (NatMap w)+type instance Eval (NatMapWithKey f mp) =+    'NatMap (Eval (Fcf.Map (Second (Uncurry f))+        =<< MWKhelp+        =<< Assocs mp))++data MWKhelp :: [(Nat,v)] -> Exp [(Nat,(Nat,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 NatMap is not well defined at the moment.+--+-- === __Example__+-- +-- >>> :kind! Eval (Fcf.Data.NatMap.Foldr (+) 0  =<< (FromList '[ '(1,1), '(2,2)]))+-- Eval (Fcf.Data.NatMap.Foldr (+) 0  =<< (FromList '[ '(1,1), '(2,2)])) :: Nat+-- = 3+data Foldr :: (v -> w -> Exp w) -> w -> NatMap 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")]) :: [Symbol]+-- = '["a", "b"]+-- >>> :kind! Eval (Elems =<< Empty)+-- Eval (Elems =<< Empty) :: [v]+-- = '[]+data Elems :: NatMap v -> Exp [v]+type instance Eval (Elems ('NatMap 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) :: [Nat]+-- = '[]+data Keys :: NatMap v -> Exp [Nat]+type instance Eval (Keys ('NatMap lst)) = Eval (Fcf.Map Fst lst)++-- | Assocs+--+-- === __Example__+-- +-- >>> :kind! Eval (Assocs =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (Assocs =<< FromList '[ '(5,"a"), '(3,"b")]) :: [(Nat, +--                                                        Symbol)]+-- = '[ '(5, "a"), '(3, "b")]+-- >>> :kind! Eval (Assocs =<< Empty)+-- Eval (Assocs =<< Empty) :: [(Nat, v)]+-- = '[]+data Assocs :: NatMap v -> Exp [(Nat,v)]+type instance Eval (Assocs ('NatMap lst)) = lst++-- | ToList+--+-- === __Example__+-- +-- >>> :kind! Eval (ToList =<< FromList '[ '(5,"a"), '(3,"b")])+-- Eval (ToList =<< FromList '[ '(5,"a"), '(3,"b")]) :: [(Nat, +--                                                        Symbol)]+-- = '[ '(5, "a"), '(3, "b")]+-- >>> :kind! Eval (ToList =<< Empty)+-- Eval (ToList =<< Empty) :: [(Nat, v)]+-- = '[]+data ToList :: NatMap v -> Exp [(Nat,v)]+type instance Eval (ToList ('NatMap lst)) = lst++-- | Filter+--+-- === __Example__+-- +-- >>> :kind! Eval (Filter ((>=) 35) =<< FromList '[ '(5,50), '(3,30)])+-- Eval (Filter ((>=) 35) =<< FromList '[ '(5,50), '(3,30)]) :: NatMap +--                                                                Nat+-- = 'NatMap '[ '(3, 30)]+data Filter :: (v -> Exp Bool) -> NatMap v -> Exp (NatMap v)+type instance Eval (Filter f ('NatMap lst)) =+    'NatMap (Eval (Fcf.Filter (f <=< Snd) lst))++-- | FilterWithKey+--+-- === __Example__+--+-- >>> :kind! Eval (FilterWithKey (>=) =<< FromList '[ '(3,5), '(6,4)])+-- Eval (FilterWithKey (>=) =<< FromList '[ '(3,5), '(6,4)]) :: NatMap+--                                                                Nat+-- = 'NatMap '[ '(6, 4)]+data FilterWithKey :: (Nat -> v -> Exp Bool) -> NatMap v -> Exp (NatMap v)+type instance Eval (FilterWithKey f ('NatMap lst)) =+    'NatMap (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)]) :: (NatMap +--                                                                    Nat, +--                                                                  NatMap Nat)+-- = '( 'NatMap '[ '(3, 30)], 'NatMap '[ '(5, 50)])+data Partition :: (v -> Exp Bool) -> NatMap v -> Exp (NatMap v, NatMap v)+type instance Eval (Partition f ('NatMap lst)) =+    Eval (PartitionHlp (Eval (Fcf.Partition (f <=< Snd) lst)))++data PartitionHlp :: ([(Nat,v)],[(Nat,v)]) -> Exp (NatMap v, NatMap v)+type instance Eval (PartitionHlp '(xs,ys)) = '( 'NatMap xs, 'NatMap ys)++

@@ -210,7 +210,7 @@ -- -- === __Example__ -- --- > :kind! Eval (Cons "h" ('Text '["a", "a", "m", "u"]))+-- >>> :kind! Eval (Cons "h" ('Text '["a", "a", "m", "u"])) -- Eval (Cons "h" ('Text '["a", "a", "m", "u"])) :: Text -- = 'Text '["h", "a", "a", "m", "u"] data Cons :: Symbol -> Text -> Exp Text