git.iko.soy/type-level-sets
on master help sign in
swap
e3689279 ahead, 0 behind
5 files changed+46−24
since splitsnapshots
unifiedsplit
changelog.md+5 example2.hs+9 src/Data/Type/Set.hs+13−6 stack.yaml+1−1 type-level-sets.cabal+18−17
changelog.mdnew file+5
@@ -0,0 +1,5 @@
1+ # v0.8.9.0
2+
3+ - GHC 8.4 and 8.6 support.
4+ - Fixed bug in the delete operation.
5+ - Non-membership predicates
example2.hs+9
@@ -1,4 +1,5 @@
11{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, GADTs, StandaloneDeriving #-}
2+{-# LANGUAGE FlexibleContexts #-}
23
34import GHC.TypeLits
45import Data.Type.Set
@@ -19,3 +20,11 @@ bar = asSet $ Ext (S (S Z)) (Ext (S Z) (Ext (S Z) Empty))
1920
2021-- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3]
2122foobar = foo `union` bar
23+
24+nonMemberTest :: NonMember (Natural 0) as => Set as -> ()
25+nonMemberTest set = ()
26+
27+-- nonMemberTest meep is well typed
28+meep = asSet $ Ext (S Z) (Ext (S (S Z)) Empty)
29+-- nonMemberTest morp is ill typed
30+morp = asSet $ Ext (S Z) (Ext (S (S Z)) (Ext Z Empty))
src/Data/Type/Set.hs+13−6
@@ -1,13 +1,13 @@
11{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies,
22 MultiParamTypeClasses, FlexibleInstances, PolyKinds,
33 FlexibleContexts, UndecidableInstances, ConstraintKinds,
4− ScopedTypeVariables #-}
4+ ScopedTypeVariables, TypeInType #-}
55
66module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
77 Sort, Sortable, (:++), Split(..), Cmp, Filter, Flag(..),
88 Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),
99 Delete(..), Proxy(..), remove, Remove, (:\),
10− Member) where
10+ Member(..), NonMember, MemberP(..)) where
1111
1212import GHC.TypeLits
1313import Data.Type.Bool
@@ -16,7 +16,7 @@ import Data.Type.Equality
1616data Proxy (p :: k) = Proxy
1717
1818-- Value-level 'Set' representation, essentially a list
19−data Set (n :: [k]) :: * where
19+data Set (n :: [k]) where
2020 {--| Construct an empty set -}
2121 Empty :: Set '[]
2222 {--| Extend a set with an element -}
@@ -77,7 +77,7 @@ append (Ext e xs) ys = Ext e (append xs ys)
7777{-| Delete elements from a set -}
7878type family (m :: [k]) :\ (x :: k) :: [k] where
7979 '[] :\ x = '[]
80− (x ': xs) :\ x = xs
80+ (x ': xs) :\ x = xs :\ x
8181 (y ': xs) :\ x = y ': (xs :\ x)
8282
8383class Remove s t where
@@ -86,8 +86,8 @@ class Remove s t where
8686instance Remove '[] t where
8787 remove Empty Proxy = Empty
8888
89−instance {-# OVERLAPS #-} Remove (x ': xs) x where
90− remove (Ext _ xs) Proxy = xs
89+instance {-# OVERLAPS #-} Remove xs x => Remove (x ': xs) x where
90+ remove (Ext _ xs) x@Proxy = remove xs x
9191
9292instance {-# OVERLAPPABLE #-} (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x)
9393 => Remove (y ': xs) x where
@@ -227,3 +227,10 @@ instance {-# OVERLAPS #-} Member a (a ': s) where
227227
228228instance {-# OVERLAPPABLE #-} Member a s => Member a (b ': s) where
229229 member a (Ext _ xs) = member a xs
230+
231+type family MemberP a s :: Bool where
232+ MemberP a '[] = False
233+ MemberP a (a ': s) = True
234+ MemberP a (b ': s) = MemberP a s
235+
236+type NonMember a s = MemberP a s ~ False
stack.yaml+1−1
@@ -1,7 +1,7 @@
11# For more information, see: https://github.com/commercialhaskell/stack/wiki/stack.yaml
22
33# Specifies the GHC version and set of packages available (e.g., lts-3.5, nightly-2015-09-21, ghc-7.10.2)
4−resolver: nightly-2016-07-18
4+resolver: lts-12.7
55
66# Local packages, usually specified by relative directory name
77packages:
type-level-sets.cabal+18−17
@@ -1,14 +1,14 @@
11name: type-level-sets
2−version: 0.8.7.0
2+version: 0.8.9.0
33synopsis: Type-level sets and finite maps (with value-level counterparts)
4−description:
4+description:
55 This package provides type-level sets (no duplicates, sorted to provide a normal form) via 'Set' and type-level
66 finite maps via 'Map', with value-level counterparts.
77 .
8− Described in the paper \"Embedding effect systems in Haskell\" by Dominic Orchard
9− and Tomas Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf> (Haskell Symposium, 2014). This version now uses Quicksort to normalise the representation.
8+ Described in the paper \"Embedding effect systems in Haskell\" by Dominic Orchard
9+ and Tomas Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf> (Haskell Symposium, 2014). This version now uses Quicksort to normalise the representation.
1010 .
11− Here is a brief example for finite maps:
11+ Here is a brief example for finite maps:
1212 .
1313 >
1414 > import Data.Type.Map
@@ -19,26 +19,26 @@ description:
1919 > combine x y = x + y
2020 >
2121 > foo :: Map '["x" :-> Int, "z" :-> Bool, "w" :-> Int]
22− > foo = Ext (Var :: (Var "x")) 2
23− > $ Ext (Var :: (Var "z")) True
24− > $ Ext (Var :: (Var "w")) 5
25− > $ Empty
22+ > foo = Ext (Var :: (Var "x")) 2
23+ > $ Ext (Var :: (Var "z")) True
24+ > $ Ext (Var :: (Var "w")) 5
25+ > $ Empty
2626 >
2727 > bar :: Map '["y" :-> Int, "w" :-> Int]
2828 > bar = Ext (Var :: (Var "y")) 3
2929 > $ Ext (Var :: (Var "w")) 1
3030 > $ Empty
31− >
31+ >
3232 > -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Bool]
3333 > foobar = foo `union` bar
3434 .
3535 The 'Map' type for 'foobar' here shows the normalised form (sorted with no duplicates).
3636 The type signatures is commented out as it can be infered. Running the example we get:
3737 .
38− > >>> foobar
38+ > >>> foobar
3939 > {w :-> 6, x :-> 2, y :-> 3, z :-> True}
4040 .
41− Thus, we see that the values for \"w\" are added together.
41+ Thus, we see that the values for \"w\" are added together.
4242 For sets, here is an example:
4343 .
4444 > import GHC.TypeLits
@@ -48,7 +48,7 @@ description:
4848 > data Natural (a :: Nat) where
4949 > Z :: Natural 0
5050 > S :: Natural n -> Natural (n + 1)
51− >
51+ >
5252 > -- foo :: Set '[Natural 0, Natural 1, Natural 3]
5353 > foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty))
5454 >
@@ -63,15 +63,15 @@ description:
6363license: BSD3
6464license-file: LICENSE
6565category: Type System, Data Structures
66−copyright: 2013-16 University of Cambridge
66+copyright: 2013-18 University of Kent
6767author: Dominic Orchard
6868maintainer: Dominic Orchard
6969stability: experimental
7070build-type: Simple
7171cabal-version: >= 1.6
72−tested-with: GHC >= 8.0.1
72+tested-with: GHC >= 8.2.2
7373
74−extra-source-files: example.hs, example2.hs
74+extra-source-files: example.hs, example2.hs, changelog.md
7575
7676
7777source-repository head
@@ -80,10 +80,11 @@ source-repository head
8080
8181library
8282 hs-source-dirs: src
83+ other-extensions: TypeInType
8384
8485
8586 exposed-modules: Data.Type.Set
8687 Data.Type.Map
87−
88+
8889 build-depends: base < 5,
8990 ghc-prim