Code playground for http://www.tomharding.me/2016/10/29/peano-forte/

Main.purs

module Main where

import Prelude
import Effect.Console (logShow)
import TryPureScript (render, withConsole)

-- Declare the recursive type.
data Peano = Z | S Peano

-- This allows us to print the type.
instance showPeano :: Show Peano where
  show  Z    = "Z"
  show (S x) = "(S " <> show x <> ")"
  
-- So we can use "==" with Peanos.
instance eqPeano :: Eq Peano where
  eq  Z     Z    = true
  eq (S x) (S y) = x == y
  eq  _     _    = false

-- So we can use "+" and "*".
instance semiringPeano :: Semiring Peano where
  add  Z    y = y
  add  x    Z = x
  add (S x) y = S (x + y)

  mul  Z    y = Z
  mul  x    Z = Z
  mul (S x) y = y + mul x y
  
  one = S Z

  zero = Z

-- For ease of debugging.
toInt :: Peano -> Int
toInt    Z      = 0
toInt   (S x)   = 1 + toInt x

-- The three examples from the article.
main = render <=< withConsole $ do
  logShow $ (S (S Z)) == (S (S (S Z)))
  logShow $ (S (S (S Z))) + (S (S Z))
  logShow $ toInt (S (S (S Z)))