master..437855c · type-level-sets

git.iko.soy/type-level-sets

on 437855c help sign in

changelog.mddeleted−5

since splitsnapshots

unifiedsplit

@@ -1,5 +0,0 @@

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,5 +1,4 @@

1{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, GADTs, StandaloneDeriving #-}

2−{-# LANGUAGE FlexibleContexts #-}

4import GHC.TypeLits

3import GHC.TypeLits

5import Data.Type.Set

4import Data.Type.Set

@@ -20,11 +19,3 @@ bar = asSet $ Ext (S (S Z)) (Ext (S Z) (Ext (S Z) Empty))

21-- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3]

20-- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3]

22foobar = foo `union` bar

21foobar = 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+6−13

@@ -1,13 +1,13 @@

1{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies,

2 MultiParamTypeClasses, FlexibleInstances, PolyKinds,

3 FlexibleContexts, UndecidableInstances, ConstraintKinds,

4− ScopedTypeVariables, TypeInType #-}

4+ ScopedTypeVariables #-}

6module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,

7 Sort, Sortable, (:++), Split(..), Cmp, Filter, Flag(..),

8 Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),

9 Delete(..), Proxy(..), remove, Remove, (:\),

10− Member(..), NonMember, MemberP(..)) where

10+ Member) where

12import GHC.TypeLits

13import Data.Type.Bool

@@ -16,7 +16,7 @@ import Data.Type.Equality

16data Proxy (p :: k) = Proxy

18-- Value-level 'Set' representation, essentially a list

19−data Set (n :: [k]) where

19+data Set (n :: [k]) :: * where

20 {--| Construct an empty set -}

21 Empty :: Set '[]

22 {--| Extend a set with an element -}

@@ -77,7 +77,7 @@ append (Ext e xs) ys = Ext e (append xs ys)

77{-| Delete elements from a set -}

78type family (m :: [k]) :\ (x :: k) :: [k] where

79 '[] :\ x = '[]

80− (x ': xs) :\ x = xs :\ x

80+ (x ': xs) :\ x = xs

81 (y ': xs) :\ x = y ': (xs :\ x)

83class Remove s t where

@@ -86,8 +86,8 @@ class Remove s t where

86instance Remove '[] t where

87 remove Empty Proxy = Empty

89−instance {-# OVERLAPS #-} Remove xs x => Remove (x ': xs) x where

89+instance {-# OVERLAPS #-} Remove (x ': xs) x where

90− remove (Ext _ xs) x@Proxy = remove xs x

90+ remove (Ext _ xs) Proxy = xs

92instance {-# OVERLAPPABLE #-} (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x)

93 => Remove (y ': xs) x where

@@ -227,10 +227,3 @@ instance {-# OVERLAPS #-} Member a (a ': s) where

227

228instance {-# OVERLAPPABLE #-} Member a s => Member a (b ': s) where

229 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 @@

1# For more information, see: https://github.com/commercialhaskell/stack/wiki/stack.yaml

3# Specifies the GHC version and set of packages available (e.g., lts-3.5, nightly-2015-09-21, ghc-7.10.2)

4−resolver: lts-12.7

4+resolver: nightly-2016-07-18

6# Local packages, usually specified by relative directory name

7packages:

type-level-sets.cabal+17−18

@@ -1,14 +1,14 @@

1name: type-level-sets

2−version: 0.8.9.0

2+version: 0.8.7.0

3synopsis: Type-level sets and finite maps (with value-level counterparts)

4−description:

4+description:

5 This package provides type-level sets (no duplicates, sorted to provide a normal form) via 'Set' and type-level

6 finite maps via 'Map', with value-level counterparts.

7 .

8− Described in the paper \"Embedding effect systems in Haskell\" by Dominic Orchard

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.

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.

10 .

11− Here is a brief example for finite maps:

11+ Here is a brief example for finite maps:

12 .

13 >

14 > import Data.Type.Map

@@ -19,26 +19,26 @@ description:

19 > combine x y = x + y

20 >

21 > foo :: Map '["x" :-> Int, "z" :-> Bool, "w" :-> Int]

22− > foo = Ext (Var :: (Var "x")) 2

22+ > foo = Ext (Var :: (Var "x")) 2

23− > $ Ext (Var :: (Var "z")) True

23+ > $ Ext (Var :: (Var "z")) True

24− > $ Ext (Var :: (Var "w")) 5

24+ > $ Ext (Var :: (Var "w")) 5

25− > $ Empty

25+ > $ Empty

26 >

27 > bar :: Map '["y" :-> Int, "w" :-> Int]

28 > bar = Ext (Var :: (Var "y")) 3

29 > $ Ext (Var :: (Var "w")) 1

30 > $ Empty

31− >

31+ >

32 > -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Bool]

33 > foobar = foo `union` bar

34 .

35 The 'Map' type for 'foobar' here shows the normalised form (sorted with no duplicates).

36 The type signatures is commented out as it can be infered. Running the example we get:

37 .

38− > >>> foobar

38+ > >>> foobar

39 > {w :-> 6, x :-> 2, y :-> 3, z :-> True}

40 .

41− Thus, we see that the values for \"w\" are added together.

41+ Thus, we see that the values for \"w\" are added together.

42 For sets, here is an example:

43 .

44 > import GHC.TypeLits

@@ -48,7 +48,7 @@ description:

48 > data Natural (a :: Nat) where

49 > Z :: Natural 0

50 > S :: Natural n -> Natural (n + 1)

51− >

51+ >

52 > -- foo :: Set '[Natural 0, Natural 1, Natural 3]

53 > foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty))

54 >

@@ -63,15 +63,15 @@ description:

63license: BSD3

64license-file: LICENSE

65category: Type System, Data Structures

66−copyright: 2013-18 University of Kent

66+copyright: 2013-16 University of Cambridge

67author: Dominic Orchard

68maintainer: Dominic Orchard

69stability: experimental

70build-type: Simple

71cabal-version: >= 1.6

72−tested-with: GHC >= 8.2.2

72+tested-with: GHC >= 8.0.1

74−extra-source-files: example.hs, example2.hs, changelog.md

74+extra-source-files: example.hs, example2.hs

77source-repository head

@@ -80,11 +80,10 @@ source-repository head

81library

82 hs-source-dirs: src

83− other-extensions: TypeInType

86 exposed-modules: Data.Type.Set

85 exposed-modules: Data.Type.Set

87 Data.Type.Map

86 Data.Type.Map

88−

87+

89 build-depends: base < 5,

88 build-depends: base < 5,

90 ghc-prim

89 ghc-prim