today in 1 + 1 = 2 (with a reduction typeclass)

onePlusOne.hs

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}

module Main where

main :: IO ()
main = putStrLn "Hello World"

data x :=: y where
  PlainRefl :: x :=: x
  FancyRefl :: (Reduce x z, Reduce y z) => x :=: y

class Reduce x y | x -> y
-- zero reduces to zero
instance Reduce Z Z
-- if y is the reduced form of x, then S y is the reduced
-- form of S x
instance Reduce x y => Reduce (S x) (S y)

-- addition rules
instance Reduce (Add x Z)  x
instance Reduce (Add (S x) y) z => Reduce (Add x (S y)) z

-- multiplication rules
instance Reduce (Mult x Z) Z
instance Reduce (Mult x (S Z)) x
instance Reduce (Mult (S x) (S y)) z => Reduce (Mult x (S (S y))) z

data Z
data Add x y
data Mult x y
data S x

-- 2 + 1 = 1 + (2 * 1)
eq :: Add (S Z) (S (S Z)) :=: S (Mult (S (S Z)) (S Z))
eq = FancyRefl