X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=GHC%2FHetMet%2FArrow.hs;h=f40ed5b7eeab412d104b314f8174e6b8597f656d;hb=7406d7e6d3e42c96a67fb233e7dc1847b9c64418;hp=39bd2fe2c680c707c5d560e55c58bf4d8f7dad7b;hpb=5d6e930086fffc10e70fe91fa30ae01d9f75c6a9;p=ghc-base.git

diff --git a/GHC/HetMet/Arrow.hs b/GHC/HetMet/Arrow.hs
index 39bd2fe..f40ed5b 100644
--- 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
@@ -20,7 +20,9 @@ import Control.Category
 -- algorithm often creates overlapping or even undecidable
 -- instance-search problems
 
-instance Arrow a => GArrow a (,) where
+type Id a = a
+
+instance Arrow a => GArrow a (,) () where
   ga_first     =  first
   ga_second    =  second
   ga_cancell   =  arr (\((),x) -> x)
@@ -30,27 +32,68 @@ instance Arrow a => GArrow a (,) where
   ga_assoc     =  arr (\((x,y),z) -> (x,(y,z)))
   ga_unassoc   =  arr (\(x,(y,z)) -> ((x,y),z))
   
-instance Arrow a => GArrowDrop a (,) where
+instance Arrow a => GArrowDrop a (,) () where
   ga_drop      =  arr (\x -> ())
 
-instance Arrow a => GArrowCopy a (,) where
+instance Arrow a => GArrowCopy a (,) () where
   ga_copy      =  arr (\x -> (x,x))
 
-instance Arrow a => GArrowSwap a (,) where
+instance Arrow a => GArrowSwap a (,) () where
   ga_swap      =  arr (\(x,y) -> (y,x))
 
-instance Arrow a => GArrowLiteral a (,) b where
-  ga_literal x = arr (\() -> x)
+instance Arrow a => GArrowConstant a (,) () t t where
+  ga_constant x = arr (\() -> x)
 
-instance Arrow a => GArrowReify a (,) where
+instance Arrow a => GArrowReify a (,) () x y x y where
   ga_reify     =  arr
 
-instance ArrowLoop a => GArrowLoop a (,) where
-  ga_loop      =  loop
+instance ArrowLoop a => GArrowLoop a (,) () where
+  ga_loopr     =  loop
+  ga_loopl  f  =  loop (ga_swap >>> f >>> ga_swap)
+
+instance ArrowApply a => GArrowApply a (,) () a where
+  ga_applyl    = ga_swap >>> app
+  ga_applyr    = app
+
+instance Arrow a => GArrowProd a (,) () where
 
+-- 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 Either Void where
+  ga_never = arr voidImpossible
+  ga_merge = arr merge
+              where
+               merge (Left  x) = x
+               merge (Right x) = x