Instantly share code, notes, and snippets.

# nfrisby/InductiveConstraints.hs Created Oct 11, 2012

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