Sequent braindump

gistfile1.md

Since I am doing this music thing, it may be a while until I do any leisurely programming again and who knows how my interests will have shifted by then. So I would like to take this time to dump my current vision of Sequent, the encapsulation-free programming environment. First I will give some of my inspirations for the idea. I will then move on to the basic concepts and operation of the environment.

Inspirations

The first inspiration is from Haskell in highly polymorphic code, or if you like, from Coq. For hard programming problems I often write down what I have and what I need. Let's take an example, writing the Monad instance for Cont.

newtype Cont r a = Cont { runCont :: (a -> r) -> r }

instance Monad (Cont r) where
    return x = 

Now, not having the gift of functional intuition, we don't quite know what to do. But the types guide us:

return x = ?
    x :: a
    ? :: Cont r a

We need to return a Cont r a, and the best way we have for getting one is the Cont constructor, so let's give that a try:

return x = Cont ?
    x :: a
    ? :: (a -> r) -> r

Now we have the same information, but we have to return a function. The most general way to make a function is with a lambda, and after introducing this lambda we will have more information to work with:

return x = Cont (\f -> ?)
    x :: a
    f :: a -> r
    ? :: r

Now we have an a, an a -> r, and we need an r, so the path is clear: apply one to the other:

return x = Cont (\f -> f x)

And our function is done. Mind, it is not quite idiomatic Haskell, but for Sequent, as we will see, this is not important, as the task of ever looking at code like this doesn't comes up.

If this style, or at least this level of explicitness, is new to you, a good exercise would be to use it to derive the implementation of bind. Try not to think, make every step as mechanically as possible.

(>>=) :: Cont r a -> (a -> Cont r b) -> Cont r b

You can perhaps see where this is headed. Somewhere near Djinn. All we needed was the signature of these functions and they were already written for us. Sequent attempts to make functions that can be written for you disappear completely. Such cannot be said for functions like sqrt, however, so there is still work to do.

The second inspiration is also from Coq, in a cognitive rather than mechanical way. In Coq you can start a section, and inside that section you can postulate the existence of various objects. Any definitions you make within that section will be under the assumption of the existence of those objects -- in other words, the objects will become parameters to your definition. Usually the postulates are interrelated in some way, which in Haskell would translate to a typeclass constraint. But every function in Haskell has to have a closed type (modulo intensional definitions), so you have to give the constraint in the type of every function you write.

Let's have a concrete example. When I was working on the first version of Life, I was writing the game engine which needed to refer to an Image type. There were a number of ways to implement this concretely (eg. from graphics-drawingcombinators or one of Conal's libraries or diagrams...), and for this portion of the engine we needed to do little with images but translate them and overlay them, so the natural solution was a typeclass.

class Image i where
    overlay :: i -> i -> i
    translate :: Vector2 -> i -> i

In almost every function in this file appeared:

:: (Image i) => ...

And Image was not the only type thus abstracted. My signatures became long and difficult to read, having to refer to a type variable and a constraint when all I meant was an abstract concept of Image.

At this point you may be saying, this is your inspiration for a language? Why not just throw around some syntactic sugar, making it so typeclass constraints can have scopes. But you have to be patient, there is more to this story.

I was in a very aesthetic mood that day, and I abhorred those ugly signatures. So I did something very wrong to make it prettier: I make the code less generic than it could be by fixing the types. I picked a specific Image type to work with, namely, the one from graphics-drawingcombinators. My library just got substantially less flexible by fixing this type. But at least my signatures looked as simple as they were:

 :: Input :~> Image

rather than

 :: (Input input, Image image, SF (~>)) => input ~> image

But all the implementation code stayed the same, only the signatures changed. Hardly anything actually happened in this substantial leap down in genericity -- and if I just wrote some typeclasses, changed the capitalization of some things, and fixed up the signatures, I would be able to regain the genericity. Except for the quantization of the typeclasses, it is an entirely mechanical procedure.

Analogous to what we talked about earlier -- making mechanically implementable functions disappear -- Sequent wants to make these two equivalent notions disappear. Defining a concrete data type and quantifying over its observations are equivalent, or perhaps adjoint -- I don't really know category theory -- except that a concrete data type is much less flexible in the way it can be used because its scope is global (or put another way, it has intensional identity). If we eliminate the global scope, such that every concrete definition is in fact an assumption at its enclosing scope, we can substantially improve the reusability of all code without even having to think about its genericity (with caveats, which Sequent attempts to address). It was this observation which initially led me to start this project.

Sequent's Design

I'd first like to note that Sequent's solution to the above problems in a way that is elegant and the right level of internally powerful is incomplete, and what is there is possibly bad. These are my current thoughts, which have developed quite a bit from my initial conception, and I don't have any reason to believe they won't develop further.

Sequent is not a traditional programming language along two axes, so to give a clear picture of what I am describing I will start by noting these differences.

• Programs are not edited in text files, rather the IDE is an essential part of the system.
• It piggybacks on another language, serving as a code organization language rather than a language in which you write actual content code. I was using Javascript in my prototypes; because Javascript is verbose and ugly we will use a unityped variant of Haskell for this discussion.

The system is organized around snippets, which should be considered analogous to theorems in mathematics. They are self-contained pieces of code with a very sophisticated and descriptive type signature. They should be read like theorems rather than like functions or procedures. For example instead of reading a specification of sqrt like this:

sqrt x gives the square root of a x :: a where a is in class Real.

You should read it like this:

If a is in class Real and x :: a then sqrt x :: a

Or, further still, like this:

If a is in class Real and x :: a then there exists y :: a such that y^2 = x.

Notice that in the last variant, the identifier sqrt does not appear. Sequent does not organize functions by identifier; functions are found and used through their signatures alone. You might consider the above signature as the name of the function, such that the name is computer-comprehensible (and precise enough to be so).

This computer-comprehensibility emerges from a network of human-only-comprehensible concepts connected by theorems. These concepts are the predicates, and they contain the programming power of the system. They are intensionally defined, in other words they have global scope. In the previous section we saw how that can lead to a lack of modularity, but I feel it is justified on the following grounds (however it is a decision that rubs me the wrong way in some respect, so there may be something better lurking): Predicates have no content, the only meaning they have is how they appear in theorems. One man's List is another man's Vector, and we don't want two different concepts that are only similar enough to both be called List to be considered the same by the system. So when you use a predicate, you get an autocomplete dialog helping you choose the correct concept for the word you are using, should there be multiple (predicates can have more documentation associated with them than their name to help you decide).

Also to mitigate the loss of modularity that you might get from predicate-polymorphism (second order logic), arbitrary code-less theorems are permitted, for example:

If x :: List(1) then x :: List(2)

declaring a relationship between the two distinct List concepts, which will be used by the system. This theorem could also have code associated with it describing how to view a List(1) as a List(2), if it is not the identity map.

Note that we may consider (::) as a binary predicate, it needs no special role (perhaps it could use some inference from the target language -- that's a long way off in feature space though). However, it may be beneficial to give it a more central role, so that eg. you can compose types without getting into Prolog-land. I haven't explored this thoroughly.

Some participants in signatures have a runtime representation, and some do not. If they do, the runtime representation should be described by the type/predicate. You might see in the browser:

x :: List    |     x is a List with member functions "length", "head", "tail", ...

And that is the extent of knowledge that the system has about the functions length, head, tail on this sort of List. It is merely documentation at this point.

If they do not, they can be used for code organization. Types are an example of representationless organizational objects. My hope is that every concept in your domain can go with one of these objects, and you use these high level concepts to organize code that talks about objects with a computational representation. That is a fairly lofty goal, because domain concepts are sometimes about a relationship rather than a model. But... we shall see.