content: {-# OPTIONS_GHC -Werror=incomplete-patterns #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE FunctionalDependencies #-}
  {-# LANGUAGE TypeOperators #-}
  
  module Sl where
  
  data Zero
  data One = True
  
  -- newtype a <-> b = Bijection (a->b, b->a)
  
  -- Modus Ponens (MP)
  mp :: (a->b) -> a->b
  mp = ($)
  
  -- Transitive (TR)
  tr :: (a->b)->(b->c)->(a->c)
  tr = flip (.)
  
  -- Explosion (X)
  x :: Zero -> a
  x z = case z of {}
  
  -- Conjunction Elimination (AE)
  class Ae a b c | a b -> c where
    ae :: (a, b)->c
  instance Ae a b a where
    ae (a, _) = a
  instance Ae a b b where
    ae (_, b) = b
  
  -- Modus Tollens (MT)
  mt ::(a->b) -> (b->Zero) -> (a->Zero)
  mt = tr
  
  -- Disjunctive Syllogism (DE)
  class De either ab result | either ab -> result where
    de :: either -> (ab->Zero) ->result
  instance De (Either a b) a b where
    de (Right b) _ = b
    de (Left a) f = x (f a)
  instance De (Either a b) b a where
    de (Left a) _ = a
    de (Right b) f = x (f b)
  
  -- Disjunction Introduction
  class Di a b c | a b -> c where
    di :: c -> Either a b
  instance Di a b a where
    di = Left
  instance Di a b b where
    di = Right
  
  -- Conjunction Introduction (AI)
  class Ai a b c | a b -> c where
    ai :: a->b->c
  instance Ai a b (a, b) where
    ai a b = (a, b)
  instance Ai b a (a, b) where
    ai b a = (a, b)
  
  -- Double Negation (DN)
  
  class Dn a b where
    dn :: a -> b
  instance Dn ((a->Zero)->Zero) a where
    dn = undefined
  instance Dn a ((a->Zero)->Zero) where
    dn = flip ($)
  
  -- Commutative (CM)
  class Cm t u | t->u where
    cm :: t->u
  instance Cm (a, b) (b, a) where
    cm (a, b) = (b, a)
  instance Cm (Either a b) (Either b a) where
    cm (Left a) = Right a
    cm (Right b) = Left b
  
  -- Conditional Exchange (CE)
  class Ce a b where
    ce :: a->b
  instance Ce (a->b) (Either (a->Zero) b) where
    ce = undefined
  instance Ce (Either a b) ((a->Zero)->b) where
    ce (Left a) z = x (z a)
    ce (Right b) z = b
  
  -- DeMorgan's (DM)
  class Dm a b where
    dm :: a->b
  instance Dm (a->Zero, b->Zero) ((Either a b)->Zero) where
    dm (x, y) (Left a) = x a
    dm (x, y) (Right b) = y b
  instance Dm ((Either a b)->Zero) (a->Zero, b->Zero) where
    dm z = (x, y)
     where
      x a = z (Left a)
      y b = z (Right b)
  instance Dm (Either (a->Zero) (b->Zero)) ((a, b)->Zero) where
    dm (Left x) (a, b) = x a
    dm (Right y) (a, b) = y b
  instance Dm ((a, b) -> Zero) (Either (a->Zero) (b->Zero)) where
    -- demorgans4 z a b = Right (z (a, b))
    -- demorgans4 z b a = Left (z (a, b))
    dm = undefined
  
  -- Contraposition (CP)
  cp :: (a->b) -> (b->Zero)->a->Zero
  cp = tr
  
  -- Association (AS)
  class As a b where
    as :: a->b
  instance As (a, (b, c)) ((a, b), c) where
    as (a, (b, c)) = ((a, b), c)
  instance As ((a, b), c) (a, (b, c)) where
    as ((a, b), c) = (a, (b, c))
  instance As (Either a (Either b c)) (Either (Either a b) c) where
    as (Left a) = Left(Left a)
    as (Right (Right a)) = Right a
    as (Right (Left a)) = Left (Right a)
  instance As (Either (Either a b) c) (Either a (Either b c)) where
    as (Left (Left a)) = Left a
    as (Left (Right a)) = Right (Left a)
    as (Right a) = Right(Right a)
  
  -- Law of Excluded Middle (LEM)
  lem :: (a->b) -> ((a->Zero)->b)->b
  lem = undefined
  
  main :: IO ()
  main = putStrLn "Proof Checks"
  