-{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFlexibleInstances -XFunctionalDependencies #-}
+{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFlexibleInstances -XFunctionalDependencies -XEmptyDataDecls #-}
-----------------------------------------------------------------------------
-- |
-- Module : GHC.HetMet.Arrow
-- 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)
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