N is for Natural; zero, or more

NNat.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
module NNat where

import GHC.TypeLits

-- Nat-indexed inductive naturals
data N (n :: Nat) where
  Z :: N 0
  -- This is the important bit.
  --
  -- We have to subtract on the left instead of adding on the right so that the type
  -- family application (the - or +) does not offend the constraint solver when it
  -- checks the kinds of the various N arguments to Plus'. The invisible kind params
  -- passed to Plus' only complicate things further.
  --
  -- Even with this, I had little success with a GADT providing witnesses of equality
  -- between a non-indexed inductive N and Nat. This makes me suspect that I won’t be
  -- able to use this to operate with Nat in my public types and only use N in the
  -- internal implementations, or at least not directly. “Time will tell,” he said,
  -- ominously.
  S :: N (n - 1) -> N n

-- Addition of Nat-indexed naturals; any two arguments determine the third
-- Oleg did it first
class Plus (a :: N na) (b :: N nb) (c :: N nc) | a b -> c, a c -> b, b c -> a
instance (Plus' a b c, Plus' b a c) => Plus a b c

-- Addition of Nat-indexed naturals; the first argument and one other decide the last
class Plus' (a :: N na) (b :: N nb) (c :: N nc) | a b -> c, a c -> b
instance Plus' 'Z n n
instance Plus' m n o
      => Plus' ('S m) n ('S o)

NNat2.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
module NNat where

import GHC.TypeLits

-- Nat-indexed inductive naturals
data N (n :: Nat) where
  Z :: N 0
  -- As before, this is important for the definition of Plus'.
  S :: N (n - 1) -> N n

-- /Injective/ mapping of Nat to N.
--
-- This is where the type index of N really pays off: this type family can’t be made
-- injective without it, because the type variable is absent and the computation in
-- the subtraction is non-injective. So there’s no way for it to tell which n a non-
-- indexed 'S relates to.
type family FromNat (n :: Nat) = (n' :: N n) | n' -> n where
  FromNat 0 = 'Z
  FromNat n = 'S (FromNat (n - 1))

-- This time around, let’s use Nat as the arguments to Plus, and map them to N in the
-- instance.
class Plus (a :: Nat) (b :: Nat) (c :: Nat) | a b -> c, a c -> b, b c -> a
instance (Plus' (FromNat a) (FromNat b) (FromNat c), Plus' (FromNat b) (FromNat a) (FromNat c)) => Plus a b c

-- Addition of Nat-indexed naturals; the first argument and one other decide the last
class Plus' (a :: N na) (b :: N nb) (c :: N nc) | a b -> c, a c -> b
instance Plus' 'Z n n
instance Plus' m n o
      => Plus' ('S m) n ('S o)