Curry Howard Examples

CurryHoward.hs

module CurryHoward where                                                                            
                                                                                                    
                                                                                                    
data And a b = And a b                                                                              
                                                                                                    
data Or a b = Inl a | Inr b                                                                         
                                                                                                    
data Impossible                                                                                     
                                                                                                    
type Not a = a -> Impossible                                                                        
                                                                                                    
type (∧) = And                                                                                      
type (∨) = Or                                                                                       
                                                                                                    
--    (A ∧ B) ⇒ (B ∧ A)                                                                             
and_comm :: a ∧ b -> b ∧ a                                                                          
and_comm (And a b) = And b a                                                                        
                                                                                                    
--    (A ⇒ B) ⇒ (B ⇒ C) ⇒ (A ⇒ C)                                                                   
imp_trans :: (a -> b) -> (b -> c) -> (a -> c)                                                       
imp_trans f g = g . f                                                                               
--imp_trans = flip (.)                                                                              
                                                                                                    
--    (A ⇒ C) ⇒ (B ⇒ C) ⇒ (A ∨ B ⇒ C)                                                               
ac_bc_avbc :: (a -> c) -> (b -> c) -> (a ∨ b) -> c                                                  
ac_bc_avbc f _ (Inl a) = f a                                                                        
ac_bc_avbc _ g (Inr b) = g b                                                                        
                                                                                                    
--    (A ∧ B ⇒ C) ⇒ (A ⇒ B ⇒ C)                                                                     
curry :: (a ∧ b -> c) -> (a -> b -> c)                                                              
curry f a b = f (And a b)                                                                           
                                                                                                    
--    (A ⇒ B ⇒ C) ⇒ (A ∧ B ⇒ C)                                                                     
uncurry_ :: (a -> b -> c) -> (a ∧ b -> c)                                                           
uncurry_ f (And a b) = f a b                                                                        
                                                                                                    
--    ¬A ⇒ (A ⇒ B)                                                                                  
explosion :: Not a -> (a -> b)                                                                      
explosion na a = case na a of

--    ¬(A ∧ ¬A)                                                                                     
no_contradiction :: Not (a ∧ (Not a))                                                               
no_contradiction = \(And a na) -> explosion na a                                                    
                                                                                                    
--    (A ⇒ B) ⇒ (¬B ⇒ ¬A)                                                                           
contraposition :: (a -> b) -> (Not b -> Not a)                                                      
contraposition f nb = nb . f                                                                        
                                                                                                    
--    A ⇒ ¬¬A                                                                                       
a_imp_nna :: a -> Not (Not a)                                                                       
a_imp_nna a = \na -> na a                                                                           
--a_imp_nna = flip ($)                                                                              
                                                                                                    
--    ¬A ∨ B ⇒ (A ⇒ B)                                                                              
or_to_implies :: (Not a) ∨ b -> (a -> b)                                                            
or_to_implies (Inl  na) a = explosion na a                                                          
or_to_implies (Inr  b) _ = b                                                                        
                                                                                                    
split_sum_domain :: ((a ∨ b) -> c) -> (a -> c) ∧ (b -> c)                                           
split_sum_domain f = And (f . Inl) (f . Inr)                                                        
                                                                                                    
--    ¬A ∨ ¬B ⇒ ¬A ∧ ¬B                                                                             
demorgan_1 :: Not (a ∨ b) -> (Not a) ∧ (Not b)                                                      
demorgan_1 = split_sum_domain                                                                       
                                                                                                    
--    ¬A ∧ ¬B ⇒ ¬(A ∨ B)                                                                            
demorgan_2 :: (Not a) ∧ (Not b) -> Not (a ∨ b)                                                      
demorgan_2 (And na nb) = ac_bc_avbc na nb                                                           
                                                                                                    
--    ¬A ∨ ¬B ⇒ ¬(A ∧ B)                                                                            
demorgan_3 :: (Not a) ∨ (Not b) -> Not (a ∧ b)                                                      
demorgan_3 (Inl  na) = \(And a _) -> na a                                                           
demorgan_3 (Inr nb) = \(And _ b) -> nb b                                                            
                                                                                                    
--    ¬¬(A ∨ ¬A)                                                                                    
em_not_false :: Not (Not (a ∨ (Not a)))                                                             
em_not_false = (uncurry_ explosion) . and_comm . demorgan_1