How programmers view type systems depends on their language background.
C` programmers see type systems as an inconvenient requirement for reliable
design. Python programmers consider types a nuisance that dynamic program frees
them from. Neither group is entirely happy with their situation: `C
programmers want type inference (e.g., through auto) and Python programmers
want the reliability of type checking (e.g., gradual typing with mypy).
Haskell programmers, on the other hand, see types as the structural backbone
and reliable documentation of a program. Where an object oriented programmer
might begin designing their program by laying out the class hierarchy, a
typed-functional programmer would begin by defining data types and function
signatures. The Haskell programmer no more wants to be freed of the tedium of
type annotations than the Java programmer wants to freed of tedium of designing
class hierarchies.
morloc is a typed functional programming language, like Haskell, where
program design consists of specifying data types and how they can be
transformed by functions. If you know the type signature of a function, you
know how to confidently use the function; the particular implementation of the
function is not often of great interest. Whereas dynamic programmers enjoy
being freed of the tedium of writing type annotations, strongly typed
functional programmers would like to be freed of the tedium of writing function
implementations. morloc is intended to allow this. Atomic functionality can
be imported from anywhere, understood within the morloc type framework, and
freely composed to build more complex programs.
The type signature in morloc is expected to specify what a function does well
enough that little further documentation is needed. Achieving this goal
requires that the signature 1) be expressive enough to describe the function
and 2) be succinct enough to be easily understood by a human. This is a
challenging goal since the two concerns, expressiveness and succinctness, are
often at odds. The balance between these two concerns, expressiveness and
succinctness, will be a reoccurring theme in future blog posts.
This post is the first in a series that is intended to outline the necessary
elements of the morloc type system and explore their syntax, semantics, and
implementation. Below is an outline of elements I intend to cover (as I post
these blogs I will update links):
-
Dimensional refinements - typechecking the dimensionality of lists and tensors
-
Effect handling - dealing with impure effects such as IO, exception and non-determinism
-
Constraints and contracts - specifying relationships between input data and output data
-
Sum types - how can the notion of sum types, a powerful way to describe grammars, be extended across languages?
-
Extensible records - adding fields, making them optional, and joining product and sum types
-
Interactive and literate - asynchronous streaming to make daemons and guis
-
Types as terms in controlled vocabulary - the next level