simple demo of "proving" in Haskell via singleton types

InductiveConstraints.hs

{-# LANGUAGE RankNTypes, TypeFamilies, DataKinds, TypeOperators,
  ScopedTypeVariables, PolyKinds, ConstraintKinds, GADTs,
  MultiParamTypeClasses, FlexibleInstances, UndecidableInstances,
  FlexibleContexts #-}

module InductiveConstraints where

import GHC.Prim (Constraint)



-- our evidence for "p implies q" is a function that can wring a q dictionary
-- out of a p dictionary
type p :=> q = forall a. p => (q => a) -> a

-- a proof is then just an implication with a trivial antecedent
type Proof p = () :=> p



-- we'll be proving inductive properties over naturals, so we need naturals
data Nat = Z | S Nat

-- we use singleton kinds to emulate dependent types (see Eisenberg and
-- Weirich's "Dependently Typed Programming with Singletons" at HASKELL 2012)
data Nat1 :: Nat -> * where
  Z1 :: Nat1 Z
  S1 :: Nat1 n -> Nat1 (S n)

data Predicate (predicate :: k -> Constraint) = Predicate



-- induction is the dependent elimination form for naturals: we're turning a
-- natural n into a dictionary for (c n)
type BaseCase      c = Proof (c Z)
type InductiveStep c = forall m. Nat1 m -> c m :=> c (S m)

ind_Nat :: Predicate c ->
           BaseCase c -> InductiveStep c ->
           Nat1 n -> Proof (c n)

ind_Nat _ base _ Z1 = \k -> base k

ind_Nat pc base step (S1 n1) = \k ->
  ind_Nat pc base step n1 $ -- introduces the inductive hypothesis
  step n1 k



--------------------
-- Natural-ness is hopefully an inductive property!
class Natural (n :: Nat) where nat1 :: Nat1 n

inductive_Natural :: Nat1 n -> Proof (Natural n)
inductive_Natural = ind_Nat (Predicate :: Predicate Natural)
  (\x -> x) -- base case
  (\_ x -> x) -- inductive step

{-

If you comment out the rest of this file, the above declaration causes the
following type errors. Inspecting them actually informs us what Natural
instances we need to declare.

InductiveConstraints.hs:56:10:
    Could not deduce (Natural 'Z) ...
    ...
    Possible fix: add an instance declaration for (Natural 'Z)

InductiveConstraints.hs:57:12:
    Could not deduce (Natural ('S m)) ...
    ...
    or from (Natural m)
      ...
    Possible fix: add an instance declaration for (Natural ('S m))

-}

instance Natural Z where nat1 = Z1
instance Natural m => Natural (S m) where nat1 = S1 nat1





-- use of ind_Nat is more interesting on ~ constraints, because its "instances"
-- are built-in

--------------------
-- proof that plus is commutative
type family Plus (n :: Nat) (m :: Nat) :: Nat
type instance Plus Z     m = m
type instance Plus (S n) m = S (Plus n m)

class    (Plus n m ~ Plus m n) => Plus_Comm (n :: Nat) (m :: Nat)
instance (Plus n m ~ Plus m n) => Plus_Comm  n          m

plus_Comm :: forall n. Nat1 n -> forall m. Nat1 m -> Proof (Plus_Comm n m)
plus_Comm n1 = ind_Nat (Predicate :: Predicate (Plus_Comm n))

-- again, the type errors raised with the naive base case "proof" and inductive
-- step "proof" indicate what we need to prove.

{-  (\x -> x)
InductiveConstraints.hs:74:10:
    Couldn't match type `m' with `Plus m 'Z'
      `m' is a rigid type variable bound by
          the type signature for
            plus_Comm :: Nat1 n -> Nat1 m -> Proof (Plus_Comm m n)
          at InductiveConstraints.hs:72:22
    ... -}

  -- base case
  (let plus0 :: forall n. Nat1 n -> Proof (Plus_Comm Z n)
       plus0 = ind_Nat (Predicate :: Predicate (Plus_Comm Z))
              (\x -> x)   -- base case
              (\_ x -> x) -- inductive step
   in \x -> plus0 n1 x)

{-  (\_ x -> x)
InductiveConstraints.hs:95:12:
    Could not deduce (Plus n ('S m1) ~ 'S (Plus n m1))
    ...
    or from (Plus_Comm n m1)
      ... -}

  -- inductive step
  (let lemma :: forall m. Nat1 m -> Nat1 n ->
                Plus_Comm n m :=> Plus_Comm_Lemma m n
       lemma _ = ind_Nat (Predicate :: Predicate (Plus_Comm_Lemma m))
         (\x -> x) (\_ x -> x)
   in \m1 x -> lemma m1 n1 x)

class    (Plus n (S m) ~ S (Plus n m)) => Plus_Comm_Lemma m n
instance (Plus n (S m) ~ S (Plus n m)) => Plus_Comm_Lemma m n