Data types and satisfying assumptions

In my last post, I talked about Effes' concept of "assumptions," and how they can be used to specify an object's behavior. Like an interface in Java, assumptions just tell you what the behavior is — they don't provide an implementation for it. In this post, I'll introduce the Effes' composite data type and discuss how it can satisfy an assumption.

A data type in Effes is basically what C would call a struct — a composition of values, each with a name. The data type itself has a name, which is strongly type-checked. Here's an example of the simplest data type possible, which is composed of zero values.

data Nothing

Okay, but not very interesting. How about something that can satisfy the a Stack[A] assumption I introduced in the last post? A linked list node is a good place to start.

data Node[A] = head :: A, next :: (Nothing | Node[A])

This is similar to Haskell's data, but with two key differences. First, the equivalent of record notation is required. You can't define a data Node[A] (A, Nothing|Node[A]); each value must be named. Secondly, each data type has exactly one constructor. In Haskell, you can define a type as the union of multiple constructors:

data Maybe a = Nothing | Just a

In Effes, this appears as two completely separate types:

data Nothing ()
data One[A] = value :: A

In the previous post, I mentioned nicknames as a way to alias the conjunction or disjunction of assumptions. Let's provide a nickname for the union of Nothing and Node[A], and then show how this union satisfies the Stack[A] assumption:

nickname LinkedList[A] = Nothing | Node[A]
LinkedList[A] -> Stack[A] st
    push a = Node(head = a, next = it)

    pop Nothing = Nothing
    pop Node = next

    head n = case n of
        Nothing -> Nothing
        n = head n

(Read that second line as "being a LinkedList implies being a Stack, such that...") Here's the first thing to notice: a type which either Nothing or Node[A] can work as a Stack[A]; it doesn't have to be typed as the union Nothing | Node[A]. This reflects the reliance of type composition (for lack of a better word?) in Effes. (This shameless plug for synergistic abilities makes Effes the perfect language for Enterprise 2.0!) In other words, having defined this implication about LinkedList[A] we can now pop a plain Node[A] or a Nothing.

The next thing to notice is that pop and head provide different syntax to express the same concept: "do abc if the input is a foo, or xyz if it's a bar." I'm not sure if I'll keep this duality, though. I'm tempted to get rid of the first form, and require all matching to be done via case. We'll see.

Lastly, pop has a covariant return type. The Stack[A] assumption knows only that pop returns a Stack[A], but the LinkedList[A] nickname knows that its implementation of pop has two code branches, one of which returns Nothing and the other of which returns Node[A]. This means that LinkedList[A]'s pop returns a Nothing | Node[A], which still satisfies the Stack[A] requirement, but is more specific than it.

In the next few posts, I'll talk a bit about function resolution rules and stateful assumptions, which blur the line between data types and assumptions as I've discussed them so far. I'll then talk a bit more about the role of composition in Effes — more of the synergy 2.0 stuff. I tell ya, I'm a few XML docs away from an IPO with this, baby.