clean-unions 0.0.1 → 0.0.2

raw patch · 2 files changed

+20/−15 lines, 2 files

Files

• clean-unions.cabal +1/−1
• src/Data/OpenUnion1/Clean.hs +19/−14

@@ -1,5 +1,5 @@ name:                clean-unions
-version:             0.0.1
+version:             0.0.2
 synopsis:            Open unions without need for Typeable
 -- description:         
 homepage:            https://github.com/fumieval/clean-unions

@@ -15,8 +15,9 @@   , UndecidableInstances
   , OverlappingInstances #-}
 module Data.OpenUnion1.Clean (Union(..), Nil, List(..), (|>)(..), (||>), exhaust, simply, (∈)(), Member, liftU, (⊆)(..), Include) where
-import Data.Proxy
 
+data Proxy a = Proxy
+
 -- | Poly-kinded list
 data List a = Empty | a :> List a
 
@@ -28,6 +29,9 @@ 
 type instance f |> Union s = Union (f :> s)
 
+-- | Combine two 'List's.
+type family (s :: List k) ++> (t :: List k) :: List k
+
 -- | An uninhabited union.
 type Nil = Union Empty
 
@@ -57,32 +61,33 @@ simply :: (f a -> r) -> ((f |> Nil) a -> r)
 simply f = f ||> exhaust
 
-data MemberInfo f s where
-  Head :: MemberInfo f (f :> s)
-  Tail :: (f ∈ s) => MemberInfo f (g :> s)
+data Position f s where
+  Zero :: Position f (f :> s)
+  Succ :: Position f s -> Position f (g :> s)
 
 -- | Constraint @f ∈ s@ indicates that @f@ is an element of a type-level list @s@.
-class f　∈ s | s -> f where
-  query :: Proxy f -> Proxy s -> MemberInfo f s
+class f ∈ s | s -> f where
+  query :: Proxy f -> Proxy s -> Position f s
 
 infix 4 ∈
 infix 4 ⊆
 
-instance f ∈ (f :> s) where query _ _ = Head
-instance (f　∈ s) => f　∈ (g :> s) where query _ _ = Tail
+instance f ∈ (f :> s) where query _ _ = Zero
+instance (f ∈ s) => f ∈ (g :> s) where query p q = Succ (query p (Proxy :: Proxy s))
 
 -- | Lift some value into a union.
-liftU :: forall s f a. (f　∈ s) => f a -> Union s a
-liftU f = case query (Proxy :: Proxy f) (Proxy :: Proxy s) of
-  Head -> Single f
-  Tail -> Union (liftU f)
+liftU :: forall s f a. (f ∈ s) => f a -> Union s a
+liftU f = go $ query (Proxy :: Proxy f) (Proxy :: Proxy s) where
+  go :: forall t. Position f t -> Union t a
+  go Zero = Single f
+  go (Succ q) = Union (go q)
 
 -- | Type-level inclusion characterized by 'reunion'.
-class s　⊆ t where
+class s ⊆ t where
   -- | Lift a union into equivalent or larger one, permuting elements if necessary.
   reunion :: Union s a -> Union t a
 
-instance (f ∈ t, s　⊆ t) => (f :> s)　⊆ t where
+instance (f ∈ t, s ⊆ t) => (f :> s) ⊆ t where
   reunion (Single f) = liftU f
   reunion (Union s) = reunion s