Basics

Introduction

The functional programming style brings programming closer to simple and everyday mathematics: If a procedure or method has no side effects, then (ignoring efficiency) all we need to understand about it is how to map inputs to outputs - in other words, we can think of it as a concrete method that computes a mathematical function. This is one sense of "functional" in "functional programming". The direct connection between programs and simple mathematical objects supports both the formality of correctness proofs and informal reasoning about program behavior.

The other sense in which functional programming is "functional" is that it emphasizes the use of functions as first-class values - that is, values that can be passed as arguments to other functions, returned as results, included in data structures, etc. The recognition that functions can be treated in this way as data enables a range of useful commands.

Other common features of functional languages include algebraic data types and pattern matching, which make it easy to construct and manipulate data structures, and sophisticated polymorphic type systems, supporting abstraction and code reuse. Kind contains all of these features.

The first half of this chapter introduces the most basic elements of the Kind functional programming language. The second half introduces some basic techniques that can be used to prove properties about programs in Kind.