da03b64 · type-level-sets

README+1−1

compare with master

unifiedsplit

@@ -3,7 +3,7 @@ subsets, and split sets. Also included is a "mapping" type constructor that pair

3sets of variable-type pairs, which is used in the paper "Embedding effect systems in Haskell" (Dominic Orchard,

4Tomas Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf>) to embed effect sets.

5

6−A full example can be seen in 'example.hs'. Here is a shorter version:

6+The following shows an example:

7

8 {-# LANGUAGE DataKinds, TypeOperators #-}

9

example.hs+5−7

@@ -1,20 +1,18 @@

1−{-# LANGUAGE DataKinds, TypeOperators, FlexibleInstances, FlexibleContexts, GADTs #-}

1+{-# LANGUAGE DataKinds, TypeOperators #-}

2

3import Data.Type.Set

4

5−instance Nubable ((v :-> a) ': s) => Nubable ((v :-> a) ': (v :-> a) ': s) where

5+foo :: Set '["x" :-> Int, "z" :-> Int, "w" :-> Int]

6− nub (Ext _ (Ext x xs)) = nub (Ext x xs)

7−

8−foo :: Set '["x" :-> Integer, "z" :-> Integer, "w" :-> Integer]

9foo = Ext ((Var :: (Var "x")) :-> 2) $

6foo = Ext ((Var :: (Var "x")) :-> 2) $

10 Ext ((Var :: (Var "z")) :-> 4) $

7 Ext ((Var :: (Var "z")) :-> 4) $

11 Ext ((Var :: (Var "w")) :-> 5) $

8 Ext ((Var :: (Var "w")) :-> 5) $

12 Empty

9 Empty

13

10

14−bar :: Set '["y" :-> Integer, "w" :-> Integer]

11+bar :: Set '["y" :-> Int, "w" :-> Int]

15bar = Ext ((Var :: (Var "y")) :-> 3) $

12bar = Ext ((Var :: (Var "y")) :-> 3) $

16 Ext ((Var :: (Var "w")) :-> 1) $

13 Ext ((Var :: (Var "w")) :-> 1) $

17 Empty

14 Empty

18

15

16+-- GHC can easily infer this type, so an explicit signature not necessary

19−foobar :: Set '["w" :-> Integer, "x" :-> Integer, "y" :-> Integer, "z" :-> Integer]

17+-- foobar :: Set '["w" :-> Int, "x" :-> Int, "y" :-> Integer, "z" :-> Int]

20foobar = foo `union` bar

18foobar = foo `union` bar

src/Data/Type/Set.hs+4−2

@@ -1,7 +1,6 @@

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

2 MultiParamTypeClasses, FlexibleInstances, PolyKinds, FlexibleContexts,

3− UndecidableInstances, ConstraintKinds, OverlappingInstances, ScopedTypeVariables,

3+ UndecidableInstances, ConstraintKinds, OverlappingInstances, ScopedTypeVariables #-}

4− AllowAmbiguousTypes #-}

5

4

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

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

7 Sort, Sortable, Append(..), Split(..), Cmp,

6 Sort, Sortable, Append(..), Split(..), Cmp,

@@ -111,6 +110,9 @@ instance Nubable '[] where

111instance Nubable '[e] where

110instance Nubable '[e] where

112 nub (Ext x Empty) = Ext x Empty

111 nub (Ext x Empty) = Ext x Empty

113

112

113+instance Nubable (e ': s) => Nubable (e ': e ': s) where

114+ nub (Ext _ (Ext e s)) = nub (Ext e s)

115+

114instance (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),

116instance (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),

115 Nubable (f ': s)) => Nubable (e ': f ': s) where

117 Nubable (f ': s)) => Nubable (e ': f ': s) where

116 nub (Ext e (Ext f s)) = Ext e (nub (Ext f s))

118 nub (Ext e (Ext f s)) = Ext e (nub (Ext f s))