X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=GHC%2FHetMet%2FArrow.hs;h=f40ed5b7eeab412d104b314f8174e6b8597f656d;hb=7406d7e6d3e42c96a67fb233e7dc1847b9c64418;hp=5bead2c491e4720b9170f87820d4bd95bb29933c;hpb=f98950484a7cb01e43352e3d88277a2784cd58bf;p=ghc-base.git diff --git a/GHC/HetMet/Arrow.hs b/GHC/HetMet/Arrow.hs index 5bead2c..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 @@ -48,15 +48,52 @@ instance Arrow a => GArrowReify a (,) () x y x y where ga_reify = arr instance ArrowLoop a => GArrowLoop a (,) () where - ga_loopl = loop - ga_loopr f = loop (ga_swap >>> f >>> ga_swap) + 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