add ArrowChoice=>GArrowSum instance

diff --git a/GHC/HetMet/Arrow.hs b/GHC/HetMet/Arrow.hs
index 5bead2c..08b75b3 100644 (file)
--- a/GHC/HetMet/Arrow.hs
+++ b/GHC/HetMet/Arrow.hs
@@ -1,4 +1,4 @@
-{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFlexibleInstances -XFunctionalDependencies #-}
+{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFlexibleInstances -XFunctionalDependencies -XEmptyDataDecls #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  GHC.HetMet.Arrow
@@ -55,8 +55,43 @@ instance ArrowApply a => GArrowApply a (,) () a where
   ga_applyl    = ga_swap >>> app
   ga_applyr    = app
 
-
-
+-- The uninhabited type
+data Void
+
+-- In Coq we could simply prove that these cases are impossible; in Haskell we need to have some faith.
+voidImpossible :: Void -> a
+voidImpossible = error "this is impossible; you have a bug in your compiler"
+
+instance ArrowChoice a => GArrow a Either Void where
+  ga_first     =  left
+  ga_second    =  right
+  ga_uncancell =  arr Right
+  ga_uncancelr =  arr Left
+  ga_cancell   =  arr unVoidLeft
+                   where
+                    unVoidLeft  (Left  v) = voidImpossible v
+                    unVoidRight (Right x) = x
+  ga_cancelr   =  arr unVoidRight
+                   where
+                    unVoidRight (Left  x) = x
+                    unVoidRight (Right v) = voidImpossible v
+  ga_assoc     =  arr eitherAssoc
+                   where
+                    eitherAssoc (Left (Left  x)) = Left         x
+                    eitherAssoc (Left (Right y)) = Right (Left  y)
+                    eitherAssoc (Right       z ) = Right (Right z)
+  ga_unassoc   =  arr eitherUnAssoc
+                   where
+                    eitherUnAssoc (Left         x ) = Left  (Left  x)
+                    eitherUnAssoc (Right (Left  y)) = Left  (Right y)
+                    eitherUnAssoc (Right (Right z)) = Right        z
+
+instance ArrowChoice a => GArrowSum a (,) () Void Either where
+  ga_never = arr voidImpossible
+  ga_merge = arr merge
+              where
+               merge (Left  x) = x
+               merge (Right x) = x
 
 
 

diff --git a/GHC/HetMet/GArrow.hs b/GHC/HetMet/GArrow.hs
index 88f84fb..9f8aab1 100644 (file)
--- a/GHC/HetMet/GArrow.hs
+++ b/GHC/HetMet/GArrow.hs
@@ -83,8 +83,8 @@ class (GArrow     g (**)  u,
 class (GArrow     g (**)  u,
        GArrow     g (<+>) v) => 
        GArrowSum  g (**)  u v (<+>) where
-  ga_merge :: g (x**x) x
-  ga_never :: g v      x
+  ga_merge :: g (x<+>x) x
+  ga_never :: g v       x