Functional Programming in Lean Show
PolymorphismJust as in most languages, types in Lean can take arguments. For instance, the type In functional programming, the term polymorphism typically refers to datatypes and definitions that take types as arguments. This is different from the object-oriented programming community, where the term typically refers to subclasses that may override some behavior of their superclass. In this book, "polymorphism" always refers to the first sense of the word. These type arguments can be used in the datatype or definition, which allows the same datatype or definition to be used with any type that results from replacing the arguments' names with some other types. The
Just as a function definition's arguments are written immediately after the name being defined, a structure's arguments are written immediately after the structure's name. It is customary to use Greek letters to name type arguments in Lean when no more specific name suggests itself. Just like
In this example, both fields are expected to be Definitions may also take types as arguments, which makes them polymorphic. The function
In other words, when the types of the arguments This can be seen by asking Lean to check the type
of
This function type includes the name of the first argument, and later arguments in the type refer back to this name. Just as the value of a function application is found by replacing the argument name with the provided argument value in the function's body, the type of a function application is found by replacing the argument's name with the provided value in the function's return type. Providing the
first argument,
Because the remaining arguments are not explicitly named, no further substitution occurs as more arguments are provided:
The fact that the type of the whole function application expression was determined by passing a type as an argument has no bearing on the ability to evaluate it.
Polymorphic functions work by taking a named type argument and having later types refer to the argument's name. However, there's nothing special about type arguments that allows them to be named. Given a datatype that represents positive or negative signs:
it is possible to write a function whose argument is a sign. If the argument is positive, the function returns a
Because types are first class and can be computed using the ordinary
rules of the Lean language, they can be computed by pattern-matching against a datatype. When Lean is checking this function, it uses the fact that the function's body pattern-matches to run the same pattern in the type, showing that Linked ListsLean's standard library includes a canonical linked list datatype, called
Behind the scenes,
The actual definition in the standard library is slightly different, because it uses features that have not yet been presented, but it is substantially similar. This definition says that The
These two definitions are completely equivalent, but Functions that consume
The definition of
Names such as To make it easier to read functions on lists, the bracket notation
Implicit ArgumentsBoth
It can be used
with
Similarly,
This
In the standard library, Lean calls this function
Just as C# and Java require type arguments to provided explicitly from time to time, Lean is not always capable of finding implicit arguments. In these cases, they can be provided using their names. For instance, a version of
More Built-In DatatypesIn addition to lists, Lean's standard library contains a number of other structures and inductive datatypes that can be used in a variety of contexts.
|