"propositions as types" is cool!

Deduction.hs

module Logic.Deduction where

modusPonens :: (a -> b) -> a -> b
modusPonens = id

transitivity :: (b -> c) -> (a -> b) -> a -> c
transitivity = (.)

cons1 :: (a -> c) -> (b -> c) -> Either a b -> c
cons1 f _ (Left  x) = f x
cons1 _ g (Right y) = g y

cons2 :: (a -> c) -> (b -> d) -> Either a b -> Either c d
cons2 f _ (Left  x) = Left  (f x)
cons2 _ g (Right y) = Right (g y)

LessThan.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}

module Logic.LessThan where

import Data.Kind    (Type)
import GHC.TypeLits (type (+), Nat)

data (x :: Nat) < (y :: Nat) where
    LessBy1 :: x < (x + 1)
    LessByN :: x < y -> x < (y + 1)

class Transitive (t :: x -> x -> Type) where
    transitive :: t a b -> t b c -> t a c

instance Transitive (<) where
    transitive ab LessBy1 = LessByN ab
    transitive ab (LessByN bcm1) = LessByN (transitive ab bcm1)