type-level-sets (empty) → 0.5
raw patch · 5 files changed
+325/−0 lines, 5 filesdep +basedep +ghc-primsetup-changed
Dependencies added: base, ghc-prim
Files
- LICENSE +26/−0
- Setup.hs +6/−0
- example.hs +18/−0
- src/Data/Type/Set.hs +214/−0
- type-level-sets.cabal +61/−0
+ LICENSE view
@@ -0,0 +1,26 @@+Copyright (c) 2014, Dominic Orchard++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,6 @@+module Main (main) where++import Distribution.Simple++main :: IO ()+main = defaultMain
+ example.hs view
@@ -0,0 +1,18 @@+{-# LANGUAGE DataKinds, TypeOperators #-}++import Data.Type.Set++foo :: Set '["x" :-> Int, "z" :-> Int, "w" :-> Int]+foo = Ext ((Var :: (Var "x")) :-> 2) $+ Ext ((Var :: (Var "z")) :-> 4) $+ Ext ((Var :: (Var "w")) :-> 5) $+ Empty ++bar :: Set '["y" :-> Int, "w" :-> Int]+bar = Ext ((Var :: (Var "y")) :-> 3) $+ Ext ((Var :: (Var "w")) :-> 1) $+ Empty ++-- GHC can easily infer this type, so an explicit signature not necessary+-- foobar :: Set '["w" :-> Int, "x" :-> Int, "y" :-> Integer, "z" :-> Int]+foobar = foo `union` bar
+ src/Data/Type/Set.hs view
@@ -0,0 +1,214 @@+{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, + MultiParamTypeClasses, FlexibleInstances, PolyKinds, FlexibleContexts,+ UndecidableInstances, ConstraintKinds, OverlappingInstances, ScopedTypeVariables #-}++module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append, + Sort, Sortable, Append(..), Split(..), Cmp, + Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),+ (:->)(..), Var(..)) where++import GHC.TypeLits+import Data.Type.Bool+import Data.Type.Equality+import Data.Proxy++{-| Core Set definition, in terms of lists -}+data Set (n :: [*]) where+ Empty :: Set '[]+ Ext :: e -> Set s -> Set (e ': s)++instance Show (Set '[]) where+ show Empty = "{}"++instance (Show e, Show' (Set s)) => Show (Set (e ': s)) where+ show (Ext e s) = "{" ++ show e ++ (show' s) ++ "}" ++class Show' t where+ show' :: t -> String+instance Show' (Set '[]) where+ show' Empty = ""+instance (Show' (Set s), Show e) => Show' (Set (e ': s)) where+ show' (Ext e s) = ", " ++ show e ++ (show' s)++{-| At the type level, normalise the list form to the set form -}+type AsSet s = Nub (Sort s)++{-| At the value level, noramlise the list form to the set form -}+asSet :: (Sortable s, Nubable (Sort s)) => Set s -> Set (AsSet s)+asSet x = nub (quicksort x)++{-| Predicate to check if in the set form -}+type IsSet s = (s ~ Nub (Sort s))++{-| Useful properties to be able to refer to someties -}+type SetProperties f = (Union f '[] ~ f, Split f '[] f, + Union '[] f ~ f, Split '[] f f, + Union f f ~ f, Split f f f,+ Unionable f '[], Unionable '[] f)++{-- Union --}++{-| Union of sets -}+type Union s t = Nub (Sort (Append s t))++union :: (Unionable s t) => Set s -> Set t -> Set (Union s t)+union s t = nub (quicksort (append s t))++type Unionable s t = (Sortable (Append s t), Nubable (Sort (Append s t)))++{-| List append (essentially set disjoint union) -}+type family Append (s :: [k]) (t :: [k]) :: [k] where+ Append '[] t = t+ Append (x ': xs) ys = x ': (Append xs ys)++append :: Set s -> Set t -> Set (Append s t)+append Empty x = x+append (Ext e xs) ys = Ext e (append xs ys)++{-| Useful alias for append -}+type (s :: [k]) :++ (t :: [k]) = Append s t++{-| Splitting a union a set, given the sets we want to split it into -}+class Split s t st where+ -- where st ~ Union s t+ split :: Set st -> (Set s, Set t) ++instance Split '[] '[] '[] where+ split Empty = (Empty, Empty)++instance Split s t st => Split (x ': s) (x ': t) (x ': st) where+ split (Ext x st) = let (s, t) = split st+ in (Ext x s, Ext x t)++instance Split s t st => Split (x ': s) t (x ': st) where+ split (Ext x st) = let (s, t) = split st+ in (Ext x s, t) ++instance (Split s t st) => Split s (x ': t) (x ': st) where+ split (Ext x st) = let (s, t) = split st+ in (s, Ext x t) ++++{-| Remove duplicates from a sorted list -}+type family Nub t where+ Nub '[] = '[]+ Nub '[e] = '[e]+ Nub (e ': e ': s) = Nub (e ': s)+ Nub (e ': f ': s) = e ': Nub (f ': s)++{-| Value-level counterpart to the type-level 'Nub'+ Note: the value-level case for equal types is not define here, + but should be given per-application, e.g., custom 'merging' behaviour may be required -}++class Nubable t where+ nub :: Set t -> Set (Nub t)++instance Nubable '[] where+ nub Empty = Empty++instance Nubable '[e] where+ nub (Ext x Empty) = Ext x Empty++instance Nubable (e ': s) => Nubable (e ': e ': s) where+ nub (Ext _ (Ext e s)) = nub (Ext e s)++instance (Nub (e ': f ': s) ~ (e ': Nub (f ': s)), + Nubable (f ': s)) => Nubable (e ': f ': s) where+ nub (Ext e (Ext f s)) = Ext e (nub (Ext f s))+++{-| Construct a subsetset 's' from a superset 't' -}+class Subset s t where+ subset :: Set t -> Set s++instance Subset '[] '[] where + subset xs = Empty++instance Subset '[] (x ': t) where + subset xs = Empty++instance Subset s t => Subset (x ': s) (x ': t) where+ subset (Ext x xs) = Ext x (subset xs)+++{-| Type-level quick sort for normalising the representation of sets -}+type family Sort (xs :: [k]) :: [k] where+ Sort '[] = '[]+ Sort (x ': xs) = ((Sort (Filter FMin x xs)) :++ '[x]) :++ (Sort (Filter FMax x xs))++data Flag = FMin | FMax++type family Filter (f :: Flag) (p :: k) (xs :: [k]) :: [k] where+ Filter f p '[] = '[]+ Filter FMin p (x ': xs) = If (Cmp x p == LT) (x ': (Filter FMin p xs)) (Filter FMin p xs) + Filter FMax p (x ': xs) = If (Cmp x p == GT || Cmp x p == EQ) (x ': (Filter FMax p xs)) (Filter FMax p xs) ++{-| Value-level quick sort that respects the type-level ordering -}+class Sortable xs where+ quicksort :: Set xs -> Set (Sort xs)++instance Sortable '[] where+ quicksort Empty = Empty++instance (Sortable (Filter FMin p xs),+ Sortable (Filter FMax p xs), FilterV FMin p xs, FilterV FMax p xs) => Sortable (p ': xs) where+ quicksort (Ext p xs) = ((quicksort (less p xs)) `append` (Ext p Empty)) `append` (quicksort (more p xs))+ where less = filterV (Proxy::(Proxy FMin))+ more = filterV (Proxy::(Proxy FMax))++{- Filter out the elements less-than or greater-than-or-equal to the pivot -}+class FilterV (f::Flag) p xs where+ filterV :: Proxy f -> p -> Set xs -> Set (Filter f p xs)++instance FilterV f p '[] where+ filterV _ p Empty = Empty++instance (Conder ((Cmp x p) == LT), FilterV FMin p xs) => FilterV FMin p (x ': xs) where+ filterV f@Proxy p (Ext x xs) = cond (Proxy::(Proxy ((Cmp x p) == LT)))+ (Ext x (filterV f p xs)) (filterV f p xs) ++instance (Conder (((Cmp x p) == GT) || ((Cmp x p) == EQ)), FilterV FMax p xs) => FilterV FMax p (x ': xs) where+ filterV f@Proxy p (Ext x xs) = cond (Proxy::(Proxy (((Cmp x p) == GT) || ((Cmp x p) == EQ))))+ (Ext x (filterV f p xs)) (filterV f p xs) ++class Conder g where+ cond :: Proxy g -> Set s -> Set t -> Set (If g s t)++instance Conder True where+ cond _ s t = s++instance Conder False where+ cond _ s t = t++{-| Open-family for the ordering operation in the sort -}++type family Cmp (a :: k) (b :: k) :: Ordering++{-| Pair a symbol (represetning a variable) with a type -}+infixl 2 :->+data (k :: Symbol) :-> (v :: *) = (Var k) :-> v++data Var (k :: Symbol) where Var :: Var k + {-| Some special defaults for some common names -}+ X :: Var "x"+ Y :: Var "y"+ Z :: Var "z"+++instance (Show (Var k), Show v) => Show (k :-> v) where+ show (k :-> v) = "(" ++ show k ++ " :-> " ++ show v ++ ")"+instance Show (Var "x") where+ show X = "x"+ show Var = "Var"+instance Show (Var "y") where+ show Y = "y"+ show Var = "Var"+instance Show (Var "z") where+ show Z = "z"+ show Var = "Var"+instance Show (Var v) where+ show _ = "Var"++{-| Symbol comparison -}+type instance Cmp (v :-> a) (u :-> b) = CmpSymbol v u
+ type-level-sets.cabal view
@@ -0,0 +1,61 @@+name: type-level-sets+version: 0.5+synopsis: Type-level sets (with value-level counterparts and various operations)+description: + This package provides type-level sets (no duplicates, sorted to provide a nomral form) via 'Set', + with value-level counterparts. Described in the paper \"Embedding effect systems in Haskell\" by Dominic Orchard + and Tomas Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf> (Haskell Symposium, 2014)+ .+ Here is a brief example: + .+ >+ > import Data.Type.Set+ >+ > foo :: Set '["x" :-> Int, "z" :-> Int, "w" :-> Int]+ > foo = Ext ((Var :: (Var "x")) :-> 2) $+ > Ext ((Var :: (Var "z")) :-> 4) $+ > Ext ((Var :: (Var "w")) :-> 5) $+ > Empty + >+ > bar :: Set '["y" :-> Int, "w" :-> Int]+ > bar = Ext ((Var :: (Var "y")) :-> 3) $+ > Ext ((Var :: (Var "w")) :-> 1) $+ > Empty+ > + > -- foobar :: Set '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Int]+ > foobar = foo `union` bar+ .+ The 'Set' type for 'foobar' here shows the normalised form (sorted with no duplicates).+ The type signatures is commented out as it can be infered. Running the example we get:+ .+ > >>> foobar + > [(Var :-> 1), (Var :-> 2), (Var :-> 3), (Var :-> 4)]+ .+ Thus, we see that the first value paired with the \"w\" variable is dropped.+ .+license: BSD3+license-file: LICENSE+category: Type System, Data Structures+copyright: 2013-14 University of Cambridge+author: Dominic Orchard+maintainer: Dominic Orchard+stability: experimental+build-type: Simple+cabal-version: >= 1.6+tested-with: GHC == 7.8.2++extra-source-files: example.hs+++source-repository head+ type: git+ location: https://github.com/dorchard/type-level-sets++library+ hs-source-dirs: src+++ exposed-modules: Data.Type.Set+ + build-depends: base < 5,+ ghc-prim