Next: Why be a Star programmer?, Up: (dir) [Contents][Index]
This is the guide for the Star language.
This book gives an introduction into the form and usage of the Star programming language. However, it is not a definitive reference on the language; for which the reader is referred to See The Star Reference by F.G. McCabe.
| • Why be a Star programmer?: | ||
| • A tour of Star: | ||
| • Functional Programming: | ||
| • Collections: | ||
| • Making choices: | ||
| • Boiling the Ocean: | ||
| • Concept index: | ||
| • Function index: | ||
| • List of Syntax Rules: |
Next: A tour of Star, Previous: Top, Up: Top [Contents][Index]
This book is about the programming language called Star. Why, you may ask, do you need to learn yet another language? We hope to answer that question and more in the course of this book. We also aim to show you how to program effectively in Star to solve real world problems.
| • Programming has changed: | ||
| • Is Star for you?: | ||
| • Design goals for Star: | ||
| • About this book: |
Next: Is Star for you?, Up: Why be a Star programmer? [Contents][Index]
Many of the world’s most popular languages are quite old: C/C++ date back to the 1970’s and 1980’s; Java dates back to 1995. Although it sometimes does not seem like it; quite a lot has changed since those days.
| • Programs are huge: | ||
| • Planning for change: | ||
| • Programming safely and effectively: | ||
| • Real-time is normal time.: | ||
| • This train is leaving the station: | ||
| • Technology: |
Next: Planning for change, Up: Programming has changed [Contents][Index]
If your program is 100 lines long, it does not actually matter what programming language you use to write it in – unless you are learning programming for the first time.
However, in practice, many software systems are huge. It is normal to develop and to encounter programs measured in 100 Klocs (thousands of lines of code) and it is not uncommon to encounter software systems measured in the millions of lines of code.
NOTE: To put these numbers into perspective, 500KLocs is comparable to the expected output of a programmer over their entire career. So, these systems necessarily involve many people over many years: a team of 10 programmers would take 10 years to write 1M lines of code.1
Software development at this scale does not share much with developing small systems. Large scale software is invariably a team effort, spread over multiple years. It often involves large numbers of components and multiple sub-systems interacting with each other. Overall, this is a scenario of staggering heterogeneity and complexity.
If there is one theme that is common in large code bases is that tooling is critical: powerful IDEs can make a difference in productivity measured in factors of 2-5. However, it is our opinion that language tooling starts with a sound programming language design: the sounder the foundations, the taller the structure that can be built on it.
Next: Programming safely and effectively, Previous: Programs are huge, Up: Programming has changed [Contents][Index]
Furthermore, change is the dominant fact of life for large systems. Software systems evolve, grow, are repurposed to meet new objectives, and are re-implemented to take advantage of new technologies.
Managing change in code is often left to Source Code Control Systems; but these systems only address part of the problem. For example, code re-use is also a requirement and a challenge for large systems. In fact, one could imagine a three Rs2 for software engineering: Reuse, Repurpose, and Refactor.
When the code base is over 500 Kloc, the theoretical probability of being able to re-use existing code is high, the actual probability of re-use may be very low – software engineers may simply not be able to find the needle in the code haystack, or, typically, the cost of re-using code may outweigh the cost of developing from scratch.
The need to repurpose reflects the fact that requirements change and that software written for one purpose may be used for something different. Finally, even if the requirements dont change, the context almost certainly will: increasing workload can lead to a need to refactor existing code to enable it to meet changing needs.
There is another kind of change that we need to consider: the evolution of our programming languages and other tools. A successful programming language is part of an ecosystem. That ecosystem consists of the language itself, together with compilers and related tools. It also contains libraries, frameworks and packages. In many cases the libraries that are associated with a language are far more important than the language compiler (e.g., Java’s package ecosystem is enormous).
A well designed language is capable of supporting a large variety of libraries without running into limitations. Furthermore, a well designed language is structured in a way that supports its own evolution – new requirements can lead to new features being added to the language.
Managing this evolution may be the hardest aspect of designing programming languages!
Next: Real-time is normal time., Previous: Planning for change, Up: Programming has changed [Contents][Index]
At the same time, safety and security are also critical: no-one likes to have their private information exposed to the bad guys. Most main-stream programming languages were designed in an era when safety was not uppermost in programmers’ minds – usually it was performance. Some seemingly trivial design choices – such as C’s conventions for laying out strings in memory – turn out to have potentially devastating security implications.
In addition, systems that are built assuming a shielded execution environment, behind closed doors as it were, are often actually expected to perform in the full glare of the Internet. Hardening programs so that they stand up to that glare can often dramatically add to the cost of development – both in time and in money.
Next: This train is leaving the station, Previous: Programming safely and effectively, Up: Programming has changed [Contents][Index]
Many kinds of business are becoming more and more ‘real-time’: a small – over the order of milliseconds – slowdown in loading a web page can mean the loss of 5% or more of revenue for an e-commerce site; an unrented car, like an unrented hotel room, represents a permanent loss of business and a competitive disadvantage.
For the modern programmer, this means that applications must be engineered from the start to be responsive and multitasking – aspects that challenge even the most professional of programmers.
Next: Technology, Previous: Real-time is normal time., Up: Programming has changed [Contents][Index]
Perhaps most importantly, we need to be able to do these things now – time to market is a critical factor in many if not most modern applications. Its no good developing the world’s best widget if you run out of ‘runway’ trying to build it.
A major bottleneck is the relative poor productivity of most modern programming languages. It is simply too hard to produce correct robust code in languages like C/C++, Python etc.
Productivity is an issue for individual programmers but is especially salient for programmer teams.
Every successful software project involves a team.
The requirements for team-based development tend to put certain aspects of programming language design into sharp focus. For example, strong types and clear interfaces may be excellent aids for individual programmers but they are absolutely paramount for team development.
More generally, in a competitive environment, the only way to reliably out-perform the competition in reaching the market is to use radically more productive technology.
Previous: This train is leaving the station, Up: Programming has changed [Contents][Index]
The technology platform that programs are written for is also changing. Just a few decades ago most computers were single-core; nowadays most computers are multi-core and are capable of significant parallelism.
Especially spectacular is the parallelism available in modern GPUs; where a high end graphics processor may have thousands of cores capable of processing instructions in parallel. We expect that the days of personal computers with thousands of cores is not too far in the future.
Programming parallel machines with conventional languages is an exercise in frustration. This is because programming models that worked in single core computers do not scale well to highly parallel machines. One of the primary reasons for this is that state – as represented by the changing values of variables – is implicit in procedural and object oriented languages. The implicitness of state is important because it makes many programs easier to express. On the other hand, that implicitness becomes a liability in multi-threaded and parallel situations where state is no longer so well behaved.
However, Star has adopted some of the recent innovations in that make dealing with multi-tasking and parallel execution easier. These innovations layer on top of basic features such as threading and provide simpler models of execution than ‘conventional’ threaded models. Star’s computation expressions combine the best of fork-join queues and map-reduce frameworks whilst enabling a more normal style of programming.
Next: Design goals for Star, Previous: Programming has changed, Up: Why be a Star programmer? [Contents][Index]
Choosing a programming language – when you actually have a choice – is highly personal. Here are some reasons to think about Star.
| • If you are already a Java (or C#): | ||
| • If you are already a C++ programmer: | ||
| • If you are already a functional programmer: |
Next: If you are already a C++ programmer, Up: Is Star for you? [Contents][Index]
Most OO languages are embracing some of the simpler features of functional languages. Even modern Java with its lambda expressions and stream features represents a nod to the power of functional programming. However, at the same time, there is a substantial gap in the capabilities of most OO languages compared to modern functional programming languages.
Fundamentally, OO languages revolve around nouns rather than verbs. Verbs (methods) are relegated to being inside the scope of some noun (object): they are not first class. In functional programming languages, like Star, there is more of an balance between nouns and verbs.
It is possible to have functions that are about data; it is also quite straightforward in functional programming languages to have data structures with functions embedded in them. In fact, a simple definition of a module is a record that contains functions in it.
While OO languages like Java provide excellent data abstraction tools, the same cannot be said for control abstractions. The result is that OO languages are ‘stuck in the 1970s’ when it comes to control abstractions. However, concepts such as map/reduce, computation expressions, and continuations bring a rich suite of new control possibilities that solve important problems in modern programming.
Similarly, the type systems of languages like Java (or C# or C/C++) make are not as expressive or sensitive as modern type systems in functional languages can be. Professional programmers will recognize a typical symptom of insufficiently expressive types: lots of casting and dynamic meta-programming. But, while powerful, these techniques amount to giving up on types and their important advantages. Furthermore, contrary to many programmers’ expectations, a modern type system is quite capable of dealing statically with scenarios that require dynamic programming in languages like Java.
Next: If you are already a functional programmer, Previous: If you are already a Java (or C#), Up: Is Star for you? [Contents][Index]
Moving to a language like Star is a radically different programming experience for the C++ programmer. However, most of the differences are not because Star is a functional programming language. Rather, it is because Star does not abide by two of C++’s core principles: zero-cost abstractions and compatibility with C.
While Star’s compiler does not willfully make programs execute more slowly, strict CPU performance is not the primary driver for design features. This shows up in a desire to avoid the so-called premature optimization problem: of optimizing the wrong feature.
In the case of Star vs C++, the most salient of these is likely to be the different ways that generic programs are compiled: C++ compiles generic programs by constructing special case implementations for all used versions of the generic program; whereas Star constructs a single – type agnostic – implementation of generic functions.
This affects many aspects of one’s day-to-day usage of the language and its tooling. One of which is that, for a compiler that has been in daily use for over 40 years, C++ compilers are still remarkably slow. C++ binaries can often be very large – typically outclassed in performance by the Java compiler.
The compatibility with C requirement has meant that C++ has to support many programming paradigms (such as pointer arithmetic) that most modern programming languages – Star included – eschew.
Pointer arithmetic is known to put applications at risk of severe security problems; and there are many modern safer alternatives (which C++ does also support).
Beyond these, you will find Star to be a rich and expressive language; especilly if your focus is on applications rather than systems programming.
Previous: If you are already a C++ programmer, Up: Is Star for you? [Contents][Index]
You have many choices for functional programming languages that are excellent. The author considers two languages that are principal sources of inspiration for many of the functional features of Star: Haskell and Standard ML (SML) – both of which are excellent; but not perfect.
For the functional programmer, the principal benefits of Star are readability, modernity and predictability.
One of the major drivers of the design of Haskell and (to a lesser extent) SML is conciseness. However, conciseness is not the same as readability. In modern software development environments there are many stakeholders beyond the developer. Having a language that is easy to follow by non-technical readers is a major benefit in mixed skill teams.
Like Haskell, Star has a powerful type system. Star’s type system has many features in common with Haskell’s type system – features that typically go beyond the capabilities of many OO languages. In particular, Star’s contract system is reminiscent of Haskell’s type classes; and Star’s existential and higher-kinded types give considerable expressive power to the programmer.
Star does not follow all of Haskell’s type features; and some type concepts are rephrased into terminology that is more familiar to main-stream (sic) programmers.
Like SML, Star has a powerful module system. However, unlike SML’s functors, Star modules are first class values. This means that there is no artificial separation between ‘ordinary’ programs and ‘functor’ programs.
The result is a balanced set of type features that provides capabilities that scale well from small programs to large systems.
Star’s evaluation is, like that of SML but unlike Haskell, strict. We believe that that makes it significantly easier to reason about the actual behavior and performance of programs. However, Star has a rich set of features that support productive concurrent and parallel programming – based on a combination of system threads and the features of Concurrent ML.
Like SML, Star is not a strictly ‘pure’ language. This was neither an accident nor an afterthought. Computer systems are built to fulfill purposeful activity (although there may be many times when the actual purpose is hard to discern). For example, if I deposit a check into my bank account, I require that the bank’s state is updated to reflect my new balance: the world has changed as a result of my action.
However, the converse does not follow: just because the world is stateful does not mean that all our programs should be needlessly stateful. Much, if not most, of a given application program can and should be crafted in a mathematical style – the merits of functional programming are very great.
Overall, the primary rationale in the design of Star is to empower the programmer in making obviously correct programs.
Next: About this book, Previous: Is Star for you?, Up: Why be a Star programmer? [Contents][Index]
Star is a multi-paradigm high-level symbolic language. It is designed to be scalable, readable, accurate, high performing and extensible.
Paradoxically, scalability in a programming language is always about large and small chunks of code. Scalability in Star is fostered by a range of elements that facilitate composition, change and re-use:
A meta-language based on logical annotations makes it possible to build meaningfully connected documentation and facilitates processes such as code re-use, issue tracking, and code lifetime management.
The syntax of Star is oriented towards readability rather than strict conciseness. The reason for this is that the programmer is only one of the stake holders in a given program. A readable program is one that is more easily trusted by non-programmers.
Experience also suggests that readability enhances programmer productivity also: much of team-based development involves comprehending and modifying other programmers’ code.
Star is a strongly, statically typed language. The purpose of a strong type system is to facilitate the communication of intent of the programmer. The purpose of static typing is to ensure that the compiler can rapidly ‘fail’ incorrect programs without requiring the program to be run. Furthermore, static type checking minimizes any run-time penalty for imposing type constraints.
Although Star is strongly typed, it uses type inference to eliminate much of the clutter that some type systems impose on the programmer – which itself is a productivity sink of course.
Generally, the stronger the type system, the more the language system can detect errors before programs are run. In addition, the more expressive the type system is, the less the temptation to try to subvert or bypass the type system.
However, even though it is technically feasible to completely eliminate type declarations of functions; doing so is in conflict with some of the other goals behind Star. For example, type declarations act as a form of documentation; and when there is a type error in your program, having no explicit type declarations can make tracking the culprit of the error very difficult. So all top-level variable definitions (typically functions) are required in Star to have explicit type annotations.3
Star has a range of features that make exploiting parallelism easier to manage. For example, it has support for computation expressions and actors. Partitioning an application into different agents allows programming to follow a more human approach. Computation expressions allow the programmer to manipulate computations as easily as they do data values; that in turns greatly eases the development of parallel and concurrent applications.
There is no one technology that can solve all problems. This is as true for programming as for other domains. Star supports a range of programming paradigms that allows the developer to ‘use the best tool for the job’. However, we go beyond this ‘swiss army knife’ stance and make it straightforward to extend the language.
Virtually every non-trivial program can be factored into a combination of general purpose mechanism and specific policy for applying the mechanism. Star has powerful self-extension features that allow programmers to design their own policy structures (a.k.a. domain specific languages).
Many of Star’s own features – such as its query notation and its actor notation – are built using these extension mechanisms.
Previous: Design goals for Star, Up: Why be a Star programmer? [Contents][Index]
This book acts as an introduction to the language and to its use. The basic features of the language are introduced; however, this is not a reference manual: it is not intended to be a complete description of the language.
That can be found in the Star Language Definition.
Introducing a programming language like Star can be a challenge in presentation. This is because there is a significant amount of mutual support between elements of the language.
Our strategy is to take a layered approach – we start with simple examples, occasionally skipping over certain aspects of the language without explanation. Later chapters focus on deeper, more complex topics.
For the most part, examples in the text of the book are executable. You are encouraged to try to get them running on your own system.
| • Getting hold of Star: | ||
| • Typographical conventions: | ||
| • Acknowledgements: |
Next: Typographical conventions, Up: About this book [Contents][Index]
The Star compiler and run-time is being developed as an open source project on GitHub. You can access the source by cloning or downloading the repository at
github.com/frankmccabe/star
Next: Acknowledgements, Previous: Getting hold of Star, Up: About this book [Contents][Index]
Any text on a programming language often has a significant number of examples of programs and program fragments. We show these using a typewriter-like font, often broken out in a display form:
P:integer; …
We use the … ellipsis to explicitly indicate a fragment of a program that may not be syntactically correct as it stands.
As we noted above, Star is a rich language with many features. As a result, some parts of the text may require more careful reading, or represent comments about potential implications of the main text. These notes are highlighted the way this note is.
Previous: Typographical conventions, Up: About this book [Contents][Index]
No-one is an island, and no project of this scale is one person’s work. I have had the great fortune to be able to develop Star in the context of real world applications solving hard problems. Individuals have also played a large role; and it can be hard to ensure that all are properly acknowledged: please forgive any omissions.
Of particular significance, I would like to thank Michael Sperber for our many discussions on the finer topics of language design; and for his not insignificant contributions to the implementation itself.
I would also like to thank my old colleagues at Starview inc., in particular Steve Baunach and Bob Riemenschneider who were the world’s first Star programmers! In addition, I would like to thank Michael Sperber, David Frese and Andreas Bernauer who helped with crucial parts of the implementation of the concurrency features. I would also like to thank Keith Clark, Kevin Cory, Prasenjit Dey, Chris Gray, Mack Mackenzie, and Kevin Twidle for their help and advice. I would like to acknowledge the support of Thomas Sulzbacher who originated the project and Jerry Meerkatz for keeping the faith.
Last, but definitely not least, I would like to acknowledge the love and support of my family; without whom none of this makes sense.
Next: Functional Programming, Previous: Why be a Star programmer?, Up: Top [Contents][Index]
Our first task is to introduce you to the Star language. It is difficult to find the right order in which to present a programming language like Star; this is because many of the features are highly inter-related. For example, types depend on values which depend on functions which depend on types!
Instead, our approach in this book is to take a series of horizontal slices through the whole language; going progressively deeper as you become more comfortable with the language. Each layer represents a reasonably workable subset of the complete language.
Since a layered approach means that any given description may be incomplete or slightly inaccurate, there is a temptation to use footnote annotations which declare ’… but there is also4 …’.
| • A first Star program: | ||
| • Texture: | ||
| • Types more types and even more types: | ||
| • A tale of three loops: | ||
| • A functional loop: | ||
| • Contracts and constrained types: | ||
| • There is more: |
Next: Texture, Up: A tour of Star [Contents][Index]
It is traditional to introduce a new programming language with something like the hello world example. Which we will do in a moment. However, the factorial function often makes a better first example for functional programming languages:
sample.factorial{ import star. -- Access standard language features public fact : (integer)=>integer. fact(0) => 1. -- base case fact(N) where N>0 => N*fact(N-1). }
This is not an executable program per se.; however, it does represent a more typical source code unit – most programs are built from many smaller modules which come together to make the application. This program is small, but already introduces many of the key elements of the Star language.
In this module, we see the name of the module –
sample.factorial
– an import statement and a function
definition – of the fact
function.
Source code can be in any form of textual container. There is, for
example, no specific requirement that this sample.factorial
package be in a file called factorial.star
; although that may
be good advice. Instead, the Star system relies on a catalog
based system that maps package names to text entities. The catalog
system also serves as an anchor point in the version management of
Star programs. We will cover this, and the related repository
system for generated artifacts, in Chapter 4.
Next: Types more types and even more types, Previous: A first Star program, Up: A tour of Star [Contents][Index]
All programming languages can be said to have a particular style or texture. This is often so strong that it is often possible to identify a programming language from a single line of source code. In the case of Star, this line might be:
public fact : (integer)=>integer.
which is a type annotation statement declaring the type of the
function fact
.
The public
annotation means that the function is exported by
this module and will be available in other modules where the
sample.factorial
module is imported.
| • Lexical style: | ||
| • Types: | ||
| • Rules: | ||
| • Patterns: | ||
| • Packages: | ||
| • Worksheets: | ||
| • String interpolation: |
Starâs lexical syntax uses a combination of special operators and keywords.
It can be difficult for language designers to decide when to use a keyword and when to use a special operator. In the case of Star we use special operators for common elements and keywords when either a graphical operator would be obscure and/or is not common.
For example, in the factorial module, we use braces for grouping; but
we also use the import
and the where
keywords. The
rationale here is that programmers have become used to seeing braces
for grouping statements;5
whereas the import and where elements are somewhat rarer.
Notice that every statement is terminated with a period. This is one of those places where a little redundancy can help when building large programs: the statement terminator is not technically necessary; but it helps to reduce the scope of error messages.6
NOTE: The precise rule is slightly more nuanced: a period is required to terminate a statement; unless the last character of the statement is a closing brace – or unless the statement is itself the last statement in a brace sequence.7
Another aspect of Starâs texture that may not be visible at this stage is the reliance on an underlying meta-grammar – specifically on an operator precedence grammar. OPGs are likely already familiar to you: it is the almost universally used grammar that underpins arithmetic expressions. We take the OPG and stretch its use to include the whole language. The relevance of this will be apparrent when we look at extending Star with new language features.
Next: Rules, Previous: Lexical style, Up: Texture [Contents][Index]
Star is a strongly, statically typed language. This means that all variables and expressions have a single type; and that all type constraints are enforceable at compile-time. This is a fairly strong (sic) statement but it is a key aspect of Starâs design – we need everything to be well typed and we also want to guarantee completeness of the type system.
The type annotation statement:
fact : (integer)=>integer.
is a statement that declares that the type of fact
is a
function of one integer argument and which returns an integer result.
Star encourages, but does not require, most programs to have explicit type annotations. The precise rule is a little subtle: variables whose type are not quantified may have their type automatically inferred. For top-level functions, that annotation is often contiguous in the text; but in other cases that may not be the case.
Other variables – like the variable N
which is part of the
second recursive equation – do not need type annotations. This is
possible because underlying the type system is a powerful type
inference system that can actually infer all types.
The result is that a lot of the ‘clutter’ that can pervade a strongly typed language is just not necessary; but the use of explicit type annotations for top-level definitions provides useful structure and documentation.
Note that the requirement is that quantified definitions have explicit type annotations. We donât distinguish functions in any way here. In particular, functions which are not generic – for example lambda functions – do not need type annotations.
In Star, most programs are defined using rules. In this
case, fact
is defined using equations. The equations
that make up a function definition (or any program definition for that
matter) are statements that are written in order.
Rule-based programs support a case driven approach to programming: a program is defined in terms of the different cases or situations that apply. Using rules to cover different cases allows the programmer to focus on each case in relative isolation.
In addition, as we shall see later on, the partitioning of programs into cases like this is very helpful in supporting large-scale issues such as code annotations, versioning and life-cycle management.
Star has various kinds of rules, including function definitions, grammar definitions, variable definitions and type definitions.
Patterns are ubiquitous in Star: they form the basis of many rules: including, most importantly, to define equations. In fact, all variables are introduced by means of patterns.
A pattern can be viewed as a combination of a test — does a value match a particular pattern — and as a way ( the way in Star) of binding a variable to a value.
An equationâs pattern defines when the equation is applicable. The
first equation for fact
above:
fact(0) => 1.
has a literal pattern on the left hand side of the =>
operator. This equation only applies when fact
is called with
zero as its argument.
The pattern in the second equation:
fact(N) where N>0 => N*fact(N-1).
has a guard on it — after the where
keyword. Guards are
additional conditions that constrain patterns. In this case, the
equation only applies if the argument is greater than zero.
Any pattern may be qualified with a guard; we could have written the guard inside the argument pattern:
fact(N where N>0) => N*fact(N-1).
We did not because having the guard outside the arguments is neater.
NOTE: The fact functionâs equations are not fully covering: there are no cases for fact for negative numbers. This means that the function is partial; and if called with a negative number will result in a run-time exception.
Next: Worksheets, Previous: Patterns, Up: Texture [Contents][Index]
The normal compilation unit is a package. The sample.factorial package contains just the function fact, but packages can contain functions, type definitions, import statements and many other elements that we will encounter.
Package names and references to packages do not refer to file names; package names are symbolic – in general a package name consists of a sequence of identifiers separated by periods.
The catalog and repository system explored in Chapter 7 that supports the language ensures a proper connection between files and packages.
Next: String interpolation, Previous: Packages, Up: Texture [Contents][Index]
The other main kind of compilation unit is the worksheet. Worksheets are a modern replacement for the REPL8 that you see in many functional programming languages.
We say a modern replacement for REPLs because worksheets fit much better in the typical environment of an IDE.
A worksheet can be used to implement the infamous hello world example in just a few lines:
worksheet{ show "hello world". }
We can also use a worksheet to display the results of using and testing our fact function:
worksheet{ import sample.factorial. show "fact(10) is \(fact(10))". assert fact(5) == 120. }
Worksheets are like a combination of a module and the transcript of a session. In an IDE, the ideal mode of displaying a worksheet is via an interactive editor that responds to edit changes by recomputing the transcript and displaying the results in-line.
The key features of a worksheet that we will use are the ability to import packages, define elements, show the results of computations and define assertions.
Previous: Worksheets, Up: Texture [Contents][Index]
The expression
"fact(10) is \(fact(10))"
is an interpolated string expression. It means the string
"fact(10) is \(fact(10))"
with the substring (fact(10)
replaced by the value of the expression embedded within. Interpolated
string expressions are a convenient way of constructing string values;
and, via the use of contracts, are also type safe.
Next: A tale of three loops, Previous: Texture, Up: A tour of Star [Contents][Index]
In many ways, the defining characteristic of a programming language is the approach to types. As we shall see, Starâs type system is quite extensive and powerful; however, simple types are quite straightforward.
The most basic question to ask about types is
What is a type?
There is some surprising variability to the answer to this question; for example, in many OO languages, types are conflated with classes. Star types are terms – i.e., names – that denote different kinds of values.
Type: A type is a term that denotes a collection of values.9
Starâs type system can be broken down into a number of dimensions:
Star distinguishes two basic styles of type: so-called structural or transparent types and nominative or opaque types. A structural type term echoes the values it models, whereas a nominative type typically does not.
For example, the standard type integer
is nominative — its
name gives no hint as to the representation, structure or kinds of
values that are modeled by integer.10 However, a nominative type often indicates some
actual entity being modeled – in this case integer values. Two
nominative types which have different names always denote distinct
values, whereas two structural types that look the same are actually
identical.
| • Nominative types: | ||
| • Reference Type: | ||
| • Structural types: | ||
| • Optional values: | ||
| • The flavors of equality: |
Next: Reference Type, Up: Types more types and even more types [Contents][Index]
A nominative type is normally defined using an algebraic type definition. This both introduces a type and defines all the legal values that belong to the type. For example, we might introduce a Person type with the type definition:
Person ::= noOne | someOne{ name : string. dob : date. }
This statement tells us that there are two kinds of Person
: a
someOne
who has a name
and date of birth (dob
)
associated with them; and a distinguished individual we identify as
noOne
. The no-one individual does not have a name or
date of birth.
Notice how the type annotation statement we saw for declaring the type of
fact
is also used for defining the types of fields in thesomeOne
record.
We can make a Person value with a labeled record expression:
S = someOne{ name = "fred". dob = today() }
The equality symbol is used to introduce a new single-assignment
variable. In this case the variable S
is defined to be a
someOne
record.
Recall that names do not always require an explicit type
annotation. In this case we can infer that S
is a Person
(because someOne
marks it). Furthermore, we do not need to
explicitly give types to the name
and dob
fields because
their type is constrained by the type declaration for Person
.
Next: Structural types, Previous: Nominative types, Up: Types more types and even more types [Contents][Index]
An important detail about the someOne
record defined above is
that the fields within it are not re-assignable. If we want to make a
variable reassignable, or if we want to make a field of a record
reassignable, we use a special ref
type to denote that. For
example, the type definition
employee ::= employee{ dept : ref string. name : string }
allows the dept
field within the employee record to be
modifiable – although the employee’s name is still fixed.
Only fields that have a ref
type are modifiable in
records. This is even true when a record is assigned to a reassignable
variable.
A reassignable variable is declared using the :=
operator:
N := employee{ dept := "your department". name = "Anon. Y. Mouse" }
Since the variable N
is declared as being reassignable, we can
give it a new value:
N := employee{ dept := "another". name = "some one" }
We can also modify the dept
field of N
:
N.dept := "new department".
However, we cannot modify the name
field – because it is not
re-assignable within the Person
type.
Notice that the re-assignability of variables and fields does not
inherit: each field or variable is separate. So, for example, if we
declared a single-assignment variable D
to be an employee:
D = employee{ dept := "his department". name = "Your Name Here" }
then, even though D
itself cannot be re-assigned to, the
dept
field of D
can be altered:
D.dept := "my department"
Next: Optional values, Previous: Reference Type, Up: Types more types and even more types [Contents][Index]
A structural type is, informally, a type that looks like a value. For example, the type
(integer,string,employee)
is a tuple type – it denotes the type of a triple of values,
consisting of an integer
, a string
and an
employee
in this case. Values of this tuple type are also
tuples; for example:
(3,"fred",employee{name="peter". dept:="sales"})
Star has several forms of structural type, the tuple type is one of them; others include record types and function types.
We shall see more of these as we introduce the rest of the language. However, it is worth pausing to ask the question Why?
Briefly, nominative types help the programmer focus on what a value denotes; whereas structural types tend to expose what a value can do.
For example, the employee
type clearly points to what an
employee value is intended to denote (an employee!), but does not help
if we want to know what an employee can do. On the other hand, the
function type in the annotation:
f : (integer)=>string
clearly indicates what one can use f
for, but it does not
indicate anything about why you would want to (except, perhaps, to
convert an integer
to a string
).
In summary, use nominative types when you are modeling real world entities and structural types when the focus is on operations and structure more than on what the intention is. In practice, of course, you will use both in some combination.
Next: The flavors of equality, Previous: Structural types, Up: Types more types and even more types [Contents][Index]
Notice that we identified a special case of noOne
in our
Person
type. One reason for including this in a type is to be
able to cope with non-existent people. However, this approach is not
always the most effective one when modeling situations where a
variable or field may not have a value.
Explicit null values, as found in Java and similar languages, cause a great number of problems: for example, null must have a special universal type; there are many scenarios where it is not possible for a variable to be null but the compiler must discover those for itself; and there is often a consequent tendency in defensive programming to test for null.
Star has no direct equivalent of a global null value. However, the
standard option
type allows the equivalent of selective
nullability. Any variable that might not have a proper value can be
marked with the option type rather than the underlying type. And you
can use none
in those cases to indicate the equivalent of no
value.
So, for example, suppose that a Person
might have a
spouse
— who is also a Person
— but is not
guaranteed to have one. Such a type can be described using:
Person ::= someOne{ name : string. dob : date. spouse : ref option[Person]. }
Here we have done two things: we have eliminated the noOne
case
for Person
and we have marked the spouse
as being both
read-write and option
al.
Someone with no spouse would be written:
freddy = someOne{ name = "Freddy". dob = today(). spouse := none }
whereas someone who has a spouse would be written:
someOne{ name = "Lisa". dob = lastYear. spouse := some(johnny) }
Of course, we can record freddy
âs marriage to lisa
using
an assignment:
freddy.spouse := some(lisa) lisa.spouse := some(freddy)
although such circular structures should be avoided where possible.
Previous: Optional values, Up: Types more types and even more types [Contents][Index]
Equality in programming languages is typically a very subtle topic. The issues can range from the nature of floating point numbers, the difference between integers and long values and the multiple potential concepts of equality for objects.
Equality in Star is always between values of the same type and it is always semantic. So, for example, an equality condition such as:
3==3.0
is not considered type safe — because 3
is an integer
literal and 3.0
is a float
literal. If you need to
compare an integer and a floating point number for equality you will
need to first of all decide in which type the comparison will be made
(integer or floating point equality) and then coerce the other
value into that type:
3 :: float == 3.0
is valid11 excepting, of course, that exact comparison between floating point numbers is not stable.
This is an important issue because not all integer values can be represented in a float value and vice-versa. So, comparing an integer and a floating point value raises the possibility of spurious accuracy as a result of losing information. The intended effect of the coercion is to make explicit the nature of equality being relied on.
The second principle is that equality is semantic. What that means is
that the ==
symbol is the name of a boolean-valued
function. The precise type of ==
is quite interesting, we
shall, however, leave it to later when we have covered some of the
core type features around contracts.
In effect, equality is not considered to be privileged; and it is definable by the programmer — albeit with some important useful default implementations.
Next: A functional loop, Previous: Types more types and even more types, Up: A tour of Star [Contents][Index]
Imagine that your task is to add up a list of numbers. Sounds simple enough: in most procedural or OO languages (such as Java) one would write a fragment of code that looks like:
int total = 0; for(Integer ix:L) total += ix;
However, this code is also full of pitfalls. For one thing we have a lot of extra detail in this code that represents additional commitments beyond those we might be comfortable with:
We can also write an equivalent loop in Star:
total = valof do{ tot := 0; for ix in L do tot := tot+ix; return tot }
The valof/return combination is a neat way of segueing from the ‘world of expressions’ into the ‘world of actions’.
This program is essentially equivalent to the Java loop; although there are some subtleties about the nature of valof/valis that go beyond Java. As a result, it has similar architectural issues.
While one loop is not going to hurt anyone; real code in languages like Java typically has many such loops. Especially when nesting loops to any depth, such code quickly becomes impossible to follow.
Next: Contracts and constrained types, Previous: A tale of three loops, Up: A tour of Star [Contents][Index]
A more idiomatic way of expressing a computation like the totalizer is to use a function. For example, we can write:
let{ total:(cons[integer])=>integer. total(nil) => 0. total(cons(E,L)) => total(L)+E } in total(L)
while short, this code too has some of the same drawbacks as the for iteration.
The type expression cons[integer]
refers to the standard type
of ‘cons lists’. Similarly, nil
refers to the empty list and
cons(E,L)
refers to the list obtained by prepending E
to
the list L
. We will explore this in more detail in
see Functional Programming.
Even if it is more declarative, there is still a lot of extra detail
and architectural commitments here — like the commitment to
cons
lists and the commitment to integers. These result in a
function that is needlessly restricted.
Like other functional languages, Star has a range of higher-order
operators that may come to the rescue. For example, we can avoid the
explicit recursion altogether by using leftFold
:
leftFold((+),0,L)
where leftFold
means
apply a left associative accumulating function to the elements of the data, assuming that the applied operator is left associative.
This expression is clearly both more concise and higher-level than either the explicit loop or the explicit recursion; and it begins to illustrate the productivity gains that are potentially available to the functional programmer.
Using leftFold
means that we can often abstract away the
machinery of loops and recursion completely — instead we can solve
the problem at a more holistic level. This is one of the hallmarks of
functional programming – it is possible to eliminate many instances
of explicit loops and recursions.
| • A totalizer query: | ||
| • The homunculus in the machine: |
Next: The homunculus in the machine, Up: A functional loop [Contents][Index]
While concise, expressions involving much use of leftFold
(and
the analogous rightFold
) can be difficult to follow. An even
clearer way of adding up numbers is to use a query expression:
{fold X with (+) | X in L}
This query expression frees us from most of the commitments we endured
before: it can add up the elements of any kind of collection — not
just cons
lists — and it can add up floating point numbers
just as easily as integers. Finally, we have not had to say exactly
how the numbers should be added up: the language system is free to use
a parallel algorithm for the computation should it be more optimal.
The query expression is also very close to the natural specification:
Add up the numbers in L
Starâs query expressions — which are similar to but also more expressive than LINQ — can be used to encapsulate a wide range of such computations. We shall look deeper into them when we look at query rules in Star.
Of course, SQL programmers have long had access to this kind of conciseness and declarative expressiveness. However, SQL is constrained by the fact that it is intended to represent queries and actions over a very particular form of data — the relational table.
Previous: A totalizer query, Up: A functional loop [Contents][Index]
Programming is often taught in terms of constructing sequences of steps that must be followed. What does that imply for the programmer? It means that the programmer has to be able to imagine what it is like to be a computer following instructions.
It is like imagining a little person — a homunculus — in the machine that is listening to your instructions and following them literally. You, the programmer, have to imagine yourself in the position of the homunculus if you want to write effective programs in most languages today.
Not everyone finds such feats of imagination easy. It is certainly often tedious to do so. Using query expressions and other higher-order abstractions significantly reduces the programmerâs burden — precisely by being able to take a more declarative approach to programming.
Next: There is more, Previous: A functional loop, Up: A tour of Star [Contents][Index]
The concepts of interface and contract are foundational in modern software engineering. This is because explicit interfaces make it substantially easier to develop and evolve systems. A Star contract goes beyond the traditional concept of interface in important ways: we do not mark the definition of a type with its implemented contracts and we allow contracts to involve multiple types.
A contract defines a collection of signatures and an implementation provides specific implementations for those functions for a specific type (or type combination).
For example, we can imagine a contract for simple four function calculator arithmetic containing definitions for the basic four functions of addition, subtraction, multiplication and division:
contract all t ~~ four[t] ::= { plus : (t,t)=>t. sub : (t,t)=>t. mul : (t,t)=>t. div : (t,t)=>t. }
This contract defines — but does not implement — the four
calculator functions plus
, sub
, mul
and
div
. All these functions have a similar type, the type for
plus
is:
plus : all t ~~ four[t] |: (t,t)=>t.
The clause four[t] |:
is a type constraint, specifically
a contract constraint. So, these functions are generic
(universally quantified) but the bound type (t
) has the
additional constraint that there must be an implementation for
four
for t
.
The four
contract defines a set of functions that can be used
without necessarily knowing the type(s) that are involved. For
example, we can define the double
function in terms of
plus
:
double(X) => plus(X,X).
The type of double
reflects the fact that we are using elements
from the four
contract:
double : all t ~~ four[t] |: (t)=>t.
I.e., it inherits the same constraint as the function plus
has. There are several kinds of type constraint in Starâs type
system; but the contract constraint is the most significant of
them.
Notice that we have to give an explicit type annotation for
double
. The reason is that we want to have it have a quantified type.
| • Implementing contracts: | ||
| • Coercion not casting: |
Next: Coercion not casting, Up: Contracts and constrained types [Contents][Index]
Defining a contract is a big step, but it is not generally sufficient
to produce working programs. If we had a worksheet
containing
only:
worksheet{ contract all t ~~ four[t] ::= { plus : (t,t)=>t. sub : (t,t)=>t. mul : (t,t)=>t. div : (t,t)=>t. } double : all t ~~ four[t] |: (t)=>t. double(X) => plus(X,X). show double(2) }
we would get a compiler error along the lines of:
2:integer which is not consistent with display[t_12] , four[t_12] |: t_12 because four[integer] not known to be implemented
This error message is effectively warning us that we have defined the
four
contract but we have not implemented it. Until we do, the
program is not complete. However, if we do supply an implementation of
four over integer
s:
worksheet{ contract all t ~~ four[t] ::= { plus : (t,t)=>t. sub : (t,t)=>t. mul : (t,t)=>t. div : (t,t)=>t. } double : all t ~~ four[t] |: (t)=>t. double(X) => plus(X,X). implementation four[integer] => { plus(x,y) => x+y. sub(x,y) => x-y. mul(x,y) => x*y. div(x,y) => x/y. } show double(2) }
then everything works as expected.
Notice that the error message above shows that type t_12 actually has two type constraints:
display[t_12] , four[t_12] |: t_12
This is because the show
action also results in a type
constraint being involved. The display
contract is used to
display values in a number of circumstances; including the string
formatting we saw above.
As may be expected, arithmetic itself is also mediated via the arithmetic contract in Star. This is how we can support multiple numeric types using a common set of operators: there are standard implementations of arithmetic for integers, and floating point numbers.
Previous: Implementing contracts, Up: Contracts and constrained types [Contents][Index]
Star does not support automatic type casting, as found in languages like Java and C/C++. This is for many reasons, not the least of which is safety and predictability of code.
Casting in many languages is really two kinds of operations-in-one which we can refer to as casting and coercion. Casting is mapping of a value from one type to another without changing the value itself; and coercion involves converting a value from one type to another.
For example, the Java cast expression:
(Person)X
amounts to a request to verify that X
is actually a
Person
object. In particular, this only checks the value of
X
to see if it is a Person
. On the other hand, casting
an integer to a floating point number involves changing the value to
conform to the floating point representation.
Star does not support casting, but does support coercion. However, coercion in Star is never silent or implicit – as it can be in Java and C/C++. An expression of the form:
3+4.5
will fail to type in Star – because there is an attempt to add an integer to a floating point number.
The reason for signaling an error is strongly related to safety and predictability: automatic conversion of integers to floating point can be a common source of errors in languages like C – because such coercions are not always guaranteed to be semantics preserving (not all integers can be represented as floating point values). The implicit coercion of numeric values is easy to miss when reading arithmetic expressions.
Star provides a coercion notation that allows programmers to be precise in their expectations:
(3 :: float)+4.5
denotes the explicit coercion of the integer 3
to a
float
and type checks as expected.
In fact, type coercion in Star is mediated via a contract and this expression is equivalent to
(_coerce(3):float)+4.5
where _coerce
is defined in the coercion
contract
involving two types:
contract all s,t ~~ coercion[s,t] ::= { _coerce :: (s)=>t }
The coercion
contract is an interface, but has no analog in
most OO languages: it involves two types – the source type and the
destination type. Each implementation of coercion specifies both
types. For example, the implementation of coercion between integers
and floating point is explicitly given:
implementation coercion[integer,float] => { … }
This statement gives the implementation for coercing integers to floats. Other implementation statements give the definitions for other forms of coercion.
Having coercion as a contract makes it straightforward to add new
forms of coercion. This is used quite extensively within Star
itself: for example, parsing JSON can be viewed as coercion from
string values to json
values. Thus the interface to parsers can
be standard across all types and parsers.
Previous: Contracts and constrained types, Up: A tour of Star [Contents][Index]
As we have noted, Star is a rich language and it would be impossible to try to cover it in a short introduction. Later chapters will look at some of the other features such as a deeper look at contracts, queries & query rules, actors, concurrency, existential types, and extending Star with domain specific languages. The next chapter (See Functional Programming) starts this process by looking at functional programming in Star.
Next: Collections, Previous: A tour of Star, Up: Top [Contents][Index]
There is a perception of functional programming that it is weird and difficult. This is unfortunate for a number of reasons; the most important being that functional programming is not weirder than procedural programming and that all programmers can benefit by programming functionally.
As for being difficult, a more accurate description would be that there is a deeper range of features in functional programming than in most modern programming languages: so a perception of complexity can arise simply because there is more to say about functional programming languages. However, the simplest aspects of functional programming are very simple and the ramp need not be steep.
What may be surprising to the reader who is not familiar with functional programming is that it is old: predating the origins of modern computing itself, that there is a huge amount that can be expressed functionally, and that functional programming is often at least as efficient and sometimes more efficient than procedural programming.
In this chapter we will show how we can utilize Star as a vehicle for functional programming. As a side-goal, we also hope to demystify some of the language and ideas found in functional programming.
| • What is functional programming?: | ||
| • Basics: | ||
| • Another look at types: | ||
| • Functions as values: | ||
| • Going further: | ||
| • Polymorphic arithmetic: | ||
| • A word about type inference: | ||
| • Are we there yet?: |
Next: Basics, Up: Functional Programming [Contents][Index]
The foundations of functional programming rest on two principles:
This is what people mean when they say that functional programs are declarative.12
This last principle is what people mean when they refer to functions as being first class values. It is also what is meant when we say that functional programming languages are higher order.
It is worth asking why these two principles are so important. Although most early programmers were mathematicians; the extreme constraints imposed by early machines meant that one might not have seen much evidence of mathematical thinking in those early programs. However, almost by accident, programming and mathematics share some attributes: the importance of composition and the power of abstraction. Functional programming is almost ideally placed to exploit both of these to the full.
Star is not actually a pure functional programming language; i.e., it is possible to write programs that violate the declarative principle. However, it is a functional-first programming language: a declarative style is strongly encouraged. In this book we shall mostly focus on writing pure functional programs in Star.
Next: Another look at types, Previous: What is functional programming?, Up: Functional Programming [Contents][Index]
It is often easier to introduce functional programming using numerical examples. Last chapter we saw, for example, the factorial program. This is mostly because most programmers are already familiar with numbers. Continuing that tradition, here is a function that returns the sign of a number:
sign(X) where X<0 => -1. sign(0) => 0. sign(X) where X>0 => 1.
Each of these equations applies to different situations: the first equation applies when the input argument is negative, the second when it is exactly zero and the third when it is strictly positive. These represent the three possible cases in the definition of the sign function.
A Star function may be built from any number of rewrite equations; however, they must all be contiguous within the same group of statements.
Although it is good practice to ensure that equations in a function definition do not overlap, Star will try the equations in a function definition in the order they are written in.13 We could have relied on this and written ‘sign‘ using:
sign(X) where X<0 => -1. sign(0) => 0. sign(X) => 1.
Sometimes it is important to mark a particular equation as the default case: i.e., an equation that should be used if none of the other cases apply:
sign(X) where X<0 => -1. sign(0) => 0. sign(X) default => 1.
An explicitly marked ‘default‘ equation does not need to be the last equation; but, wherever it is written, default equations are only attempted after all other equations have failed to apply.
| • Functions: | ||
| • Order of evaluation: |
Next: Order of evaluation, Up: Basics [Contents][Index]
A function is defined as a sequence of rewrite equations each of which consist of a pattern and an expression. There are three general forms of rewrite equations:
Pattern => Expression
or
Pattern where Condition => Expression
or
Pattern default => Expression
The left hand side of a rewrite equation consists of a pattern which determines the applicability of the equation; and the right hand side represents the value of the function if the pattern matches.
Pattern: A pattern represents a test or guard on an (implicit) value. Patterns can be said to succeed or fail depending on whether the value being tested matches the pattern.
We also refer to a pattern being satisfied when matching a value.14
The pattern in a rewrite equation is a guard on the arguments of the function call. For example, given a call
sign(34)
the patterns in the different equations of the sign
function
will be applied to the integer value 34
.
When the pattern on the left hand side of a rewrite equation succeeds then the equation fires and the value of the expression on the right hand side of the equation becomes the value of the function.
There are many kinds of pattern in Star; here, we look at three of the most common kinds of pattern, and in later sections, we look at additional forms of patterns.
A variable pattern is denoted by an identifier; specifically by the first occurrence of an identifier.
A variable pattern always succeeds and has the additional effect of binding the variable to the value being matched.
For example, the X
in the left hand side of
double(X) => X+X
is a variable pattern. Binding X
means that it is available for
use in the right hand side of the equation – here to participate in
the expression X+X
.
The part of the program that a variable has value is called its scope.
Subsequent occurrences of variables in a pattern are semantically
equivalent to an equality test; specifically a call to the ==
predicate. For example, in the equation:
same(X,X) => true.
the second occurrence of X
is regarded as an equality test;
i.e., this equation is equivalent to:
same(X,X1 where X==X1) => true.
Sometimes, the earlier occurrence of a variable is not in the pattern itself but in an outer scope.
A literal pattern – such as a numeric literal or a string literal – only matches the identical number or string.
Clearly, a literal match amounts to a comparison of two values: the pattern match succeeds if they are identical and fails otherwise.
Equality is based on semantic equality rather than reference equality. What this means, for example, is that two strings are equal if they have the same sequence of characters in them, not just if they are the same object in memory.
NOTE: not all types admit equality: for example, functions are not comparable; similarly, implementing equality for circular structures is problematic.15
There is no automatic coercion of values to see if they might match. In particular, an integer pattern will only match an integer value and will not match a float value – even if the numerical values are the same. I.e., there will be no attempt made to coerce either the pattern or the value to fit.
This, too, is based on the desire to avoid hard-to-detect bugs from leaking into a program.
Sometimes known as a semantic guard, a guard pattern consists of a pair of a pattern and a condition:
Pattern where Condition
Conditions are boolean-valued and a guard succeeds if both its pattern matches and if its condition is satisfied.
Note that conditions may bind variables. This is why we do not state that conditions are boolean-valued expressions.
Star has a normal complement of special conditional forms which we shall explore as we encounter the need. In the case of the equation:
sign(X) where X>0
the guard pattern is equivalent to:
X where X>0
We can put guard pattern anywhere that a pattern is valid; and, for
convenience, we can also put them immediately to the left of the
rewrite equation’s =>
operator.
Any variables that are bound by the pattern part of a guarded pattern are in scope in the condition part of the guard. Furthermore, any variables that are bound by the condition part of the guarded pattern have the same scope as variables introduced in the pattern.
In the pattern above, the variable X
will be bound in the
variable pattern X
and will then be tested by evaluating the
condition X>0
.
Star is a so-called strict language. What that means is that arguments to functions are evaluated prior to calling the function.
We do not specify the order of evaluation of the arguments of the function; except that:
- Arguments are evaluated before entry to the function.
- The function is evaluated before entry to the function.
Most programming languages are strict; for two main reasons:
There many possible styles of evaluation order; one of the great merits of programming declaratively is that the order of evaluation does not affect the actual results of the computation.
It may, however, affect whether you get a result. Different strategies for evaluating expressions can easily lead to differences in which programs terminate and which do not.
One other kind of evaluation that is often considered is lazy evaluation. Lazy evaluation means simply that expressions are only evaluated when needed. Lazy evaluation has many potential benefits: it certainly enables some very elegant programming techniques.
Essentially for the reasons noted above, Star does not use lazy evaluation; however, as we shall see, there are features of Star that allow us to recover some of the power of lazy evaluation.16
The other dimension in evaluation order relates to the rewrite equations used to define functions. Here, Star uses an in-order evaluation strategy: the equations that make up the definition of a function are tried in the order that they are written – with the one exception being any default equation which is always tried last.
Next: Functions as values, Previous: Basics, Up: Functional Programming [Contents][Index]
Organizing data is fundamental to any programming language. Star’s data types are organized around the algebraic data type. In addition, Star’s supports quantified types of several varieties.
| • Quantifier types: | ||
| • Contract constrained types: | ||
| • Algebraic data types: |
Next: Contract constrained types, Up: Another look at types [Contents][Index]
A generic type is one which has one or more type variables in it. For example, the type expression:
(x,x)=>boolean
is such a generic type (assuming that x
is a type variable –
see below).
All type variables must be bound by a quantifier in some enclosing scope. If a type variable is not bound within a particular type expression, it is considered free in that type expression.
A quantified type is a type that introduces (i.e., binds) a type variable. There are two quantifiers in Star: a universal quantifier and an existential quantifier.
The most common quantifier is the universal quantifier and universally quantified types correspond closely to generic types in other languages.
Universally quantified types are often used to denote function types and collection types. For example, the type
all x ~~ (x,x)=>boolean
denotes the type of a generic binary function that returns a boolean
value. The standard type for the equality predicate ==
is
similar to this type.
A universally quantified type should be read as ‘for all possible values’ of the bound variable. For example, this function type should be read as denoting functions that:
for any possible type –
x
– the function takes two suchx
’s and returns aboolean
.
Star also supports existentially quantified types – these are useful for denoting the types of modules and/or abstract data types. For example, the type expression:
exists e ~~ { f1 : e }
denotes the type of a record with a field – f1
– which has a
type. The analogous reading for this type expression would be:
there is a type –
x
– such that the record has a field – calledf1
– of this type.
As may be guessed, this is kind of obscure: f1
has a type, but
we don’t know much else about it!
However, existential types can be very useful, especially in combination with record types like this one. We will leave our more detailed exploration of existential types for later.
Next: Algebraic data types, Previous: Quantifier types, Up: Another look at types [Contents][Index]
We noted above that the type of the standard equality predicate was almost the same as:
all x ~~ (x,x)=>boolean
This type denotes a universally quantified function type that can be applied to arguments of any given type. However, equality in a normal programming language is not universal: not all values admit to being reliably tested for equality. A great example of such a limitation are functions – equality between functions is not well defined.17
To capture this, we need to be able to constrain the scope of the quantifier; specifically to those argument types that do admit equality.
We can do this by adding a contract constraint to the type –
the constraint states that equality must be defined for the type. We
do this by prepending an equality
constraint clause to the
type:
all x ~~ equality[x] |: (x,x)=>boolean
The equality[x] |:
clause states that the type variable
x
must satisfy the equality
contract.
What is implied when we state this? This is captured in the definition of the contract itself, in this case:
contract all t ~~ equality[t] ::= { (==) : (t,t) => boolean. }
In effect, the equality
contract states that there must be a
single function defined – ==
– that is defined for any type that
claims to satisfy the equality
contract.
If this seems a little circular, it is not. The equality
contract is effectively saying that the ==
function must be
defined for the type; and we constrain function (and other) types with
the equality
contract constraint when we need to ensure that
==
is defined!
We provide evidence for contracts through the implementation
statement. This declares that a given type satisfies a contract by
providing implementations for the functions in the contract.
For example, we can provide evidence that the equality
contract
applies to strings using a built-in primitive to actually implement
equality for strings:
implementation equality[string] => { s1 == s2 => _string_eq(s1,s2). }
We shall explore more fully the power of this form of type constraint in later sections and chapters. For now, the core concept is that quantified types can be constrained to allow very precise formulations of types.
Previous: Contract constrained types, Up: Another look at types [Contents][Index]
An algebraic data type definition achieves several things simultaneously: it introduces a new type into scope, it gives an enumeration of the legal values of the new type and it defines both constructors for the values and it defines patterns for decomposing values. This is a lot for a single statement to do!
For example, we can define a type that denotes a point in a two-dimensional space:
point ::= cart(float,float).
This kind of statement is called a type definition statement and is legal in the same places that a function definition is legal.
The new type that is named by this statement is point; so, a variable may have point type, we can pass point values in functions and so on.
The constructor cart allows us to have expression that allow new point structures to be made:
cart(3.4,2.1)
cart
is also the name of a pattern operator that we can
use to take apart point values. For example, the euclid function
computes the Euclidian distance associated with a point:
euclid:(point)=>float. euclid(cart(X,Y)) => sqrt(X*X+Y*Y).
Of course, this particular point
type is based on the
assumption that point values are represented in a cartesian coordinate
system. One of the more powerful aspects of algebraic data types is
that it is easy to introduce multiple alternate forms of data. For
example, we might want to support two forms of point: in cartesian
coordinates and in polar coordinates. We can do this by introducing
another case in the type definition statement:
point ::= cart(float,float) | polar(float,float).
Of course, our euclid
function also needs updating with the new
case:
euclid:(point)=>float. euclid(cart(X,Y)) => sqrt(X*X+Y*Y). euclid(polar(R,T)) => R.
cart
and polar
are called constructor
functions. The term constructor refers to the common
programming concept of constructing data structures. They are called
functions because, logically, they are functions.
For example, we might give a type to polar
:
polar : (float,float)=>point
In fact, constructor functions are one-to-one functions. Variously known as free functions (in logic), bijections (in Math), one-to-one functions are guaranteed to have an inverse. This is the logical property that makes constructor functions useful for representing data.
Of course, we are talking of a logical property of constructor functions. Internally, when implementing functional languages like Star, the values returned by constructor functions are represented using data laid out in memory – just like in any other programming language.
Star actually uses a special type for constructor functions; so
the correct type of polar
is given by:
polar : (float,float)<=>point
The double arrow representing the fact that constructor functions are bijections.
In addition to constructor functions, an algebraic type definition can
introduce two other forms of data: enumerated symbols and
record functions. Enumerated symbols are quite useful in
representing symbolic alternatives. The classic example of an
enumerated type is daysOfWeek
:
daysOfWeek ::= monday | tuesday | wednesday | thursday | friday | saturday | sunday.
Another example is the standard boolean
type which is defined:
boolean ::= true | false.
Unlike enumerated symbols in some languages, there is no numeric value associated with an enumeration symbol: an enumerated symbol ‘stands for’ itself only. The reason for this will become clear in our next type definition which mixes enumerated symbols with constructor functions:
sTree ::= sEmpty | sNode(sTree,string,sTree)
In addition to mixing the enumerated symbol (sEmpty
) with the
sNode
constructor, this type is recursive: in fact, this
is a classic binary tree type where the labels of the non-empty nodes
are strings. (We shall see shortly how to generalize this).
Whenever you have a recursive type, its definition must always include
one or more cases that are not recursive and which can form the base
case(s). In that sense, an enumerated symbol like sEmpty
plays
a similar role in Star as null does in other languages; except that
sEmpty
is only associated with the sTree type.
We can use sTree
to construct binary trees of string value; for
example:
sNode(sNode(sEmpty,"alpha",sEmpty), "beta", sNode(sEmpty,"gamma",sEmpty))
denotes the tree in:
One of the hallmarks of languages like Star is that every value has a legal syntax: it is possible to construct an expression that denotes a literal value of any type.
Just as we can define sTree
values, so we can also define
functions over sTree
s. For example, the check
function
returns true
if a given tree contains a particular search term:
check(sEmpty,_) => false. check(sNode(L,Lb,R),S) => Lb==S || check(L,S) || check(R,S).
Here we see several new aspects of Star syntax:
_
– matches anything. It is
called the anonymous pattern and is used whenever we don’t care
about the actual content of the data.
||
disjunction is a short-circuit disjunction; much
like ||
in languages like Java. Similarly, conjunction
(&&
) is also short-circuiting.
We can use sTest
to check for the occurrence of particular
strings:
T = sNode(sNode(sEmpty,"alpha",sEmpty), "beta", sNode(sEmpty,"gamma",sEmpty)). show check(T,"alpha"). -- results in true show check(T,"delta"). -- results in false
Next: Going further, Previous: Another look at types, Up: Functional Programming [Contents][Index]
The second principle of functional programming is that functions are first class. What that means is that we can have functions that are bound to variables, passed into functions and returned as the values of functions. In effect, a function is a legal expression in the language. It also means that we can have function types in addition to having types about data.
We can see this best by looking at a few examples. One of the benefits
of passing functions as arguments to other functions is that it makes
certain kinds of parameterization easy. For example, suppose that you
wanted to generalize check
to apply an arbitrary test to each
node – rather than just looking for a particular string.
We will first of all define our fTest
function itself:
fTest:(sTree,(string)=>boolean)=>boolean. fTest(sEmpty,_) => false. fTest(sNode(L,Lb,R),F) => F(Lb) || fTest(L,F) || fTest(R,F).
The substantial change here is that, rather than passing a string to
look for, we pass fTest
a boolean-valued function to apply;
within fTest
we replace the equality test Lb==S
with a
call F(Lb)
.
Notice that the type annotation for fTest
shows that the type
of the second argument is a function type – from string
to
boolean
.
Given fTest
, we can redefine our earlier check
function
with:
check(T,S) => fTest(T,(X)=>X==S).
We have a new form of expression here: the anonymous function or lambda expression. The expression
(X)=>X==S
denotes a function of one argument, which returns true
if its
argument is the same value as S
.
Interestingly, it would be difficult to define a top-level function
that is equivalent to this lambda because of the occurrence of the
variable S
in the body of the lambda. This is an example of a
free variable: a variable that is mentioned in the body of a
function but which is defined outside the function. Because S
is free, because it is not mentioned in the arguments, one cannot
simply have a function which is equivalent to the lambda as a
top-level function.
Free variables are a powerful feature of functional programming
languages because they have an encapsulating effect: in this
case the lambda encapsulates the free variable so that the
fTest
function does not need knowledge of S
.
| • Functions and closures: | ||
| • Let binding: | ||
| • Generic types: | ||
| • Generic functions: |
Next: Let binding, Up: Functions as values [Contents][Index]
If a function is an expression, what is the value of the function expression? The conventional name for this value is closure:
A closure is a structure that is the value of a function expression and which may be applied to arguments.
It is important to note that, as a programmer, you will never ‘see’ a closure in your program. It is an implementation artifact in the same way that the representation of floating point numbers is an implementation artifact that allow computers to represent fractional numbers but which programmers (almost) never see explicitly in programs.
Pragmatically, one of the important roles of closures is to capture any free variables that occur in the function. Most functional programming languages implement functions using closure structures. Most functional programming languages (including Star) do not permit direct manipulation of the closure structure: the only thing that you can do with a closure structure is to use it as a function.
In the world of programming languages, there is a lot of confusion about closures. Sometimes you will see a closure referring to a function that captures one or more free variables.
Next: Generic types, Previous: Functions and closures, Up: Functions as values [Contents][Index]
We noted that it is difficult to achieve the effect of the
(X)=>X==S
lambda expression with named functions. The reason is
that the lambda is not defined in the same way that named
functions are defined – because it occurs as an expression not as a
statement. If we wanted to define a named function which also captures
S
, we would have to be able to define functions inside
expressions.
There is an expression that allows us to do this: the let
expression. A let
expression allows us to introduce local
definitions anywhere within an expression. We can define our lambda as
the named function isS
using the let
expression:
let{ isS(X) => X==S } in isS
The region between the braces is a definition environment and Star allows any definition statement to be in such an environment. We can define check using a let expression:
check(T,S) => fTest(T, let{ isS(X) => X==S. } in isS)
This is a somewhat long-winded way of achieving what we did with the
anonymous lambda function – we would not normally recommend this way
of writing the check
function as it is significantly more
complicated than our earlier version. However, there is a strong
inter-relationship between anonymous lambdas, let expressions and
variable definitions. In particular, these are equivalent:
let{ isS = (X) => X==S } in isS
and
(X)=>X==S
Apart from being long-winded, the let
expression is
significantly more flexible than a simple lambda. It is much easier
within a let
expression to define functions with more than one
rewrite equation; or to define multiple functions. We can even define
types within the let binding environment.
Conversely, lambda functions are so compact because they have strong limitations: you cannot easily define a multi-rewrite equation function with a lambda and you cannot easily define a recursive function as a lambda.
In short, we would use a let
expression when the function being
defined is at all complex; and we would use a lambda when the function
being defined is simple and small.
Assembling functions in this way, either by using anonymous lambdas or
by using let
expressions, is one of the hallmarks of functional
programming.
Next: Generic functions, Previous: Let binding, Up: Functions as values [Contents][Index]
What actually makes fTest
more constrained than it could be is
the type definition of sTree
itself. It too is unnecessarily
restrictive: why not allow trees of any type? We can, using the type
definition for tree
:
all t ~~ tree[t] ::= tEmpty | tNode(tree[t],t,tree[t]).
Like the original sTree
type definition, this statement
introduces a new type: tree[t]
which can be read as tree
of something. The name tree
is not actually a type identifier
– although we often refer to the tree type – but it is a type
constructor.
In an analogous fashion to constructor functions, a type constructor constructs types from other types. Type constructors are even bijections – one-to-one functions from types to types.
Unlike constructor functions though, type functions play no part in the run-time evaluation of programs.
The identifier t
in the type definition for tree
denotes
a type variable. Again, similarly to regular variables and
parameters, a type variable denotes a single unspecified type. The
role of the type variable t
is like a parameter in a function:
it identifies the unknown type and its role.
The tree
type is a universally quantified type. What that means
is that instead of defining a single type it defines a family of
related types: for example:
tree[string] tree[integer] …
are tree
types. We can even have trees of trees:
tree[tree[string]]
We capture this genericity of the tree type by using a universal quantifier:
all t ~~ tree[t]
What this type expression denotes is a set of possible types: for any
type t
, tree[t]
is also a type. There are infinitely
many such types of course.
The all
quantifier is important: as in logic, there are two
kinds of quantifiers in Star’s type system: the universal
quantifier all and the existential quantifier exists.
Star uses context to determine whether any given identifier is a type variable or a type name. Specifically, if an identifier is bound by a quantifier then it must refer to a type variable.
The types of the two constructors introduced in the tree
type
definition are similarly quantified:
tEmpty:all t ~~ tree[t]. tNode:all t ~~ (tree[t],t,tree[t)]<=>tree[t].
The type tree[t]
on the right hand side of tEmpty
’s type
annotation raises a couple of interesting points:
tEmpty
symbol was originally introduced in a type
definition is enough of a signal for the compiler to avoid looking for
a definition for the name.
tEmpty
expression – assuming that no
further information is available – will be of the form
tree[t34]
where t34
is a ‘new’ type variable not
occurring anywhere else in the program. In effect, the type of
tEmpty
is tree of some type t34
where we don’t
know anything more about t34
.
Previous: Generic types, Up: Functions as values [Contents][Index]
Given this definition of the tree type, we can construct a more general form of the tree test function; which is almost identical to fTest:18
test:all t ~~ (tree[t],(t)=>boolean)=>boolean. test(tEmpty,_) => false. test(tNode(L,Lb,R),F) => F(Lb) || test(L,F) || test(R,F).
and our original string check function becomes:
check(T,S) => test(T,(X) => X==S)
The type of check is also more generic:
check:all t ~~ (tree[t],t)=>boolean
I.e., check
can be used to find any type of element in a tree
– providing that the types align of course.
Actually, this is not the correct the type for check. This is because we do not, in general, know that the type can support equality. The precise type for check should take this into account:
check:all t ~~ equality[t] |: (tree[t],t) => boolean
Next: Polymorphic arithmetic, Previous: Functions as values, Up: Functional Programming [Contents][Index]
Although better than the original sTest
program there is still
one major sense in which the test program is not general enough. We
can see this by looking at another example: a function that counts
elements in the tree:
count:all t ~~ (tree[t]) => integer. count(tEmpty) => 0. count(tNode(L,_,R)) => count(L)+count(R)+1
This code is very similar, but not identical, to the test
function.
The issue is that test
is trying to do two things
simultaneously: in order to apply its test predicate to a binary tree
it has to implement a walk over the tree, and it also encodes the fact
that the function we are computing over the tree is a boolean-value
function.
We often need to do all kinds of things to our data structures and writing this kind of recursion over and over again is tedious and error prone. What we would like to do is to write a single visitor function and specialize it appropriately when we want to perform a specific function.
This principle of separating out the different aspects of a system is one of the core foundations of good software engineering. It usually goes under the label separation of concerns. One of the beautiful things about functional programming is that it directly supports such good architectural practices.
Since this visitor may be asked to perform any kind of computation on the labels in the tree we will need to slightly generalize the type of function that is passed to the visitor. Specifically, the type of function should look like:
F : (a,t)=>a
where the a
input represents accumulated state, t
represents an element of the tree and the result is another
accumulation.
Using this, we can write a tVisit
function that implements tree
walking as:
tVisit:all a,t ~~ (tree[t],(a,t)=>a,a)=>a. tVisit(tEmpty,_,A) => A. tVisit(tNode(L,Lb,R),F,A) => tVisit(R,F,F(tVisit(L,F,A),Lb)).
Just as the accumulating function acquires a new ‘state’ parameter, so
the tVisit
function also does. The A
parameter in the
two equations represents this accumulated state.
The second rewrite equation for tVisit
is a bit dense so let us
open it out and look more closely. A more expanded way of writing the
tVisit
function would be:
tVisit(tEmpty,_,A) => A. tVisit(tNode(L,Lb,R),F,A) => let{ A1 = tVisit(L,F,A). A2 = F(A1,Lb). } in tVisit(R,F,A2)
where A1
and A2
are two local variables that represent
the result of visiting the left sub-tree and applying the accumulator
function respectively. We have used the let expression form to make
the program more obvious, rather than to introduce new functions
locally; but this is a legitimate role for let expressions.
The tVisit
function knows almost nothing about the computation
being performed, all it knows about is how to walk the tree and it
knows to apply functions to labels in the tree.
Given tVisit
, we can implement our original check
and
count
functions as one-liners:
check(T,S) => tVisit(T,(A,X)=>(A || X==S),false). count(T) => tVisit(T,(A,X)=>A+1,0).
The lambda that is embedded in the definition of check bears a little closer scrutiny:
(A,X)=>(A || X==S)
In this lambda, we return A
– if it is true
– or we
return the result of the test X==S
. This is a common pattern in
such programs: the accumulator A
acts as a kind of state
parameter that keeps track of whether we have already found the value.
Functional programs are not actually state-free; often quite the opposite. However, the state in a functional program is never hidden. This is the true distinction between functional and regular procedural programs.
Notice that we have effectively hidden the recursion in the function
definitions of check
and count
– all the recursion is
encapsulated within the tVisit
function.
One of the unofficial mantras of functional programming is hide the recursion.
The reason we want to hide recursions that this allows the designer of functions to focus on what is being computed rather than focusing on the structure of the data and, furthermore, this allows the implementation of the visitor to be shared by all users of the tree type.
Notice that, while a
and t
are type variables, we did
not put an explicit quantifier on the type of F
. This is
because the quantifier is actually put on the type of tVisit
instead:
tVisit:all a,t ~~ (tree[t],(a,t)=>a,a)=>a
Just like regular variables, type variables have scope and points of introduction. Also like regular variables, a type variable may be free in a given type expression; although it must ultimately be bound by a quantifier.
| • Going even further: |
Up: Going further [Contents][Index]
We have focused so far on generalizing the visitor from the
perspective of the tree type. But there is another sense in which we
are still architecturally entangled: from the perspective of
the check
and count
functions themselves.
In short, they are both tied to our tree
type. However, there
are many possible collection data types; Star for instance has some
5 or 6 different standard collection types. We would prefer not to
have to re-implement the check
and count
functions for
each type.
The good news is that, using contracts, we can write a single
definition of check
and count
that will work for a range
of collection types.
Let us start by defining a contract that encapsulates what it means to visit a collection:
contract all c,t ~~ visitor[c->>t] ::= { visit:all a ~~ (c,(a,t)=>a,a)=>a }
This visitor
contract defines a single function that embodies
what it means to visit a collection structure. There are quite
a few pieces here, and it is worth examining them carefully.
A contract header has a template that defines a form of contract constraint. The clause
visitor[c ->> t]
is such a constraint. The sub-clause
c ->> t
refers to two types: c
and t
. The presence of the
->>
term identifies the fact that t
depends on
c
.
The visitor
contract itself is about the collection type
c
. But, within the contract, we need to refer to both the
collection type and to the type of elements in the collection: the
visit
function is over the collection, it applies a function to
elements of the collection.
Furthermore, as we design the contract, we do not know the
exact relationship between the collection type and the element
type. For example, the collection type may be generic in one argument
type – in which case the element type is likely that argument type;
conversely, if the type is not generic (like string
say), then we have no direct handle on the element type.
We do know that within the contract the element type is functionally determined by the collection type: if you know the collection type then you should be able to figure out the element type.
We express this dependency relationship with the the c ->> t
form: whatever type c
is, t
must be based on it.
The body of the contract contains a single type annotation:
visit:all a ~~(c,(a,t)=>a,a)=>a
This type annotation has three type variables: the types c
and
t
come from the contract header and a
is local to the
signature. What the signature means is
Given the visitor contract, the
visit
function is from the collection typec
, a function argument and an initial state and returns a new accumulation state.
It is worth comparing the type of visit
with the type of
tVisit
:
tVisit:all t,a ~~(tree[t],(a,t)=>a,a)=>a
The most significant difference here is that in tVisit
the type
of the first argument is fixed to tree[t]
whereas in
visit
it is left simply as c
(our collection type).
Given this contract, we can re-implement our two check
and
count
functions even more succinctly:
check(T,S) => visit(T, (A,X)=>A || X==S,false) count(T) => visit(T, (A,X)=>A+1,0)
These functions will apply to any type that satisfies – or
implements – the visitor
contract. This is made visible in the
revised type signature for count
:
count:all c,t ~~ visitor[c->>t] |: (c)=>integer.
This type is an example of a constrained type. It is generic in
c
and t
but that generality is constrained by the
requirement that the visitor
contract is appropriately
implemented. The eagled-eyed reader will notice that count
does
not actually depend on the type of the elements in the collection:
this is what we should expect since count
does not actually
care about the elements themselves.
The type signature for check
, however, does care about the
types of the elements:
check:all c,t ~~ visitor[c->>t], equality[c] |: (c,t)=>boolean
This type annotation now has two contract constraints associated with
it: the collection must be something that is visitable and the
elements of the collection must support equality
.
Given the work we have done, we can implement the visitor
contract for our tree[t]
type quite straightforwardly:
implementation all t ~~ visitor[tree[t]->>t] => { visit = tVisit }
Notice that header of the implementation statement provides the
connection between the collection type (which is tree[t]
) with
the element type (t
). The clause
visitor[tree[t]->>t]
is effectively a declaration of that connection.
Now that we have disconnected visit
from tree
types, we
can extend our program by implementing it for other types. In
particular, we could also implement the visitor for the sTree
type:
implementation visitor[sTree ->> string] => { visit = sVisit }
however, we leave the definition of sVisit
as a simple exercise
for the reader.
Our final versions of count
and check
are now quite
general: they rely on a generic implementation of the visit
function to hide the recursion and are effectively independent of the
actual collection types involved.
If we take a second look at our visitor contract we can see something quite remarkable: it counts as a definition of the famous visitor pattern. This is remarkable because, although visitor patterns are a common design pattern in OO languages, it is often hard in those languages to be crisp about the semantics of visiting; in fact, they are called patterns because they represent patterns of use which may be encoded in Java (say) whilst not necessarily being definable in them.
The combination of contract and implementation represents a quite formal way of defining patterns like the visitor pattern.
There is something else here that is quite important too: we are able
to define and implement the visitor contract without having to
modify in any way the type definition of tree
or
sTree
. From a software engineering point of view this is quite
important: we are able to gain all the benefits of interfaces without
needing to entangle them with our types. This becomes critical in
situations where we are not able to modify types – because they don’t
belong to us and/or we don’t have access to the source.
Next: A word about type inference, Previous: Going further, Up: Functional Programming [Contents][Index]
There are other ways in which programs can be polymorphic. In particular, let us focus for a while on arithmetic. One of the issues in arithmetic functions is that there are many different kinds of numbers. Pretty much every programming language distinguishes several kinds of numbers; for example, Java distinguishes byte, short, int, long, float, double, BigInteger and BigDecimal – and this does not count the wrapped versions. Other languages have even more choice.
One question that might seem relevant is why? The basic answer is that different applications call for different properties of numbers and no one numeric type seems to fit all needs. However, that variety comes at a cost: when we use numbers we tend to have to make too early a choice for the numeric type.
For example, consider the double
function we saw earlier:
double(X) => X+X
What type should double
have? In particular, what should the
type of +
be? Most people would be reluctant to use different
arithmetic operators for different types of numbers.19 This is resolved in
Star by relying on contracts for the arithmetic operations.
The result is that the most appropriate type signature for
double
is exquisitely tuned:
double:all t ~~ arith[t] |: (t)=>t
This type is precisely the most general type that double
could
have. Any further constraints result in making a potentially premature
choice for the numeric type.
If we take another look at our original fact
function:
fact(0) => 1 fact(N) => N*fact(N-1)
this is constrained to be a function from integer
to
integer
because we introduced the literal integers 0
and
1
. However, the arith
contract contains synonyms for
these very common literals. Using zero
and one
allow us
to be abstract in many arithmetic functions:
genFact:all a ~~ arith[a] |: (a)=>a. genFact(zero) => one. genFact(N) => N*genFact(N-one).
We call out zero
and one for special treatment because they
occur very frequently in numerical functions. We can introduce other
numeric literals without compromising our type by using
coercion; although it is more clumsy:
factorialC:all t ~~ arith[t],coercion[integer,t] |: (t)=>t. factorialC(N) where N==0::t => 1::t. factorialC(N) => N*factorialC(N-1::t).
The expressions 0::t
and 1::t
are coercions from
integer
to t
.
Of course, coercion is also governed by contract, a fact represented
in the type signature by the coercion contract constraints on the type
of t
.
In any case, using these techniques, it is possible to write numeric functions without unnecessarily committing to specific number types. That in turn helps to make them more useful.
| • Optional computing: | ||
• Special syntax for option al values: |
There are many situations where it is not possible to guarantee that a
computation will succeed. The simplest examples of this include
scenarios such as accessing external files; but may also apply to
getting the first element of a list or the label of a tree
node. The great unknown of accessing elements of a collection is ‘is
it there?’. Its not guaranteed of course, and we need to be able to
handle failure.
Many languages employ the concept of a special null
value to
denote some of these cases – like a someOne
not having a
spouse
. However, the special null
value brings its own
problems: the type of null
is problematic (it is a legal value
for every type) and there are many situations where null
is
never possible.
We address this by handling those situations where failure is possible
differently than where it is not. Specifically, we do this via the
option
type.
The type definition of option
is quite straightforward:
all t ~~ option[t] ::= none | some(t).
where none
is intended to denote the non-existence of a value
and some
denotes an actual value.
The option
type is intended to be used in cases where functions
are known to be partial.20 An option
return type signals that the function may not always have a value.
Normal pattern matching can be used to access a value wrapped in a
some
; for example, to access someone’s spouse
we can use
the condition:
isMarriedTo(P,J) where some(JJ).=P.spouse => J==JJ. isMarriedTo(_,_) default => false.
The important detail here is that all access to a option
wrapped value is gated by some form of pattern matching and that,
normally, this takes place in a condition.
The condition
some(JJ).=P.spouserepresents a pattern matching condition: it is satisfied if
P.spouse
matchessome(JJ)
and has the additional effect of defining and binding the variableJJ
to the matched spouse.
Previous: Optional computing, Up: Polymorphic arithmetic [Contents][Index]
option
al valuesOf course, the code above is kind of clumsy! There is a range
of operators in Star to make using option
values more
pleasant.
The most important of these is the ^=
operator which combines
the .=
with the some
match. Using this, the
isMarriedTo
function becomes:
isMarriedTo(P,J) where JJ^=P.spouse => J==JJ. isMarriedTo(_,_) default => false.
The meaning of ^=
is similar to the pattern match condition
.=
; except that the pattern is assumed to be for a some
value.
While the ^=
operator21 is very
useful in unpacking an optional value, the ^|
operator allows
us to handle cases where we always need to be able to give some kind
of value. For example, normally a map
returns none if an entry
is not present. However, a cache is structured differently: if
a value is not present in a cache then we must go fetch it:
cacheValue(K) => cache[K] ^| fetch(K)
We can also apply a match in line to an option
al value. The
^
operator allows a pattern to be formed by applying a
option
valued function directly in place. For example, the
equation:
head(first^(1)) => "alpha"
is equivalent to:
head(X) where some(1).=first(X) => "alpha"
We will see more examples of this when we look more closely at sequences and collections processing.
Finally, we can promote an optional expression into an enclosing expression (which is therefore also optional). For example, in the expression:
nameOf(^P.spouse)
if P.spouse
is none
, then the value returned by the
nameOf
expression is also none
, otherwise it takes the
form:
some("P_spouse_name")
(assuming that nameOf
is defined for Person
s.)
Overall, the option
type is part of an elegant approach to
nullability that is easily incorporated into Star’s (and similar)
type system.
Next: Are we there yet?, Previous: Polymorphic arithmetic, Up: Functional Programming [Contents][Index]
We have seen some powerful forms of types in this chapter: recursive types defined using algebraic type definitions, generic types and even function types. Recall also that Star only requires programmers to explicitly declare the types of quantified variables and functions. It is worth pausing a little to see how this might be done.
Recall our original fact
function:
fact(0) => 1. fact(N) => N*fact(N-1).
The compiler is able to compute the types of the various variables automatically through a process known as type inference. Type inference may seem magical, but is actually (mostly) quite simple. Let us take a look at the expression:
N-1
which is buried within the recursive call in fact
. Although it
looks like a special operator, Star does not treat arithmetic
expressions in a special way; the -
function is just a function
from numbers to numbers; its type is given by:22
(-) : all t ~~ arith[t] |: (t,t)=>t
However, we should simplify this type a little in order to make the
explanation of type inference a little simpler. In what follows, we
assume that the type of (-
) is:
(-) : (integer,integer)=>integer
Type inference proceeds by using special type inference rules which relate expressions to types, in this case the applicable rule is that a function application is consistent if the function’s parameter types are consistent with the types of the actual arguments. If they are consistent, then the type of the function application is the return type of the function.
The type inference process initially gives every variable an unknown
type – represented by a new type variable not appearing anywhere
else. For our tiny N-1
example, we will give N
the type
tN.
The (-
) function has two arguments whose types can be expressed
as a tuple of types:
(integer,integer)
and the types of the actual arguments are also a tuple:
(tN,integer)
In order for the expression to be type correct, the actual types of the arguments must be consistent with the expected types of the function; which we can do by making them the same. There is a particular process used to do this – called unification.
An algorithm that replaces variables with values in such a way as to make two terms identical.
Unification matches equals with equals and handles (type) variables by
substitutions – for example, we can make these two type expressions
equal by binding the type variable tN to
integer
.
We initially picked the type of N
to be an arbitrary type
variable, but the process of checking consistency leads us to refine
this and make the type concrete. I.e., the use of N
in a
context where an integer is expected is enough to allow the compiler
to infer that the type of N
is indeed integer
and not
tN.
Of course, if there are multiple occurrences of N
then each of
those occurrences must also be consistent with integer; and if an
occurrence is not consistent then the compiler will report an error –
a given expression may only have one type!
The bottom line is that Star’s types are based on a combination of unification for comparing types and a series of type rules that have the effect of introducing constraints on types based on which language features are present in the text. The type checker is really a constraint solver: if the constraints are not satisfiable (for example by trying to ‘call’ a variable and add a number to it) then there is a type error in the program.
The magic of type inference arises because it turns out that solving these constraints is sufficient for robustly type checking programs.
A sharp-eyed reader will notice that Star’s type system is different in nature to that found (say) in OO languages. In Star’s type system, types are considered to be consistent in Star if they are equal. This is quite different to the notion of consistency in OO languages where an argument to a function is consistent if its type is a sub-type of the expected type.
However, we would note that the apparent restriction to the type system imposed by type equality is much less severe in practice than in theory – and that OO languages’ type systems also often incorporate some of the same restrictions.
| • Why is type inference restricted?: |
We have stated a few times that Star’s type system only infers types of variables that are not quantified. In fact, it is fairly straightforward to build a type inference system that can infer quantified types. For example, such a complete type inference system would infer from these equations:
conc(nil,x)=>x. conc(cons(h,tl),x) => cons(h,conc(tl,x))
the generalized type for conc
:
conc:all t ~~ (cons[t],cons[t])=>cons[t].
However, several technical and non-technical considerations stay our hand at building such a type inference system:
On the other hand, requiring type annotations for every
variable would be extremely tedious and verbose. An extreme version of
this policy would require the conc
program above to be written:
conc:all t ~~ (cons[t],cons[t])=>cons[t]. conc(nil,x:list[t])=>x. conc(cons(h:t,tl:list[t]),x:list[t]) => cons(h,conc(t,x))
The design of Star strikes a balance between useability and rigor: most variables do not require explicit type annotations. We require them only when something ’special’ is being indicated; one of those special circumstances is when defining a generic function.
Even there, there are many situations where explicit type annotations are not needed: for example when defining a field in a record, or a function in the implementation of a contract, there already is a type that the type system can use to verify the program.
So, the precise rule for type inference is:
If the type of a variable is known from context, then use that type to verify the type of any value the variable may be bound to. Otherwise, use type inference on the value to infer a type for the variable but do not attempt to generalize it by adding quantifiers to the inferred type.
We are only able to scratch the surface of the type system here. It is certainly true that – like many modern functional languages – Star’s type system is complex and subtle. The primary motivation for this complexity is to reduce the burden for the programmer: by being able to infer types automatically, and by being able to address many programming subtleties, the type system comes to be seen as the programmer’s friend rather than as an obstacle to be ‘gotten around’.
Previous: A word about type inference, Up: Functional Programming [Contents][Index]
The straightforward answer to this is no. There is a great deal more to functional programming than can be captured in a few pages. However, we have covered some of the key features of functional programming – particularly as it applies to Star. In subsequent chapters we will take a closer look at collections, at modular programming, at concurrency and even take a pot shot at Monads.
If there is a single idea to take away from this chapter it should be that functional programming is natural. If there is a single piece of advice for the budding functional Star programmer, it should be to hide the recursion. If there is a single bit of comfort to offer programmers it should be that Rome was not built in a day.
In the next chapter we look at collections, one of the richest topics in programming.
Next: Making choices, Previous: Functional Programming, Up: Top [Contents][Index]
Modern programming – whether it is OO programming, functional programming or just plain C programming – relies on a rich standard library. Given that nearly every program needs to be able to manage collections of things, the central pearl of any standard library is the collections library. Recalling our mantra of hiding recursion; a well designed collections library can make a huge difference to the programmer’s productivity, often by hiding many of the recursions and iterations required to process collections.
The collections architecture in Star has four main components:
The query component is sufficiently involved to merit a chapter of its own.
| • Sequence notation: | ||
| • Indexing: | ||
| • Doing stuff with collections: | ||
| • Different types of collection: | ||
| • Collecting it together: |
Next: Indexing, Up: Collections [Contents][Index]
A sequence is an ordered collection; a sequence expression is an
expression involving a complete or partial enumeration of the values
in the collection. Star has a straightforward notation for expressing
sequences of any underlying type; for example, a cons
sequence of
integers from 1 through 5 can be written:
cons of [1, 2, 3, 4, 5]
In situations where we do not know or do not wish to specify the collection type, we can write instead:
[1, 2, 3, 4, 5]
This term – it could be either an expression or a pattern – denotes the sequence without specifying the underlying collection type. The difference in the types of the two terms is telling:
cons[integer]
and
sequence[c->>integer] |: c
respectively – where c
is a type variable. The first is a
concrete type expression, the second is a constrained type – in this
case c
must implement the sequence
contract.
Although the second type expression is longer, and a bit more complex
to read, it is also actually less constraining. The type expression
cons[integer]
does not allow for variation of the underlying
collection type; the second type expression allows the term to be used
in contexts that require different concrete types.
| • Partial sequence notation: | ||
• The stream and sequence contracts: | ||
| • Stream patterns: | ||
| • Notation and contracts: |
Next: The stream
and sequence
contracts, Up: Sequence notation [Contents][Index]
The sequence notation also allows for the specification of partial sequences; this is particularly useful in writing functions that construct and traverse sequences. The sequence term:
[1,2,..X]
denotes the sequence whose first two elements are 1
and
2
and whose remainder is denoted by the variable X
–
which must also be a sequence of the appropriate type. Similarly, the
term:
[F..,23]
denotes the sequence obtained by gluing 23
to the back of the
sequence F
.
There is a strong relationship between the normal sequence notation and the partial sequence notation. In particular, the sequence expression
cons of [1,2]
is equivalent to:
cons of [1,..cons of [2,..cons of []]]
However, we are not permitted to use both of ,..
and ..,
in the same expression:
[F..,2,3,..B]
is not permitted (since it amounts to a concatenation of two sequences which, in turn, implies a non-deterministic decomposition when used as a pattern).
The major benefit of general sequence notation is that it allows us to construct programs involving collections that are independent of type and to do so in a syntax which is concise.
For example, we can use sequence notation to write functions over
sequences; such as the concat
function that concatenates two
sequences:
concat:all c,e ~~ stream[c->>e], sequence[c->>e] |: (c,c)=>c. concat([],X) => X. concat([E,..X],Y) => [E,..concat(X,Y)].
This function will work equally well with cons
lists, lists,
strings, even your own collection types. All that is required is that
there is an implementation of the stream
and the
sequence
contracts for the actual type being concatenated.
There are two contracts here: the
stream
contract is used when decomposing sequences and thesequence
contract is used when building them.
Next: Stream patterns, Previous: Partial sequence notation, Up: Sequence notation [Contents][Index]
stream
and sequence
contractsUnderlying the sequence notation are two contracts: the sequence
contract and the stream
contract. These contracts contains
type signatures that can be used to construct and to match against
sequence values. The sequence notation is realized by the compiler
translating sequence terms to a series of calls to those functions.
The standard stream
contract is
contract stream[t->>e] ::= { _eof:()=>boolean. -- is stream empty _hdtl:(t)=>option[(e,t)]. -- match front of stream _back:(t)=>option[(t,e)]. -- match back of stream }
and the standard sequence
contract is:
contract stream[t->>e] ::= { _nil:t. -- empty stream _cons:(e,t)=>t. -- add to front _apnd:(t,e)=>e. -- add to back }
The entries in the sequence
contract should be fairly self-evident:
_nil
is the empty sequence;
_cons
is a function that ‘glues’ a new element to the front of
the sequence; and
_apnd
appends elements to the *back* of the sequence.
The compiler uses these three functions to transform sequence expressions into function calls.
For example, the sequence expression:
[1,2,3]
is transformed into
_cons(1,_cons(2,_cons(3,_nil())))
If a sequence expression has an explicit type marker on it, then its translation is slightly different – to allow the type checker to make use of the type information. For example,
cons of [1,2]
is translated as:
_cons(1,_cons(2,_nil())):cons[_]
This annotation is all that is needed to force the compiler to treat the result as a concrete cons list. Type inference does the rest of the hard work.23
Next: Notation and contracts, Previous: The stream
and sequence
contracts, Up: Sequence notation [Contents][Index]
The the stream
contract is used in patterns to match and
decompose sequences. For example, the signature for hdtl
–
which is used to decompose sequences into a head and tail – is:
_hdtl:(t)=>option[(e,t)].
This function will be applied to a sequence in the attempt to split it into a head and remainder. The question is how can a function be used in a pattern?
The term [1,2,..X]
as a pattern is rewritten as:
_hdtl^(1,_hdtl^(2,X))
where the ^
is syntactic sugar for the more elaborate form:
S0 where (1,S1) ^= _hdtl(S0) && (2,X)^=_hdtl(S1)
which is, in turn, syntactic sugar for:
S0 where some((1,S1)) .= _hdtl(S0) && some((2,X)) .= _hdtl(S1)
I.e., the sequence pattern becomes a series of progressive
decompositions of the stream; at each stage an option
-valued
function is applied to peel off elements from the stream.
We can now straightforwardly give the translation for sequence patterns. Syntactically, there is no distinction between sequence expressions and stream patterns – what distinguishes them is context: stream patterns show up as patterns in functions and sequence expressions show up in the expression context.
A stream pattern, as in the pattern [E,..X]
for the non-empty
case in concat
:
concat([E,..X],Y) => [E,..concat(X,Y)]
is transformed into the pattern:
_hdtl^(E,X)
and the entire concat
equation becomes:
concat(_hdtl^(E,X),Y) => _cons(E,concat(X,Y))
which, as we noted above, is actually equivalent to:
concat(S0,Y) where some((E,X)).=S0 => _cons(E,concat(X,Y)).
The sequence
and stream
contracts are two of the most
important and commonly used contracts in the Star library. As we
shall see further, many of the standard collections functions are
built on top of it.
We have two contracts – one for composing and another for decomposing sequences – because not all collections are equally amenable to decomposing and/or composing. For example, the
map
type we describe below does not have a natural notion of decomposing (because ordering within amap
is not preserved); even though it does have a natural form of describing actualmap
collections.
Previous: Stream patterns, Up: Sequence notation [Contents][Index]
One of the distinctive features of the sequence notation is that it is an example of syntax that is underwritten by a semantics expressed as a contract. This is part of a widespread pattern in Star.
This has a parallel in modern OO languages like Java and C# where important contracts are expressed as interfaces rather than concrete types. However, Star extends the concept by permitting special notation as well as abstract interfaces – as many mathematicians understand, a good notation can sometimes make a hard problem easy. In Star we further separate interfaces from types by separating the type definition from any contracts that may be implemented by it.
The merit of this combination of special syntax and contracts is that we can have the special notation expressing a salient concept – in this case the sequence – and we can realize the notation without undue commitment in its lower-level details. In the case of sequence notation, we can have a notation of sequences without having to commit to the type of the sequence itself.
Next: Doing stuff with collections, Previous: Sequence notation, Up: Collections [Contents][Index]
Accessing collections conveniently is arguably more important than a good notation for representing them. There is a long standing traditional notation for accessing arrays:
L[ix]
where L
is some array or other collection and ix
is an
integer offset into the array. Star uses a notation based on this
for accessing collections with random indices; suitably generalized to
include dictionaries (collections accessed with non-numeric indices)
and slices (contiguous sub-regions of collections).
Before we explore Star’s indexing notation it is worth looking at
the contract that underlies it – the indexed
contract.
| • The indexed contract: | ||
| • The index notation: | ||
| • Implementing indexing: | ||
| • Index slices: |
Next: The index notation, Up: Indexing [Contents][Index]
The indexed contract captures the essence of accessing a collection in a random-access fashion. There are functions in the contract to access a directly accessed element, to replace and to delete elements from the collection:
contract all s,k,v ~~ indexed[s->>k,v] ::= { _index:(s,k)=>option[v]. _insert:(s,k,v)=>s. _replace:(s,k,v)=>s. _remove:(s,k)=>s. }
There are several noteworthy points here:
_index
which
accesses elements; and
_insert
, _replace
and _remove
which return new collections rather than modifying them in-place.
Recall that the stream
contract had the form:
contract all s, e ~~ stream[s->>e] ::= ...
the s->>e
clause allows the implementation of the contract to
functionally determine (sic) the type of the elements of the
collection.
In the case of indexed
, the contract form determines two
types denoted by k
and v
. The type k
denotes the
type of the key used to access the collection and v
denotes the
type of the elements of the collection. Each individual implementation
of indexed is free to specify these types; usually in a way that best
reflects the natural structure of the collection.
For example, the implementation of indexed
for strings starts:
implementation indexed[string ->> integer,integer] => ...
reflecting the fact that the natural index for strings is integer and the natural element type is integer (neither being explicitly part of the string type name). 24
On the other hand, the implementation of indexed
for the
concrete type map
starts:
implementation all k,v ~~ indexed[map[k,v] ->> k,v] => { … }
reflecting the fact that dictionaries are naturally generic over both the key and value types.
If we look at the signature for _index
we can see that this
function does not directly return a value from the collection, but
instead returns an option
value. This bears further
explanation.
The great unknown of accessing elements of a collection is ‘is it
there?’. Its not guaranteed of course, and we need to be able to
handle failure. In the case of the _index
function, its
responsibility is to either return a value wrapped as a some
value – if the index lookup is successful – or the signal
none
if the index lookup fails. Just to be clear: _index
can act both as a lookup and as a test for membership in the
collection.
| • Adding and removing elements: |
Up: The indexed contract [Contents][Index]
The function _insert
is used to add an element to a collection
associating it with a particular index position; and the function
_remove
removes an identified element from the collection. The
function _replace
is similar to _insert
except that it
is expected that an existing element is replaced rather than a new
value being inserted.
These functions have a property often seen in functional programming languages and not often seen elsewhere: they are defined to return a complete new collection rather than simply side-effecting the collection. This is inline with an emphasis on persistent data structures25 and on declarative programming.
One might believe that this is a bit wasteful and expensive – returning new collections instead of side-effecting the collection. However, that is something of a misconception: modern functional data structures have excellent computational properties and approach the best side-effecting structures in efficiency. At the same time, persistent data structures have many advantages – including substantially better correctness properties and behavior in parallel execution contexts.
It should also be stressed that the
indexed
contract allows and encourages persistence but does not enforce it. It is quite possible to implement indexing for data structures that are not persistent.
Next: Implementing indexing, Previous: The indexed contract, Up: Indexing [Contents][Index]
Given the indexed contract we can now show the specific notation that Star has for accessing elements of a collection. Accessing a collection by index follows conventional notation:
C[ix]
will access the collection C
with element identified by
ix
. For example, given a map
D
of strings to
strings, we can access the entry associated with âalphaâ using:
D["alpha"]
Similarly, we can access the third character in a string S
using:
S[2]
As might be expected, given the discussion above, the type of an index expression is optional.
The most natural way of making use of an index expression is to use it
in combination with a ^=
condition or an ^|
expression
– which allows for smooth handling of the case where the index
fails. For example, we might have:
nameOf(F) where N ^= names[F] => N. nameOf(F) default => ...
We will take a deeper look at exceptions and more elaborate management of tentative computation in Computation Expressions.
Star also has specific notation to represent modified collections. For example, the expression
D["beta"->"three"]
denotes the map D
with the entry associated with "beta"
replaced by the value "three"
. Note that the value of this
expression is the updated map.
For familiarity’s sake, we also suppose a form of assignment for the case where the collection is part of a read-write variable. The action:
D["beta"] := "three"
is entirely equivalent to:
D := D["beta"->"three"]
always assuming that the type of D
permits assignment.
Similarly, the expression:
D[\+"gamma"]
which denotes the map D
where the value associated with the key
"gamma"
has been removed.
Although, in these examples, we have assumed that D
is a map
value (which is a standard type in Star); in fact the index
notation does not specify the type. As with the sequence notation, the
only requirement is that the indexed
contract is implemented
for the collection being indexed.
In particular, as well as the map
type, index notation is
supported for the built-in list
type, and is even supported for
the string
type.
In addition to the indexed access notation described so far, Star also allows a variant of the sequence notation for constructing indexed literals (aka dictionaries). In particular, an expression of the form:
["alpha"->1, "beta"->2, "gamma"->3]
is equivalent to a sequence of tuples, or to:
_cons(("alpha",1),_cons(("beta",2),_cons(("gamma",3),_nil))
which is understood by indexed types as denoting the contruction of a literal.
Note that there are two levels of domain-specific notation here: the
representation of indexed literals in terms of a sequence of
two-tuples and the implicit rule governing indexed types: they should
implement a specific form of sequence
contract. Both are
actually part of the semantics of representing indexed literals.
Next: Index slices, Previous: The index notation, Up: Indexing [Contents][Index]
Of course, this includes our own types. For example, before, when looking at generic types we saw the tree type:
all t ~~ tree[t] ::= tEmpty | tNode(tree[t],t,tree[t]).
We can define an implementation for the indexed contract for this type – if we arrange for the tree to be a tree of key-value pairs:
implementation all k,v ~~ order[k], equality[k] |: indexed[tree[(k,v)]->>k,v] => { _index(T,K) => findInTree(T,K). _insert(T,K,V) => setKinTree(T,K,V). _replace(T,K,V) => setKinTree(T,K,V). _remove(T,K) => removeKfromTree(T,K). }
The form of the type expression tree[(k,v)]
is required to
avoid confusion – tree
takes a single type argument that, in
this case, is a tuple type. The extra set of parentheses ensures that
tree
is not interpreted (incorrectly) as a type that takes two
type arguments.
With this statement in scope, we can treat appropriate tree
expressions as though they were regular arrays or dictionaries:
T = tNode(tEmpty,("alpha","one"),tEmpty) assert "one" ^= T["alpha"]. U = T["beta"->"two"]. -- Add in "beta" assert "one" ^= U["alpha"].
The implementation statement relies on another feature of Star’s
type system – we need to constrain the implementation of indexed to a
certain subset of possible instances of tree types – namely, where
the element type of the tree is a pair – a two-tuple – and
secondly we require that the first element of the pair is comparable
– i.e., it has the order
contract defined for it.
This is captured in the contract clause of the implementation statement:
implementation all k,v ~~ order[k], equality[k] |: indexed[tree[(k,v)]->>k,v] => ...
This implementation contract qualifier is fairly long, and the type constraints are fairly complex; but it is exquisitely targeted at precisely the right kind of tree without us having to make any unnecessary assumptions.26