{-# 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
containers-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
( Set (..)
-- * Query
, Member
, NotMember
, Null
, Size
, IsSubsetOf
, IsProperSubsetOf
-- * Construction
, Empty
, Singleton
, Insert
, Delete
, PowerSet
-- * Combine
, Union
, Difference
, Intersection
-- * List
, FromList
, ToList
)
where
--------------------------------------------------------------------------------
import qualified GHC.TypeLits as TL
import Fcf ( Eval, Exp, type (=<<), type (<=<), type (&&)
, Not, If, Map, Flip, TyEq )
import qualified Fcf as Fcf (Foldr, Filter)
import Fcf.Class.Foldable (All, Any)
import Fcf.Data.List ( Elem, Cons, Concat, Reverse, Length, type (++)
, ZipWith, Replicate)
--------------------------------------------------------------------------------
import Fcf.Alg.List ( ListF(..), ListToFix)
import Fcf.Alg.Morphism
--------------------------------------------------------------------------------
-- For the doctests:
-- $setup
-- >>> import qualified GHC.TypeLits as TL
-- >>> import Fcf.Data.Nat
-- >>> import Fcf.Data.Symbol
-- >>> import Fcf.Alg.Sort
--------------------------------------------------------------------------------
-- | 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]
-- | 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)
-- | IsSubsetOf
--
-- === __Example__
--
-- >>> :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]))
-- 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]))
-- 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]))
-- 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
type instance Eval (IsSubsetOf ('Set s1) ('Set s2)) =
Eval (All (Flip Elem s2) s1)
-- | IsProperSubsetOf
--
-- === __Example__
--
-- >>> :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]))
-- Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4])) :: Bool
-- = 'True
data IsProperSubsetOf :: Set a -> Set a -> Exp Bool
type instance Eval (IsProperSubsetOf ('Set s1) ('Set s2)) = Eval
(Eval (All (Flip Elem s2) s1) &&
Eval (Any (Not <=< Flip Elem s1) s2))
-- | Type-level set 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)
-- | Type-level set 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)
-- | Type-level set 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)
--------------------------------------------------------------------------------
-- helper for PowerSet
data AddFalses :: [[Bool]] -> Exp [[Bool]]
type instance Eval (AddFalses lst) = Eval (Map (Cons 'False) lst)
-- helper for PowerSet
data AddTrues :: [[Bool]] -> Exp [[Bool]]
type instance Eval (AddTrues lst) = Eval (Map (Cons 'True) lst)
-- helper for PowerSet
data ExtendBitList :: [[Bool]] -> Exp [[Bool]]
type instance Eval (ExtendBitList lst) =
Eval ((Eval (AddFalses lst)) ++ (Eval (AddTrues =<< Map Reverse lst)))
-- helper for PowerSet
-- :kind! Eval (Cata BuildGrayBitListsAlg=<< ListToFix =<< Replicate 3 '[])
data BuildGrayBitListsAlg :: Algebra (ListF [[Bool]]) [[Bool]]
type instance Eval (BuildGrayBitListsAlg 'NilF) = '[ '[] ]
type instance Eval (BuildGrayBitListsAlg ('ConsF _ lst)) = Eval (ExtendBitList lst)
-- helper for PowerSet
-- :kind! Eval (BuildGrayBitLists '[1,2,3,4])
data BuildGrayBitLists :: [a] -> Exp [[Bool]]
type instance Eval (BuildGrayBitLists lst) =
Eval (Cata BuildGrayBitListsAlg =<< ListToFix =<< Replicate (Eval (Length lst)) '[])
-- helper for PowerSet
data SelWithBool :: a -> Bool -> Exp [a]
type instance Eval (SelWithBool a b) = If b '[a] '[]
-- helper for PowerSet
data SelectWithBools :: [a] -> [Bool] -> Exp [a]
type instance Eval (SelectWithBools elms bls) =
Eval (Concat =<< ZipWith SelWithBool elms bls)
-- | Calculate the power sets of a given type-level list. The algorithm is based
-- on Gray codes.
--
-- === __Example__
--
-- >>> :kind! Eval (PowerSet =<< FromList '["a", "b", "c"])
-- Eval (PowerSet =<< FromList '["a", "b", "c"]) :: Set (Set 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]]
--
data PowerSet :: Set a -> Exp (Set (Set a))
type instance Eval (PowerSet ('Set lst)) =
'Set (Eval (Map FromList
=<< Map (SelectWithBools lst)
=<< BuildGrayBitLists lst))
--------------------------------------------------------------------------------
-- | 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
-- | Get the type-level list out of the 'Set'.
--
-- === __Example__
--
-- >>> :kind! Eval (ToList =<< PowerSet =<< FromList '[1,2,3])
-- Eval (ToList =<< PowerSet =<< FromList '[1,2,3]) :: [Set Nat]
-- = '[ '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]) :: [[Nat]]
-- = '[ '[], '[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