A Fine Language

The main goal of Fine is to explore what a world without function extensionality would be like. I've written before that basic type theories usually leave open the question of whether two functions with different implementations but the same behavior are in fact equal. For example, the functions λ n. n and λ n. n + 0 cannot be proven equal in Coq, even though they produce equal outputs for equal inputs.

Usually, type theorists try to develop type theories where it is in fact possible to prove such functions equal. This means adding new constructors for proofs, so that you can build proofs of function equality that previously weren't available. In Fine, I want to take the opposite tack: add new destructors for data, so that previously undistinguishable functions can be told apart.

So the fundamental idea of Fine is that functions are an inductive data type, much like products or sum types or any other thing. This means you can write a program that looks at how a function f is implemented, and do different things depending on the implementation. This makes it possible to distinguish even functions that behave identically.

Since a Fine program may look at a function's implementation, we need a way to represent such an implementation in a way that's easy to reason about. The superficial syntax of most programming languages involves variables, and if you've implemented a functional language, you know that finding a way to represent variables is a classic problem.

Instead of dealing with those choices, Fine took inspiration from a different school of language design: concatenative programming languages. A concatenative language has no notion of variables. The primitive in a concatenative language is the composition of functions, usually implicit whenever two functions are placed one after another. Thus, in Fine the lft function is one of the constructors of a sum type, while fst is one of the destructors of a product. The function fst lft concatenates the two (left to right), producing a function from pairs to sums, with type α × β → α + γ: first fst operates on the input pair, producing a value of type α, and then lft operates on that, producing the left constructor of a sum type.

Since a concatenative language does not require variables, code can be represented as a simple recursive data structure with finitely many constructors (in Fine, there are 11 constructors).

Pattern matching is another feature I did not know how to concisely represent in a data type, especially since pattern matching usually involves binding variables. I instead chose a uniform data representation, where all values are primitives, binary sums, or pairs. These can be nested. For example, the 11 constructors that make up code objects are represented by ten-times-nested binary sums. Because of the uniform data representation, only a few primitives are needed to handle arbitrary code, including functions. With this primitive representations, a function can be represented by a type F defined by F = 7 + 3 (F × F) + Z, where the integers Z are used only to call built-in functions like the arithmetic operators. A “pure” Fine implementation would not have those.

Since a Fine program can operate easily on Fine programs, it ought to be possible to do easy meta-programming in Fine. For example, it ought to be especially easy to do program analysis in Fine, since the program analysis could be written in Fine itself. Similarly, an optimizer could be written in Fine, take Fine programs as input, and produce Fine as output.

A powerful achievement would be to write the Fine evaluator in Fine. The existing Fine primitives are enough to do this, but until I implement some type of recursion it won't be possible. If recursion were possible, a Fine self-evaluator (for a Fine without builtin primitives) would look like this:

eval: test
{ snd
, test
{ [fst snd,[fst fst,snd] eval] eval
, test
{ snd test
, test
{ void
, test
{ [[fst fst,snd] eval,[fst snd,snd] eval]
, test
{ snd fst
, test
{ snd snd
, test
{ [snd,fst] test {[snd,fst] eval,[snd,fst] eval}
, test
{ snd lft
, snd rgt }}}}}}}}}

It's not pretty, but it's quite surprising that it's so short; and of course it could be shorter were it less repetitive.

Fine is missing any facility for recursion. This makes it difficult to write basic list processing functions, and also makes the goal of a short self-evaluator impossible.

There is no type system. Ideally the type system would be sound and total—with some sort of out for the self-evaluator, perhaps.

The uniform data representation requires memorizing the order of constructors and fields. Plus, it is annoying to use anything with more than two constructors or more than two fields, since only binary sums are products have any support. Some superficial overlay upon Fine that added names would be nice. Of course, names take our wonderful concatenative language and add the pesky variable names back in. So names have to be added in a way that they can be easily removed again.

The uniform data representation makes data hiding impossible. Some way of hiding data and its representation is necessary for writing even moderately-sized programs.