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):

  1. Dimensional refinements - typechecking the dimensionality of lists and tensors

  2. Effect handling - dealing with impure effects such as IO, exception and non-determinism

  3. Constraints and contracts - specifying relationships between input data and output data

  4. Sum types - how can the notion of sum types, a powerful way to describe grammars, be extended across languages?

  5. Extensible records - adding fields, making them optional, and joining product and sum types

  6. Interactive and literate - asynchronous streaming to make daemons and guis

  7. Types as terms in controlled vocabulary - the next level