I solemnly swear I'm up to no good.

bpp.hs

{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE Haskell2010            #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE UndecidableInstances   #-}

module Main where

import           Prelude (IO, return, undefined)

-- Define a bi-polar Peano construction of integers in the type system...
data Z
data P n
data N n

type Zero = Z
type One = P Z
type Two = P One
type Three = P Two
type Four = P Three
type NegOne = N Z
type NegTwo = N NegOne
type NegThree = N NegTwo
type NegFour = N NegThree

zero :: Zero
zero = undefined
one :: One
one = undefined
two :: Two
two = undefined
three :: Three
three = undefined
four :: Four
four = undefined
negone :: NegOne
negone = undefined
negtwo :: NegTwo
negtwo = undefined
negthree :: NegThree
negthree = undefined
negfour :: NegFour
negfour = undefined

class Succ a b | a -> b where succ :: a -> b
instance Succ (N (N n)) (N n) where succ = undefined
instance Succ (N Z) Z where succ = undefined
instance Succ Z (P Z) where succ = undefined
instance Succ (P n) (P (P n)) where succ = undefined

class Pred a b | a -> b where pred :: a -> b
instance Pred (N n) (N (N n)) where pred = undefined
instance Pred Z (N Z) where pred = undefined
instance Pred (P Z) Z where pred = undefined
instance Pred (P (P n)) (P n) where pred = undefined

data True
data False

class Pos a b | a -> b where pos :: a -> b
instance Pos Z False where pos = undefined
instance Pos (P a) True where pos = undefined
instance Pos (N a) False where pos = undefined

class Neg a b | a -> b where neg :: a -> b
instance Neg Z False where neg = undefined
instance Neg (P a) False where neg = undefined
instance Neg (N a) True where neg = undefined

class NonZero a b | a -> where nonZero :: a -> b
instance NonZero Z False where nonZero = undefined
instance NonZero (P a) True where nonZero = undefined
instance NonZero (N a) True where nonZero = undefined

class Plus a b c | a b -> c where plus :: a -> b -> c
instance {-# OVERLAPS #-} Plus Z a a where plus = undefined
instance Plus a Z a where plus = undefined
instance (Plus a b c) => Plus (P a) (P b) (P (P c)) where plus = undefined
instance (Plus a b c) => Plus (N a) (N b) (N (N c)) where plus = undefined
instance (Plus a b c) => Plus (P a) (N b) c where plus = undefined
instance (Plus a b c) => Plus (N a) (P b) c where plus = undefined

class Negate a b | a -> b where negate :: a -> b
instance Negate Z Z where negate = undefined
instance (Negate a b) => Negate (P a) (N b) where negate = undefined
instance (Negate a b) => Negate (N a) (P b) where negate = undefined

class Subtract a b c | a b -> c where subtract :: a -> b -> c
instance (Negate b nb, Plus a nb c) => Subtract a b c where subtract = undefined

main :: IO ()
main = return ()