A first peek at Effes

I've been playing around in vim with some ideas, and I think I have an idea of how I want Effes to look. Here's a dime tour. It's a bit long, but it should be a pretty quick read.

The basic idea is to have a few basic building blocks:

• functions: objects are data, blah blah, functional programming
• data structs: just structs, no behaviors or anything
• assumptions (better name needed): just about everything else

Assumptions work as types, class interfaces and codified invariants. They can be combined using conjunctions or inclusive disjunctions (ands or ors), and their declarations take the form of "A implies B." Since none of this has been formalized yet, it may be best to show rather than tell.

Here's the simplest data struct possible, a stateless struct to represent nothingness. It's analogous to Java's null, Python's None, Haskell's Nothing, etc.

data Nothing

Not much there. Here's a nickname, which is just an alias for a conjunction or disjunction of assumptions.

nickname Possible[A] = A | Nothing

Note that an alias does not bring any additional type safety, it's just a macro-like shortcut. A method that takes an argument a::Possible[Foo] is identical to one that takes an a::(Foo | Nothing).

Okay, let's introduce an interface-like assumption:

Sizeable -> size :: Int >= 0

Sizeable ->
  it isEmpty = (size = 0)
  it notEmpty = (size > 0)

The first line defines an assumption called Sizeable, and says that anything Sizeable has a method called size that returns a non-negative integer. Read it as "being Sizeable implies that there is a size greater than or equal to 0."

The next block says that anything which is Sizeable can be the argument to two functions, isEmpty or notEmpty. Again, we'd read this as "if something is Sizeable, then (1) you can ask if it's empty and (2) you can ask if it's not empty.  Note that we could have put all three implications about Sizeable in one block, or we could have further split them into three blocks. Assumptions are open-world; anyone can add an implication to any assumption they want.

Syntax note: Whenever we declare a method in the context of an assumption, it's assumed that the first argument to that method is the object for which the assumption holds. If we want to change that behavior, we use the keyword it for that object. This works both for declaring and invoking the method.

Let's define a more interesting assumption.

Stack[A] ->
    push A :: Stack[A]
    pop :: Stack[A]
    head :: Possible[A]
    Sizeable st
        push A -> size' = size + 1
        pop -> size' = size - 1

This defines a generic assumption for a stack. If something is a Stack[A], it implies you can push an A to it (to get another Stack[A] — we're working with immutable types here), or pop the top element, or get the first element if it exists. Note that head uses the Possible[A] nickname. As mentioned above, this could have also been written head :: A | Nothing.

This assumption also states that being a Stack[A] implies being Sizeable. Furthermore, it establishes assumptions about what certain functions imply. When you push onto a stack, the resulting stack has a size that's 1 greater than the original stack; when you pop, the resulting size is 1 less. The keyword st here is short for "such that."

The size' notation here isn't just convention, it's formally significant. Remember how earlier, I said that the notation assumes an it argument when talking within the context of an assumption? When working within the context of an implication, any word that ends in an apostrophe works in the context of that implication. So for instance, the last line could be read as "being a Stack[A] implies being a Sizeable such that invoking pop implies that the resulting object (which we already know is itself a Stack[A]) has a size' equal to the original object's size - 1."

This doesn't provide an implementation for the size method, mind you. What it does do is to provide an invariant that every implementation must hold, and which any user may (formally) depend on. This is by far the sketchiest part of the language in my head, and the most ambitious, so it's still pretty sketchy. But I'll write about some of my ideas in subsequent posts.

In fact, it's not just that the above doesn't provide an implementation for size; it doesn't provide an implementation for Stack[A] at all! We've asserted that being a Stack[A] implies certain things, but we haven't shown how to actually create a Stack[A]. You can think of this as being an interface or pure virtual class. I'll talk about concrete types in the next post.