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.
Could not deduce (Natural 'Z) ...
Possible fix: add an instance declaration for (Natural 'Z)
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)
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)
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