git.iko.soy/type-level-sets
on master help sign in
specialised example of set difference + showing functions
3941daedominic
example-set.hs+22−6
compare with master
unifiedsplit
@@ -1,4 +1,4 @@
1−{-# LANGUAGE DataKinds, KindSignatures, GADTs, TypeOperators, TypeFamilies, PolyKinds, EmptyDataDecls #-}
1+{-# LANGUAGE DataKinds, KindSignatures, GADTs, TypeOperators, TypeFamilies, PolyKinds, EmptyDataDecls, StandaloneDeriving #-}
2{-# OPTIONS_GHC -fplugin=TySet #-}
2{-# OPTIONS_GHC -fplugin=TySet #-}
3
3
4import GHC.TypeLits
4import GHC.TypeLits
@@ -6,18 +6,34 @@ import TySet
6
6
7data Container (a :: *) where
7data Container (a :: *) where
8 Empty :: Container (Set '[])
8 Empty :: Container (Set '[])
9− Ext :: a -> Container (Set s) -> Container (Set (Union '[a] s))
9+ Ext :: Show a => a -> Container (Set s) -> Container (Set (Union '[a] s))
10+
11+instance Show (Container a) where
12+ show Empty = "Empty"
13+ show (Ext x xs) = "Ext " ++ show x ++ " " ++ show xs
10
14
11data Natural (a :: Nat) where
15data Natural (a :: Nat) where
12 Z :: Natural 0
16 Z :: Natural 0
13 S :: Natural n -> Natural (n + 1)
17 S :: Natural n -> Natural (n + 1)
14
18
19+instance Show (Natural a) where
20+ show Z = "Z"
21+ show (S n) = "S " ++ (show n)
22+
15-- Should be typeable with the plugin
23-- Should be typeable with the plugin
16−{-
24+
17−foo :: Container (Set '[Natural 1, Natural 2, Natural 3])
25+foo :: Container (Set '[Natural 3, Natural 2, Natural 1])
18foo = Ext (S $ S Z) (Ext (S Z) (Ext (S $ S $ S Z) Empty))
26foo = Ext (S $ S Z) (Ext (S Z) (Ext (S $ S $ S Z) Empty))
19−-}
20
27
28+foo2 :: Container (Set '[Natural 2, Natural 1])
29+foo2 = Ext (S $ S Z) (Ext (S Z) Empty)
30+
31+bar :: (Container (Set '[Natural 2, Natural 1])) -> Container (Set '[Natural 1])
32+bar (Ext (S (S Z)) (Ext (S Z) Empty)) = Ext (S Z) Empty
33+bar (Ext (S Z) (Ext (S (S Z)) Empty)) = Ext (S Z) Empty
34+
35+{-
21dup :: Container (Set s) -> Container (Set (Union s s))
36dup :: Container (Set s) -> Container (Set (Union s s))
22dup Empty = Empty
37dup Empty = Empty
23−dup (Ext x xs) = Ext x (Ext x (dup xs))
38+dup (Ext x xs) = Ext x (Ext x (dup xs))
39+-}