idk haskell stuff

equality.hs

{-# LANGUAGE MonoLocalBinds #-}

module Main where

class Relation r a b

class Relation r a a => Reflexivity r a where
  reflexivity :: r a a

class Relation r a b => Symmetry r a b where
  symmetry :: r a b -> r b a

class (Relation r a b, Relation r b c) => Transitivity r a b c where
  transitivity :: r a b -> r b c -> r a c

data Equality a b where
  Refl :: Equality a a

instance Relation Equality a b

instance Reflexivity Equality a where
  reflexivity = Refl

instance Symmetry Equality a b where
  symmetry Refl = Refl

instance Transitivity Equality a b c where
  transitivity Refl Refl = Refl

instance Show (Equality a b) where
  show Refl = "refl"

data Zero

instance Show Zero where
  show _ = "Zero"

data Succ n where
  Succ :: Nat n -> Succ (Nat n)

instance (Show n) => Show (Succ n) where
  show (Succ n) = "Succ(" ++ show n ++ ")"

data Nat n where
  O :: Nat Zero
  S :: Nat n -> Nat (Succ n)

instance (Show n) => Show (Nat n) where
  show O = "O"
  show n = show n

data EqNode n m = Eqn (Nat n) (Nat m)

instance (Show n, Show m) => Show (EqNode n m) where
  show (Eqn n m) = show n ++ " = " ++ show m

eqNode :: Nat n -> Nat m -> Equality (Nat n) (Nat m) -> EqNode n m
eqNode n m proof = Eqn n m

main = do
  let three = S (S (S O))
  let four = S three

  let foo = eqNode three three Refl

  putStrLn $ show foo