Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
simple demo of "proving" in Haskell via singleton types
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment