From b77972bb8793136b82db08061fc2b1703499880a Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Fri, 8 Apr 2011 04:05:35 +0000 Subject: [PATCH] add ArrowChoice=>GArrowSum instance --- GHC/HetMet/Arrow.hs | 41 ++++++++++++++++++++++++++++++++++++++--- GHC/HetMet/GArrow.hs | 4 ++-- 2 files changed, 40 insertions(+), 5 deletions(-) diff --git a/GHC/HetMet/Arrow.hs b/GHC/HetMet/Arrow.hs index 5bead2c..08b75b3 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 @@ -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 --- 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 -- 1.7.10.4