Copyright	(c) gspia 2020-
License	BSD
Maintainer	gspia
Safe Haskell	Safe
Language	Haskell2010

Fcf.Data.Set

Contents

Query
Construction
Combine
List

Description

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.

Synopsis

data Set a = Set [a]
data Member :: v -> Set v -> Exp Bool
data NotMember :: v -> Set v -> Exp Bool
data Null :: Set v -> Exp Bool
data Size :: Set v -> Exp Nat
data IsSubsetOf :: Set a -> Set a -> Exp Bool
data IsProperSubsetOf :: Set a -> Set a -> Exp Bool
data Empty :: Exp (Set v)
data Singleton :: v -> Exp (Set v)
data Insert :: v -> Set v -> Exp (Set v)
data Delete :: v -> Set v -> Exp (Set v)
data PowerSet :: Set a -> Exp (Set (Set a))
data Union :: Set v -> Set v -> Exp (Set v)
data Difference :: Set v -> Set v -> Exp (Set v)
data Intersection :: Set v -> Set v -> Exp (Set v)
data FromList :: [v] -> Exp (Set v)
data ToList :: Set v -> Exp [v]

Documentation

data Set a Source #

Set-definition.

Constructors

Set [a]

Instances

type Eval (Empty :: Set v -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (Empty :: Set v -> Type) = Set ([] :: [v])
type Eval (Singleton v :: Set a -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (Singleton v :: Set a -> Type) = Set (v ': ([] :: [a]))
type Eval (FromList lst :: Set a -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (FromList lst :: Set a -> Type) = Set lst
type Eval (PowerSet (Set lst) :: Set (Set v) -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (PowerSet (Set lst) :: Set (Set v) -> Type)
type Eval (Insert v (Set lst) :: Set a -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (Insert v (Set lst) :: Set a -> Type) = If (Eval (Elem v lst)) (Set lst) (Set (v ': lst))
type Eval (Delete v (Set lst) :: Set a -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (Delete v (Set lst) :: Set a -> Type) = Set (Eval (Filter (Not <=< (TyEq v :: a -> Bool -> Type)) lst))
type Eval (Union (Set lst1) (Set lst2) :: Set a -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (Union (Set lst1) (Set lst2) :: Set a -> Type)
type Eval (Difference (Set lst1) (Set lst2) :: Set a -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (Difference (Set lst1) (Set lst2) :: Set a -> Type)
type Eval (Intersection (Set lst1) (Set lst2) :: Set a -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (Intersection (Set lst1) (Set lst2) :: Set a -> Type)

Query

data Member :: v -> Set v -> Exp Bool Source #

Member

Example

Expand

>>> :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

Instances

type Eval (Member v (Set lst) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (Member v (Set lst) :: Bool -> Type) = Eval (Elem v lst)

data NotMember :: v -> Set v -> Exp Bool Source #

NotMember

Example

Expand

>>> :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

Instances

type Eval (NotMember k (Set lst) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (NotMember k (Set lst) :: Bool -> Type) = Eval (Not =<< Elem k lst)

data Null :: Set v -> Exp Bool Source #

Null

Example

Expand

>>> :kind! Eval (Null =<< FromList '[5, 3])
Eval (Null =<< FromList '[5, 3]) :: Bool
= 'False
>>> :kind! Eval (Null =<< Empty)
Eval (Null =<< Empty) :: Bool
= 'True

Instances

type Eval (Null (Set (_1 ': _2)) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (Null (Set (_1 ': _2)) :: Bool -> Type) = False
type Eval (Null (Set ([] :: [v])) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (Null (Set ([] :: [v])) :: Bool -> Type) = True

data Size :: Set v -> Exp Nat Source #

Size

Example

Expand

>>> :kind! Eval (Size =<< FromList '[5, 3])
Eval (Size =<< FromList '[5, 3]) :: Nat
= 2

Instances

type Eval (Size (Set lst) :: Nat -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (Size (Set lst) :: Nat -> Type) = Eval (Length lst)

data IsSubsetOf :: Set a -> Set a -> Exp Bool Source #

IsSubsetOf

Example

Expand

>>> :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

Instances

type Eval (IsSubsetOf (Set s1) (Set s2) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (IsSubsetOf (Set s1) (Set s2) :: Bool -> Type) = Eval (All (Flip (Elem :: a -> [a] -> Bool -> Type) s2) s1)

data IsProperSubsetOf :: Set a -> Set a -> Exp Bool Source #

IsProperSubsetOf

Example

Expand

>>> :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

Instances

type Eval (IsProperSubsetOf (Set s1) (Set s2) :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (IsProperSubsetOf (Set s1) (Set s2) :: Bool -> Type) = Eval (Eval (All (Flip (Elem :: a -> [a] -> Bool -> Type) s2) s1) && Eval (Any (Not <=< Flip (Elem :: a -> [a] -> Bool -> Type) s1) s2))

Construction

data Empty :: Exp (Set v) Source #

Empty

Example

Expand

>>> :kind! (Eval Empty :: Set Nat)
(Eval Empty :: Set Nat) :: Set Nat
= 'Set '[]

See also the other examples in this module.

Instances

type Eval (Empty :: Set v -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (Empty :: Set v -> Type) = Set ([] :: [v])

data Singleton :: v -> Exp (Set v) Source #

Singleton

Example

Expand

>>> :kind! Eval (Singleton 1)
Eval (Singleton 1) :: Set Nat
= 'Set '[1]

Instances

type Eval (Singleton v :: Set a -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (Singleton v :: Set a -> Type) = Set (v ': ([] :: [a]))

data Insert :: v -> Set v -> Exp (Set v) Source #

Insert

Example

Expand

>>> :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]

Instances

type Eval (Insert v (Set lst) :: Set a -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (Insert v (Set lst) :: Set a -> Type) = If (Eval (Elem v lst)) (Set lst) (Set (v ': lst))

data Delete :: v -> Set v -> Exp (Set v) Source #

Delete

Example

Expand

>>> :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]

Instances

type Eval (Delete v (Set lst) :: Set a -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (Delete v (Set lst) :: Set a -> Type) = Set (Eval (Filter (Not <=< (TyEq v :: a -> Bool -> Type)) lst))

data PowerSet :: Set a -> Exp (Set (Set a)) Source #

Calculate the power sets of a given type-level list. The algorithm is based on Gray codes.

Example

Expand

>>> :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]]

Instances

type Eval (PowerSet (Set lst) :: Set (Set v) -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (PowerSet (Set lst) :: Set (Set v) -> Type)

Combine

data Union :: Set v -> Set v -> Exp (Set v) Source #

Type-level set union.

Example

Expand

>>> :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]

Instances

type Eval (Union (Set lst1) (Set lst2) :: Set a -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (Union (Set lst1) (Set lst2) :: Set a -> Type)

data Difference :: Set v -> Set v -> Exp (Set v) Source #

Type-level set difference.

Example

Expand

>>> :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]

Instances

type Eval (Difference (Set lst1) (Set lst2) :: Set a -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (Difference (Set lst1) (Set lst2) :: Set a -> Type)

data Intersection :: Set v -> Set v -> Exp (Set v) Source #

Type-level set intersection.

Example

Expand

>>> :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]

Instances

type Eval (Intersection (Set lst1) (Set lst2) :: Set a -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (Intersection (Set lst1) (Set lst2) :: Set a -> Type)

List

data FromList :: [v] -> Exp (Set v) Source #

Use FromList to construct a Set from type-level list.

Example

Expand

>>> :kind! Eval (FromList '[1, 2])
Eval (FromList '[1, 2]) :: Set Nat
= 'Set '[1, 2]

Instances

type Eval (FromList lst :: Set a -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (FromList lst :: Set a -> Type) = Set lst

data ToList :: Set v -> Exp [v] Source #

Get the type-level list out of the Set.

Example

Expand

>>> :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]]

Instances

type Eval (ToList (Set lst) :: [v] -> Type) Source #
Instance details Defined in Fcf.Data.Set type Eval (ToList (Set lst) :: [v] -> Type) = lst