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
Here's the simplest data struct possible, a stateless struct to represent nothingness. It's analogous to Java's
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
Sizeablehas 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
Sizeablecan be the argument to two functions,
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
Sizeablein 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
itfor 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
Ato 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
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
sthere is short for "such that."
size'notation here isn't just convention, it's formally significant. Remember how earlier, I said that the notation assumes an
itargument 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
Sizeablesuch that invoking
popimplies 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
sizemethod, 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.