Structural Induction Principles for Functional Programmers
James Caldwell
Department of Computer Science
University of Wyoming
Laramie, WY 82071

User defined recursive types are a fundamental feature of modern functional programming languages
like Haskell, Clean, and the ML family of languages. Properties of programs defined by recursion
on the structure of recursive types are generally proved by structural induction on the type. It is well
known in the theorem proving community how to generate structural induction principles from data
type declarations. These methods deserve to be better know in the functional programming community. Existing functional programming textbooks gloss over this material. And yet, if functional
programmers do not know how to write down the structural induction principle for a new type - how
are they supposed to reason about it? In this paper we describe an algorithm to generate structural
induction principles from data type declarations. We also discuss how these methods are taught in
the functional programming course at the University of Wyoming. A Haskell implementation of the
algorithm is included in an appendix.

1

Introduction

A fundamental claim made for functional programs is that they are easier to reason about. This is largely
true because:
i.) the evaluation mechanism is substitution based (following ordinary mathematical practice), and
ii.) structural induction provides a straightforward mechanism for reasoning about programs defined by
recursion on algebraic data types.
A recursive type definition naturally gives rise to a structural induction principle for the type. For functions defined by recursion on the structure of a type, structural induction is the natural mechanism for
reasoning about those functions. A functional programming course is the obvious place to make the
relationship between induction and recursion explicit, and yet, we know of no standard text suitable for
undergraduates that does so. In fact, there is no other point in the undergraduate curriculum where the
concrete relationship between induction and recursion can be made as explicit as it can be in a course on
functional programming.
In this paper we introduce the functional programming course as taught at the University of Wyoming,
briefly discuss well-founded induction, the justification for structural induction, and then describe an algorithm for generating a structural induction schema from a data type declaration. We also discuss the
pedagogical approach we use at the University of Wyoming to teach this material and give a few examples.

2

Functional Programming in Wyoming

The University of Wyoming offers an ABET 1 is accredited Bachelor of Science in Computer Science.
Functional Programming (COSC 3015) is a required third year course for undergraduate students in the
1 ABET is the recognized accreditation board for college and university programs in applied science, computing, engineering, and technology programs in the U.S.

Philip K.F. Hölzenspies (Ed.): Trends on
Functional Programming In Education (TFPIE)
EPTCS 136, 2013, pp. 16–26, doi:10.4204/EPTCS.136.2

c James Caldwell
This work is licensed under the
Creative Commons Attribution License.

James Caldwell

17

Computer Science degree. The University of Wyoming has had the requirement for at least fifteen years.
Functional Programming is taught once a year and is a prerequisite for the senior level Principles of
Programming Languages (COSC 4870).
The functional programming course has been Haskell based since at least 2006; in earlier carnations
it was Scheme and LISP based. Students who take the course have already taken Discrete Structures
(COSC 2300) which, as taught in Wyoming, emphasizes mathematical proofs. Students taking functional
programming will (in theory) already know predicate logic, and will have done proofs by mathematical
induction and possibly by complete induction. There is often a gap between the time a student takes
Discrete Structure and Functional Programming and so proof methods are reviewed for the first week or
two of the functional programming course. This is done by reviewing the the mathematical definition of
a function and extensional equality for functions. This provides a nice segue into higher order functions
and students apply the definitions to reason about curry and uncurry.
Though the course does not follow any one text, over the years it has been taught with the assistance
of a variety of texts [2, 17, 8, 9, 10]. Bird’s text [2] was the first one used to teach the course when
it transitioned to Haskell and is still the book that is philosophically closest in spirit to the course as
taught today. An objective for the functional programming course is for students to learn to do proofs
in concert with program development2 Of the texts cited above, only Bird’s book carries through the
proof theme from the beginning of the book to the end. Bird introduces a number of induction principles
and, by example, expects students to be able to derive new structural induction principles from type
declarations [2, Exercise 6.2.1, pp. 191]. In the functional programming class at Wyoming we make the
relationship more explicit and expect students to be able to write down the structural induction principle
for an arbitrary Haskell type and to use it to prove some simple properties about programs defined by
recursion on the type.
Among the other texts references in the course, Thompson’s book [17, pp. 141] introduces structural
induction for finite lists and touches on induction for infinite lists but does not discuss induction principles
for other structures. Thompson’s first introduction is well after lists have first been introduced. Similarly,
Hudak’s book introduces list induction [8, pp. 131] and natural number induction [8, pp. 141], other
forms of induction are not discussed. Hutton’s text relegates reasoning about programs to the last chapter
[9, Chap.13] where he introduces both natural number induction and list induction. Lipovaca [10] never
mentions induction at all. In [6], Felleisen, Findler, Flatt and Krishnamurthi do not discuss induction but
the design recipe connecting the shape of the input data with the shape of the program is a closely related
topic. All texts mentioned have their strengths; but regarding the goal of teaching programming together
with the methods for reasoning about programs, Bird’s book does it best.
Among the texts that have not been used in the course (though some have been on the recommended
readings list) Reade’s book [15, pp.185] contains the only elementary explanation we know of regarding how structural induction principles can be derived from the declaration of a new type. Like Bird,
Cousineau and Mauny [5] present a series of examples which serve to indicate how the induction principles can be gleaned from the type declaration.
Of course more advanced programming language texts explain these topics in some detail [18, 11,
14].
The derivation of structural induction principles has been best covered in the theorem proving literature. The classic paper is Burstall’s [3]. Paulson covers it in detail [13, pp. 77-135]. The implementations
in Isabelle HOL prover [12] is excellent, as are the accounts of structural induction principles automati2 Students undoubtedly do not carry this practice with them to program developments beyond the functional programming
course, but they learn a disciplined and formal way to think about and reason about programs.

Structural Induction Principles for Functional Programmers

18

cally generated by the Coq prover [1, 4].
Perhaps the point we’d most like to make here is that, if programming and proving are to go handin-hand, understanding how to generate structural induction principles from data-type declarations is
essential knowledge. It is not hard to do nor is it hard to teach, and students who learn this are not
hamstrung when it comes to proving things about a new user defined type.

3

Background

3.1 Recursive Type Declarations
Modern functional programming languages all support some convenient form declaring new recursive
types. In Haskell [16, Section 4.2.1] user defined recursive data types are given by Algebraic Data Type
Declarations.
The declarations of new recursive types are given by specifying, in some way, constructor names and
their signatures. In dialects of ML and in Haskell, such type declarations may also be polymorphically
parameterized and appear as follows.
data T [tVars] = C0 [typeNames] | C1 [typeNames] | · · · | Cm [typeNames]
where T is the name of the new type being defined. The type name T is followed by a list [tVars] of
polymorphic type variable names, say [V1 , · · · ,Vk ]. If the type is not parameterized, then the list is empty.
The length of the list is the arity of T . On the right side of the declaration there are m constructor names
Ci , 0 ≤ i < m, m > 0. Each constructor is followed by a list [typeNames] of the names of the types of its
parameters. The list may contain previously declared types, polymorphic type variables, and completely
parameterized recursive instances of the type T . The arity of the constructor Ci is the length of the
specified parameter list. A constructor name with no parameters is a constant of type T .
Recursive type declarations of this kind can be interpreted as many-sorted Σ-algebras and the finite
instances of an inductively defined data type are denoted by the freely generated terms of the algebra
[11, 7].
If a data type T has arity 0 then it denotes a type of kind ∗. If T has arity 1 then it is a type constructor
k arrows
}|
{
z
and has kind ∗ → ∗. If T has arity k it is a type constructor of k arguments and has kind ∗ → · · · → ∗.
Note that by convention the function type constructor “→” associates to the right so ∗ → ∗ → ∗ means
∗ → (∗ → ∗). If S is a type (possibly parameterized) of the form (T T1 · · · Tk ) we write TyCon(S) to
denote the type constructor used to create S, in this case T . If S is a constant (not parameterized) then
TyCon(S) = S.
Note that the constructors provide the only means for building instances of a recursive data-type of
the kind described here. The implication is that every instance of the type arises from an application of a
constructor Ci to appropriately typed arguments.

3.2 Well-founded Induction
Well-founded induction is a powerful and flexible form of induction. It is based on an ordering given by
a well-founded relation over a type T . To show that a recursive function defined over a recursive type
T terminates, it is enough to show that there is some well-founded relation ≺ for which every recursive
call is on a smaller instance of T with respect to ≺. Excellent accounts of well-founded induction can be
found in [18, 11].

James Caldwell

19

Definition 3.1 (Well-founded Relation) A binary relation on a set A is well-founded iff there are no
infinitely descending chains · · · ≺ ai ≺ · · · ≺ a1 ≺ a0 , i.e. there is no function a : N → A such that for all
i ∈ N, a(i + 1) ≺ a(i).
Note that a well-founded relation need not be transitive [11]. Thus, for example, the relation i ≺
j = j = i + 1 is well-founded but not transitive: (1 ≺ 2) and (2 ≺ 3) but (1 6≺ 3).
def

Theorem 3.1 (Well-founded Induction) Let ≺ be a well-founded binary relation on a set A and let P
be a property of A, then
(∀x : A. (∀y : A. y ≺ x ⇒ P(y)) ⇒ P(x)) ⇒ ∀x : A. P(x)
If Γ is a context, well-founded induction can be written in the form of a derived proof rule as follows:
Γ, x : A, ∀y : A. y ≺ x ⇒ P(y) ⊢ P(x)
Γ ⊢ ∀x : A. P(x)
Pedagogically, well-founded induction is a bit more difficult to justify than structural induction which
is more concrete.

3.3 Structural Induction for N
To show that a property P holds for all natural numbers, mathematical induction often suffices. This
principle is presented as follows.
(P(0) ∧ ∀k : N.P(k) ⇒ P(k + 1)) ⇒ ∀ j : N.P( j)
As we shall see, mathematical induction is just an instance of structural induction on the natural numbers.
To see this, consider the following data type having two constructors, a constant Z : N and the successor function S : N → N.
data Nat = Z | S Nat
Replacing Z for 0 and S for (+1) yields the following:
(P(Z) ∧ ∀k : N.P(k) ⇒ P(S k)) ⇒ ∀ j : N.P( j)
This is simply the structural induction principle for N. As a proof rule, this appears as follows.
(MInd)

Γ ⊢ P(Z)

Γ, k : N, P(k) ⊢ P(S k)
Γ ⊢ ∀ j : N. P( j)

Read the rule as follows: To show that a property P of natural numbers holds for all natural numbers,
show P(Z) holds and then, assuming P( j) holds for some arbitrary j ∈ N show P(S j) holds as well. Note
that this is an instance of well-founded induction using the well-founded relation for natural numbers,
def
restated using the successor function in place of adding one: i ≺N j = j = S i.
How did the base case arise? Look at the rule for well-founded induction where the type A is specialized to N and the relation is the immediate successor relation (≺N ).
Γ, j : N, ∀k : N. k ≺N j ⇒ P(k) ⊢ P( j)
Γ ⊢ ∀ j : N. P( j)

Structural Induction Principles for Functional Programmers

20

Since j ∈ N we know j = Z or j = S i for some i ∈ N. Do a case split on j giving two subgoals:
i.) Γ, Z : N, ∀k : N. k ≺N Z ⇒ P(k) ⊢ P(Z)
ii.) Γ, i : N, ∀k : N. k ≺N (S i) ⇒ P(k) ⊢ P(S i)
For (i) note that the antecedent in the induction hypothesis (k ≺N Z) is always false and so the implication is vacuously true. Thus ∀k : N. k ≺N Z ⇒ P(k) is trivially true and adds no information to our
assumptions. Also, we already know Z : N so (i) simplifies to the following:
i.) Γ ⊢ P(Z)
For (ii.) note that by the definition of ≺N , if k ≺N S i then k = i and so S i = S k. We do not need i at
all, nor do we need the quantifier because the predecessor of S k is just k itself. Using these facts we can
simplify (ii.) to the following:
ii.) Γ, k : N, P(k) ⊢ P(S k)
This yields the ordinary rule for proof by mathematical induction (MInd).

3.4 Structural Induction in General
Structural induction is an instance of well-founded induction where the well-founded relation on pairs of
terms of type T , s ≺T t is interpreted to mean that s is an immediate subterm of t (s is a child of t). The
immediate subterm relation is not transitive, but as noted above, well-founded relations need not be. It is
easy to see that for finite instances of a recursive data type this definition yields a well-founded relation.
Also note that ≺N , as defined above, is the immediate subterm relation for the type N.
We can justify the structural induction principle for a particular type T by noting that instances of a
recursive type must have been generated by one of the constructors.
For a recursive type T , the fact that instances of T must have been generated by one of the constructors, together with simplifications based on the definition of ≺T , can be used to justify the structural
induction principles we describe how to generate below.

3.5 Generating the Induction Principle for a Recursive Type
We build the formula expressing the induction principle for a type T directly from its data type declaration. In Appendix A there is Haskell code which does this.
Consider a parameterized type declaration of the following form:
data T [V1 , · · · ,Vk ] = C0 [typeNames] | · · · | Cm [typeNames]
We build the structural induction principle in steps. The polymorphic type parameters (Vi ) may
denote any type. Recall that ∗ is the kind denoting types. Thus, the induction principle is a universally
quantified formula of the form3 .
∀V1 : ∗. · · · ∀Vk : ∗. 
Note that T has arity k and so T V1 · · · Vk is a type. A property of the type is a predicate over instances of
the type. This yields the following:
∀V1 : ∗. · · · ∀Vk : ∗.∀P : (T V1 · · · Vk ) → B. 
3 Here

 denotes a hole in the formula yet to be defined.

James Caldwell

21

The goal we intend to prove is that the property holds for all instances of T so we can fill in the
following bit:
∀V1 : ∗. · · · ∀Vk : ∗.∀P : (T V1 · · · Vk ) → B.
( ⇒ ∀t : (T V1 · · · Vk ). P(t))
Now, since every instance of the type is of the form Ci applied to the appropriate number and types
of arguments, if we can show that, no matter which constructor was used, the property holds, then we’ve
shown that it holds for all instances, no matter how the instance was constructed.
Consider a constructor declaration of the form Ci [T1 , · · · , T j ]. This constructor has the following
type:
Ci : T1 → · · · → T j → (T V1 · · · Vk )
Note that some of the Ti may be instances of the type T (the one being defined) itself. These references
to T are the recursive parts of the declaration and by the well-foundedness of the immediate subterm
relation, we may assume the property holds for these instances. The clause constructor Ci of arity j is
defined as follows:


def

F (Ci ) = ∀x1 : T1 . · · · ∀x j : T j . 

^


P(xi ) ⇒ P(Ci x1 · · · x j )

i∈{1.. j},
TyCon(Ti )= T

For each type Ti that is a recursive instance of T , we assume P holds for that instance. Note that the
constraint on inductive hypotheses is not that Ti = (T V1 · · · Vk ) but simply that T is the type constructor
for the type Ti . This allows for types where the recursive instances in the type declaration do not have
the same arguments in every call i.e. see the SwapTree example included below.
Putting it all together we get the following structural induction principle.
∀V1 :∗. · · · ∀Vk : ∗. ∀P
 : (T V1 · · · Vk ) → B.
V

i∈{1.. j} F (Ci )

⇒ ∀t : (T V1 · · · Vk ). P(t)

The algorithm described here is implemented by the Haskell code in Appendix A. It is not difficult
to generalize so that mutually recursive type declarations can be handled, but we do not present that
generalization in the undergraduate course. The function stind shown in Appendix A takes a Haskell
data type representing the abstract syntax of a Haskell data declaration and returns an instance of a
formula type encoding the structural induction principle. Within the body of stind, the locally defined
function mkConstructorClause implements the formula transformation defined above as F .

4

In the classroom

A significant motivation for teaching induction and proofs in the context of a functional programming
course is to get students thinking in a formal way about the programs they write. Students are encouraged
to think about the putative theorems related to the programs they write - theorems that should hold if their
programs are correct. These theorems are intended to serve as a kind of formally stated requirements for
the functions.
As an example, assuming [ ] is is a right identity for append and that append is associative:
∀m : [a]. m ++ [ ] = m
∀m, n, r : [a].(m ++ n) ++ r = m ++ (n ++ r)

Structural Induction Principles for Functional Programmers

22

show that the following theorem relating reverse and append holds for finite lists:
∀m, n : [a]. reverse(m ++ n) = reverse n ++ reverse m

This theorem gives a nice characterization of list reverse in terms of append and illustrates a pattern of
contravariant behavior that can be observed in other contexts. Another example of this behavior is that
the inverse of the composition of relations S and R is the composition of the inverses of R and S, i.e.
(S ◦ R)−1 = R−1 ◦ S−1 .
As an example of the complexity of the theorems students are expected to be able to master in the
context of a two hour final exam, the following theorems about list functions have appeared on various
final exams over the last few years.
∀m : [a]. m ++ [ ] = m
∀m : [a]. length m = length(reverse m)
∀n, m : [a]. length(m ++ n) = (length m) + (length n)
∀m, n : [a]. length(zip m n) = min(length m)(length n)
To avoid a cascade of errors, when students are asked to prove some property by induction in the exam
setting, they are provided with the induction principle they must use together with the definitions of
the functions involved and some auxiliary theorems. A student who fails to correctly write down an
induction principle may well know how to correctly use one.
In addition to knowing how to do proofs by induction, students in the functional programming course
are required to be able to write down the structural induction principles for user defined types. The
program, written for this paper, to generate induction principles has not been previously presented in
the course but will be used when the course is next offered in the Fall 2013 semester. As Bird [2] and
Cousineau and Mauny [5] have noted, examples suffice to show the pattern and that is the method that
has been used in the class until now. With the algorithm available, students will be able to explore more
examples on their own. Class quizzes and exams will be used to asses if students have internalized the
method or not.
Consider the following Haskell data types:
data
data
data
data
data

Nat = Z | S Nat
List a = Nil | Cons a (List a)
Tsil a = Snoc (Tsil a) a | Lin
BTree a = Leaf a | Fork (BTree a) (BTree a)
SwapTree a b = Leaf | Node a (SwapTree b a) (SwapTree b a)

The following are the structural induction principles output by the Haskell code in Appendix A for the
types just given. The Haskell show functions for types and formulas were specialized to produce the
LaTeX output.

James Caldwell

23

Nat :
∀P : Nat → B.
((P Z) ∧ ∀n1 : Nat.((P n1 ) ⇒ (P(S n1 )))) ⇒ ∀n : Nat.(P n)
List a :
∀a : ∗. ∀P : (List a) → B.
((P Nil) ∧ ∀x1 : a. ∀l2 : (List a).
((P l2 ) ⇒ (P (Cons x1 l2 ))))
⇒ ∀l : (List a). (P l)
Tsil a :
∀a : ∗. ∀P : (Tsil a) → B.
(∀x1 : a. ∀t2 : (T sil a).
((P t2 ) ⇒ (P (Snoc t2 x1 ))) ∧ (P Lin))
⇒ ∀t : (Tsil a). (P t)
BTree a :
∀a : ∗. ∀P : (BTree a) → B.
(∀x1 : a. (P (Lea f x1 ))
∧ (∀t1 : (BTree a). ∀t2 : (BTree a).
(((P t1 ) ∧ (Pt2 )) ⇒ (P (Fork t1 t2 )))))
⇒ ∀t : (BTree a). (P t)
SwapTree a b :
∀a : ∗. ∀b : ∗. ∀P : (SwapTree a b) → B.
((P Lea f )
∧ (∀x1 : a. ∀s2 : (SwapTree b a). ∀s3 : (SwapTree b a).
(((P s2 ) ∧ (P s3 )) ⇒ (P (Node x1 s2 s3 )))))
⇒ ∀s : (SwapTree a b). (P s)
Now consider some seemingly pathological examples; these data types are not recursive.
data Bool = T | F
data Maybe a = Nothing | Just a
The formulas produced by the method described above yield the following “induction” principles.
Bool :
∀P : Bool → B. ((P T ) ∧ (P F)) ⇒ ∀b : Bool. (P b)
Maybe a :
∀a : ∗. ∀P : (Maybe a) → B.
((P Nothing) ∧ ∀x1 : a. P(Just x1 )) ⇒ ∀m : (Maybe a). (P m)
The structural induction principles are generated by case analysis (on the constructors) and by including the appropriate induction hypotheses for each case. If there is no recursion in the type definition,
the induction principle reduces to case analysis. The resulting formulas are theorems whether there is
recursion or not.

Structural Induction Principles for Functional Programmers

24

Induction in a lazy language like Haskell is somewhat complicated by the fact that all types T are
inhabited by the undefined value ⊥. With regards to well-founded relations on terms of type T , for
all finite terms s, ⊥ ≺T s and ⊥ 6≺T ⊥. Case analysis on the natural numbers yields two cases, one for
numbers constructed from the constant Z and the other for numbers constructed by the successor function
S. To prove a property of lazy natural numbers an additional case is added to show that (P ⊥) holds. This
extra case arises naturally from the schema of well-founded induction in the same way the simplified
case for Z does when the case analysis splits to include the possibility of ⊥. The structural induction
principles can be extended to work on these pointed types [11, pp.310] simply by adding a clause P(⊥)
which must be shown to hold in addition to the others.
To give the reader a sense of the difficulty, the following question appeared on a recent final exam
and was worth 12 points out of a possible 100.

1.)

[12 points] Write structural induction principles for the following Haskell data-types.
data STree a = Leaf | Node a (STree a) (STree a)
data Lambda c = Var String
| Const c
| Ap (Lambda c) (Lambda c)
| Abs String (Lambda c)

Students typically do well on these questions.

5

Conclusion

Students learning functional programming are in a unique position to be able to prove properties about
the programs they write during the development process. It is often the case that putative properties
of the functions serve as specifications for the functions and can be used to verify their correctness.
Fundamental properties about recursive types can be verified in the context of a functional programming
course that are virtually impossible to do in the imperative setting. However, if they do not have the
ability define structural induction principles for newly defined types, students are left wanting in their
skills.
At the University of Wyoming we have been presenting these methods for years in the functional
programming course (COSC 3015). Students practice the methods in homework assignments and there
are often questions on the final examination requiring them to write structural induction principles for
types they have not seen before. On the most recent exam they were required to write induction principles
for a type representing lambda terms and for a tree structure with three kinds of nodes.
The methods described here have been widely implemented in the theorem proving community and
deserve to be better known in the functional programming community.

References
[1] Yves Bertot & Pierre Castéran (2004): Interactive Theorem Proving and Program Development. Coq’Art:
The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, Springer Verlag,

James Caldwell

25

doi:10.1007/978-3-662-07964-5.
[2] Richard Bird (1998): Introduction to Functional Programming using Haskell, second edition. Prentice-Hall.
[3] R. M. Burstall (1969): Proving Properties of Programs by Structural Induction. The Computer Journal 12(1),
pp. 41–48, doi:10.1093/comjnl/12.1.41.
[4] Adam Chlipala: Certified Programming with Dependent Types.
Feb. 12, 2013, availabe online
http://adam.chlipala.net/cpdt/.
[5] Guy Couineau & Michel Mauny (1995): The Functional Approach to Programming. Cambridge University
Press.
[6] Matthias Felleisen, Robert Bruce Findler, Matthew Flatt & Shriram Krishnamurthi (2001): How to design
programs: an introduction to programming and computing. MIT Press, Cambridge, MA, USA.
[7] Jean H. Gallier (1985): Logic for computer science: foundations of automatic theorem proving. Harper &
Row Publishers, Inc., New York, NY, USA.
[8] Paul Hudak (2000): The Haskell School of Expression: Learning Functional Programming theough Multimedia. Cambridge University Press.
[9] Graham Hutton (2007):
Programming in Haskell.
Cambridge University Press,
doi:10.1017/CBO9780511813672.
[10] Miran Lipovaca (2011): Learn You a Haskell for Great Good: A Beginner’s Guide. No Starch Press.
[11] John Mitchell (1996): Foundations for Programming Langauges. MIT Press.
[12] Tobias Nipkow, Lawrence C. Paulson & Markus Wenzel (2002): Isabelle/HOL — A Proof Assistant for
Higher-Order Logic. LNCS 2283, Springer.
[13] Lawrence C Paulson (1990): Logic and computation: interactive proof with Cambridge LCF. Cambridge
University Press.
[14] Benjamin Pierce (2002): Types and Programming Langauges. MIT Press.
[15] Chris Reade (1989): Elements of Functional Programming. Addison Wesley.
[16] et. al. Simon Peyton Jones (2003): The Haskell 98 Language and Libraries: The Revised Report. Journal of
Functional Programming 13(1), pp. 1–255.
[17] Simon Thompson (1999): Haskell: The Craft of Functional Programming, second edition. Addison Wesley.
[18] Glynn Winskel (1993): The Formal Semantics of Programming Langauges: An Introduction. MIT Press.

26

Structural Induction Principles for Functional Programmers

Appendix A Haskell code to generate structural induction principles from a Data declaration.
import Data.Char
data Type = Star | Simple String [Type] | Tuple [Type] | Arrow Type Type
deriving (Eq, Show)
type CName = String
type TName = String
data Data = Data TName [TName] [(CName, [Type])] deriving (Eq,Show)
data Formula = FTrue
| Pred String [Formula]
| And Formula Formula
| Implies Formula Formula
| Forall String Type Formula
deriving (Eq,Show)
conjoin = foldr1 (\f fs → And f fs)
forall = foldr (\(v,ty) more → Forall v ty more)
mkFormulaVars = map (\v → Pred v [ ])
numberedVars vars = map (\(x,i) → x ++ (show i)) (zip vars [1..])
stind (Data tname targs constructors) =
let indVarName = map toLower (take 1 tname) in
let varName = ”x” in
let newType = Simple tname (map (\t → Simple t [ ]) targs) in
let prefix body =
forall (Forall ”P” (Arrow newType (Simple ”Bool” [ ])) body)
(zip targs (repeat Star)) in
let mkConstructorClause (c, types) =
if null types then
Pred ”P” [Pred c [ ]]
else
let arity = length types in
let vars = numberedVars
(map (\(Simple name ) →
if name == tname then indVarName else varName) types) in
let varsXTypes = zip vars types in
let indVars = mkFormulaVars $
map fst (filter (\( , Simple t ) → t == tname) varsXTypes) in
let antecedents = conjoin (map (\t → Pred ”P” [t]) indVars) in
let concl = Pred ”P” [Pred c (mkFormulaVars vars)] in
let universal body = forall body varsXTypes in
case indVars of
[ ] → universal concl
→ universal (Implies antecedents concl) in
let antecedent = conjoin (map mkConstructorClause constructors) in
let concl = Forall indVarName newType (Pred ”P” [Pred indVarName [ ]]) in
prefix (Implies antecedent concl)

