Type system features

Subtyping and open data types

One interesting feature of type systems is extensibility; we have the typical object-oriented inheritance, but this is actually too narrow for a proper type system. We instead have the notion of an extended conversion, a function from -> to. Useful examples start from integer conversions, but the most interesting example is adding more constructors to a datatype; A | B is a subtype of A | B | C. We can also do it with product types, by removing elements; (A,B,C) is a subtype of (A,B) is a subtype of A. It makes more sense with labels and records though; {foo: A, bar: B} is a subtype of {foo: A}. This is the closest it gets to inheritance in a type system. Implementations are few, unfortunately; it's primarily Stephen Dolan's work on BRICK (blog archived) and MLSub. BRICK is notable for supporting equirecursive and regular types, so that records do not need a newtype to destructure or bind, similar to dynamically typed languages such as Python, and for compiling to LLVM (no GC, unfortunately). MLSub is just a boring extension with lots of proofs of correctness in the thesis and the coined terms of "biunification" and "bisubstitution". He basically tries to convince you that his subtyping algorithm is almost as simple to implement as Hindley-Milner; which honestly I agree with.

The most interesting part of subtyping is that it explicitly exposes the idea of polarization or duality; for example a function arrow (A -> B) is contravariant in A and covariant in B. When we type check we can divide the type variables into two classes: the pos-variables (lower bounds) and the neg-variables (upper bounds). In fact we usually need both; for mutable variables, arrays, etc. we need both in and out parameters (what can be stored vs what can be retrieved). For example the parameter type for a function that accepts a mutable array of Ints and only reads from it will be MutArray[store=\bot, retrieve=Int], where the store is a lower bound and retrieve is an upper bound.

Dependent types

Once you have subtyping, what point is there in distinguishing values and types? Letting them be used in place almost interchangeably requires some complicated compilation tricks, and an interactive interpreter, but Idris has shown that it works reasonably well in a practical programming language. But dependent types can be extended further.

Insanely dependent types let you define dependent pairs (Σ A (B a), Idris term a ** B a) using a dependent product (Π, (a : A) -> B a). There's some trickery involved in the implementation, see the source for details. The short answer is you need extra scope to reference all the values, and a careful evaluation strategy to avoid infinite loops. The related idea of circular type signatures allows indexing datatypes by values of the same datatype; for example a matrix indexed by a vector, while defining a vector as a single-dimension matrix of length n. (Their notion of matrix is n-dimensional so really it's a tensor). Also interesting from that reddit thread is the idea of making values (terms) a subtype/instance of their type, so for example 1 is a subtype of Integer.

Richard Eisenberg is working on adding them to Haskell, although only the normal form of dependent types.

Linear Types

We could borrow type constructors from Girard's logic: ! and ?, respectively weakening a type to be usable more than once and to not be used at all. There remains the linear arrow ⊸. The usual intuitionistic arrow A -> B then desugars as !A ⊸ B. But this cannot be the final answer, because in IL we decompose A -> B as ¬(A & ¬B); functions do not really exist. Following this paper it seems like it makes more sense to just add multiplicities to the constructors, 0 1 and ω for erasable, linear, and ordinary types respectively. A note here mentions extending ω to having multiple types.

We could also use monads or their more general cousins of Arrows, but why?

Tweag says they're adding them to GHC. although it's hard to say.

Higher-order Types

This paper seems interesting and useful, shouldn't be too hard to add.

Extended type classes

Haskell's type classes have been wildly successful; from an implementation perspective, they amount to adding a constraint-solving engine that discovers and writes in new terms. But I think type classes should be able to add new type information too; unfortunately my efforts in that direction have been unsuccessful so far. It seems like a simple idea though; the set of type class instances in scope is fixed, so if only one instance unifies with the types in scope then it must be the instance to use (otherwise the term must be resolved elsewhere). This is to be distinguished from GHC's current implementation, which has a more restrictive condition requiring matching instead of unification, where matching is defined to add no new information. The question is how to propagate the information from unification in the constraint solver back to the type checker at large; I don't really know enough GHC internals to diagnose the errors in the test suite I ran into.

Type-directed name resolution

One of the most annoying parts of Haskell is that record constructor names must be globally unique since they count as functions. This has been worked on here, but the problem also shows up with type classes (particularly RebindableSyntax) and just in general with similarly-named or similarly-performing functions. What would be ideal IMO is if Haskell supported ad-hoc overloading, so you could just use the name as many times as you wanted and the compiler disambiguated by type. This would also get rid of the 'import Data.Map as M, Data.Set as S' boilerplate. But this would require intermingling the renaming and type-checking phases of GHC, so unlikely to happen.

Scope and closures

In functional programming, values are bound to names. But how are names resolved? The main strategies are lexical scope and dynamic scope. Stallman writes some sections on why Emacs Lisp has dynamic scope (now extended to support lexical scope as well). But of course the two strategies are not mutually incompatible; Vesta supports both dynamic and static scoping, with dynamic as the fallback for static. (PDF page 27)  Dynamic scoping is limited to function blocks with ... in the argument list, but at least it's there. Such a feature would be quite useful in Nixpkgs, where packages are repeated twice, first in the formal parameters and second in the actual dependencies, although a version of that syntax was considered and rejected due to being too slow to execute. Vesta and Nix share much in common though; Vesta's runtool is very similar to Nix's derivation, although Nix uses cryptographic hashes and Vesta uses virtual filesystems.

In more formal terms, we may classify scoping as resolving a name along two dimensions, its semantically enclosing environment (stack frames or dynamic scope), and its syntactically enclosing environment, its AST tree or lexical scope. A filtering function selects from the possible environments and can produce an error or the proper resolution of the name.

Despite the name, dynamic scoping is not incompatible with static typing; a syntactic analysis of which names resolve where is easy, and whatever names remain unresolved can be resolved dynamically.

But the question of how environments/scopes are implemented is not trivial; a paper I read but lost lists many strategies, with choices such as heap-allocated vs stack-allocated, callee-saved vs caller-saved, and ordering of the frame layout. Given the choices, it seems foolish to lock oneself into a particular strategy, at least at a low level.

A new build system

A survey of build systems, and their advantages:

• Make - installed everywhere
• Ninja - portable format
• Shake - parallelism, unchanging files, monadic dependencies
• Pluto - dynamic dependencies
• Tup - fast rebuilds with a filesystem monitor
• Nix - configuration management, isolated builds

There are no easily found build systems that combine all these advantages. Why not? Probably due to the difficulty of switching projects over to new build systems; most people are happy to let sleeping dogs lie, even if in this case they are really hissing snakes that are still biting and constricting developers.

With no existing build system, the solution is to write a new build system. Relevant xkcd:

But the problem is in fact that there is no standard for build systems, just people (companies) doing whatever they feel like. When a committee comes along, develops USB-C, Unicode, etc., in practice it seems that everyone does end up switching. In software, there's an even stronger standardization process: the best open-source implementation usually ends up becoming the de-facto standard, just because everyone else is too lazy or too stupid to reimplement it. Look at LAMP and its history, or more recently Wordpress.


The closest candidate to a de-facto standard for build systems is Make; it has a large user community. But it's missing all the features of the other systems. Can we extend make? Probably not, look at the source, e.g. the dependencies file and main.c and job.c. It's heavily process-based and GNU-centric, the deferred string processing and loading of commands makes everything really slow, and then of course it's in C, which isn't exactly my language of choice. Also it doesn't support parallelism on Windows (maybe?).  OTOH a new implementation maintaining backwards compatibility with make is definitely possible - for example Mozilla has been using PyMake since 2011. Python has been much more successful as a scripting language than GNU Make's built in scripting language of Guile. And porting even a large project isn't that hard, the Tup guy got halfway there already. The hard part is changing over tooling / automation / infrastructure which assumes the use of Make. But as Tup mentions, make is flawed in the way it's most commonly used (overly recursive, incomplete DAG) and also slow because of how it processes files. And it doesn't use a database, all the cool build systems have a database. So all in all, Make is dead for all standards-making purposes; nobody uses it anymore in their new projects, except GNU. And autoconf can generate config files, so there's no need to replace the whole GNU toolchain entirely. Just replacing automake should be sufficient.

Requirements for a new tool in priority order, from 2007:

1. Dependency Management (we have many many libraries)
1. Search Paths 
2. Variants
2. Maintainability
3. Cost of training for day-to-day tasks (40+ developers)
4. Portability (but Linux is a must)
1. Windows, MSYS
5. Speed (A distant fifth; anything would be better than recursive make.)

But of course everyone has their own priorities. The only real priority is avoiding yet another Make DSL.

Metropolis (2001) Review

An excellent example of programming gone wrong, with detailed visuals.

General takeaways:

• Don't store all your data in a single giant tower blocking out the sun
• The most interesting details are buried at the lowest level
• Robots aren't good for much more than handjobs

Specific takeaways: Tima reversed is "Am I T?". The answer is no.

Tools for fools

In project management there's this idea of "fast, good, cheap; pick two":
https://en.wikipedia.org/wiki/Project_management_triangle

But project management triangles like these, for software, are almost always a lie; what works is requirements planning. So I'll list the requirements for a make-like tool:

• sandboxed / traced model of task execution, capturing dependencies (file I/O, subprocess creation, etc.)
• database (store) of recorded execution traces for each task
• unique stable identifiers for tasks, so you can build subsets of them and modify the task graph from the command line (like --touch and make a.o b.o)
• scheduler, buffering up file changes etc. and deciding which tasks to run when (ideally with the usual enhancements: multicore/multithreaded, perhaps distributed across a build farm)

I think that's as far as I can go here; the requirements are pretty generic. But in a bigger organization like Google or whatever it makes sense to encode the knowledge as software so it can be shared as quickly and easily as possible.