Friday, June 28, 2013

When is a new object really a new object?

Since I just brought up object construction, it's worth discussing when a new object is really created, as opposed to when a previous object can be reused. This will also anticipate some of the function resolution requirements, which I'll introduce in a few posts. As usual, I'll lead by example.

First, some data types to work with:

data Red; Green; Blue nicknamed Color
data Colorful(color : Color)
data Box(size : Int)
data Fragile

Hopefully this should be getting familiar by now. We start with three stateless traits, the union of which is nicknamed Color. We then introduce two stateful traits, followed by a third trait to mark fragility. Now let's create some objects:

a = Colorful Box where
    color = Red
    size = 27
b = Fragile b
b2 : Box = b
c = Fragile b
c2 = Fragile b2
d = Colorful c where
    color = Blue

The first assignment just creates a composite object, as I described in the last post. Easy.

The second assignment (the one to b) creates a new object. It has to, because (as I'll elaborate in the upcoming function resolution post) the object's runtime type is maintained even if the object is "upcasted" later, as happens with b2. We need some way of knowing that b is Fragile while a is not, and the easiest (onlyest?) way to do that is by creating a new object.

But Fragile has no state, which means all Fragile objects are identical. In fact, internally, Fragile could be just a metadata marker on the object. That means that when we re-add the Fragile trait in c = Fragile b, we can actually reuse the same b object. This optimization can be done at compile time.

The c2 assignment is also a no-op, but only at runtime. Even though the compile-time type of b2 doesn't include Fragile, at runtime we can see that the b2 object is already Fragile, and so we simply return it.

Contrast that to the d assignment, which also re-sets the state of one of the component traits. In this case, we do need to create a new object in the general case: objects are immutable, so we can't change the state of c, but we definitely need to store the fact that we now have a blue box where we used to have a red one. (If the new color happens to be the same as the old one, we reuse the object in principle; I'm not sure if this check would be cheaper than unconditionally creating a new object.)

Implicit in all of the above is that there is not a way to check for referential equality — that is, that the programmer won't ever care (or know) if the runtime reuses an object. I think this is a good idea even without these optimizations, so I'm going to throw that into the Effes "spec." Truth be told, I've been assuming it all along.

Incidentally, since the compile-time type of c is Fragile Colorful Box, we could have just written d = Colorful c (without the where clause). This would say that we want to change none of the fields, in which case the whole thing is a no-op at compile-time (as c was). If Colorful had more than one field (maybe it has an alpha : Float), we could have used this syntax to change only one of the fields. This would obviously still create a new object.

On the other hand, if we'd written d2 = Colorful c2, then we'd have to provide the field values. c2 has a compile-time type of Fragile Box, and the compiler would require that if we add color to this box, we need to specify which color. The fact that c2 already has a color at runtime is irrelevant; the compiler will require that the program specific values for all Color fields (in this case, just the one), and the runtime will create a new object that overwrites these fields.

Thursday, June 27, 2013

Creating composite objects

Up until now, I've talked mostly about types. In this post, I'm going to take a slight detour and talk about objects. This won't be the most jaw-dropping of posts, but it will be helpful for the discussion on subtypes, which is necessary for talking about function resolution.

I'll start by knocking out two really easy cases: uncomposed types and union types.

data Foo = Foo(foo : Int)
data Bar

a = Foo(123) -- uncomposed type
b : Foo | Bar = Foo(456)

In this example, a has an inferred compile-time type of Foo, and the code creates a new Foo object whose foo value is 123. Yawn. Then, b has an explicit compile-time type of Foo | Bar, and the code again creates a Foo object. Yawn again. But all of a sudden...

c : Foo Bar = Foo(789)

Ah, this is interesting. The object being created is a Foo, and yet it's being assigned to a Foo Bar, which is essentially a subtype of Foo! This would be like a snippet of Java code reading Car c = new Vehicle() (if Car is a subclass of Vehicle). That's not allowed in Java, so why would it be in Effes?

What's really going on in that example is this:

fTmp : Foo = Foo(789)
bTmp : Bar = Bar()
c : Foo Bar = fTmp bTmp

Just as a conjunctive composed type is created by just writing its two component types side-by-side, a composed object is created by writing its two component objects side-by-side. Simple as that!

The original syntax of the c assignment was actually sugar. If the right-hand side of an assignment is of type A, and the left-hand side is of type A B, and B is a type which doesn't require any explicitly-provided state, then an object of type B is assumed. That is, the original c : Foo Bar = Foo(789) was automatically expanded to c : Foo Bar = Foo(789) Bar() because the Bar type doesn't require any explicitly-provided state.

What happens if you do need to add state? You have two options, both analogous to the syntax for constructing uncomposed objects. You can use the parenthetical constructor syntax for each uncomposed object, and just list the objects side-by-side (this is the syntax I've been using in this post so far). You can also use where syntax, listing all of the fields you want to set in the indented field-assignment block. You can prefix any field name with its type to qualify it; this is optional in most cases, but required when field names collide.

data Foo = Foo(foo : Int, fizz : String)
data Bar(bar : Int, fizz : Int)

fooBar1 = Foo(123, "Hello") Bar(456, 789)
fooBar2 = Foo Bar where
    foo = 123 -- could have been 'Foo foo'
    Foo fizz = "Hello"
    bar = 456 -- could have been 'Bar bar'
    Bar fizz = 789

Note that the order of these fields doesn't matter — you can interleave them, whatever. Each field's name unambiguously identifies it, and they all belong to the single type Foo Bar, so there's nothing special about any particular order. That said, it's probably good form to group fields by component type.

I'm considering adding an additional syntax, which really treats Foo Bar as the new, separate type it is:

fooBar3 = (Foo Bar)(foo=123, Foo fizz="Hello",
                    bar=456, Bar fizz=789)

This has a certain symmetric elegance to it, but it's kinda ugly and potentially confusing. I was going to disallow it, but I think I have to let it in because of nicknames. While the example above is ugly, this starts to make sense:

nickname FooBar = Foo Bar
fooBar4 = FooBar(foo=123, Foo fizz="Hello",
                 bar=456, Bar fizz=789)

I suppose I could allow that syntax only if the composite type has been nicknamed (and is being constructed as such), but this feels like it would complicate the language for not much gain. Better to say that the (Foo Bar)(...) syntax is allowed but discouraged. At least, I hope that's better.

Tuesday, June 25, 2013

Sugar and the "data" keyword

In my last post, I discussed the data keyword as sugar for stateful, struct-like traits. This is mostly pure sugar, although it's also the only way to define a stateless, methodless trait (like Nothing). I'd like to justify those decisions, and also introduce two more pieces of sugar.

As I touched on in an earlier post, there is a balance to be had between deep abstractions vs. ease of use. Syntactic sugar, if designed correctly, can help that balance by highlighting certain aspects of an abstraction. This is useful both for the language design, which can now have a high-level abstraction whose concrete implications are clearer; and from an individual program's design, where it's more obvious which part of the abstraction is important for a given type or object.

The data syntax aims to do this by recognizing that a type whose only functions are getters feels different than one with abstract virtual methods. The first is used purely to store state, whereas the latter doesn't even care about state directly — just about behavior. Effes combines both of concepts into traits, so sugar can help clarify which aspect is more important for a a given type. When you want to focus exclusively on the state-storing ability of a trait, data is a better option, and when you need the behavior-defining aspect of a trait, the default syntax is a better (well, only) option.

As for requiring data syntax for stateless, methodless traits, this is partly pragmatics and partially a philosophical consideration. Given that the syntax for an abstract trait is something like this:

Sizeable:
  size : Int

... how would Nothing look with this syntax? It'd probably be something like one of these:

Nothing:
-- rest of your code here, unindented

Nothing -- no colon
-- rest of your code here, unindented

Nothing:
  pass

The first two feel like weird, dangling tokens; I don't like them from an aesthetic perspective. The last one borrows from Python's pass statement, which inserts a runtime no-op. It was designed for exactly the kind of situations Nothing would have using default trait syntax: the language requires something, but you want nothing. I've always thought this was a bit ugly. Within the context of a function, one could just use return instead; and within the context of a class definition, pass suggests that something weird is going on — a methodless, init-less, stateless class is a weird beast. In Effes, such a thing is indeed useful, but it feels very much like a data type; so, rather than introducing new syntax for it, or generalizing the default syntax to allow weird, ambiguous-looking constructs (like the first or second examples above), I just require the data syntax, which does the job just fine.

Finally, as promised, here are two more minor pieces of sugar for the data syntax. Firstly, you can define multiple types on one line, separated by a semicolon. And secondly, you can follow a data definition with "nicknamed foo" to automatically create a nickname for the union of all of the types defined on that data line. So this:

data LT
data GT
data EQ
nickname Comparison = LT | GT | EQ

...can be expressed more succinctly as:

data LT; GT; EQ nicknamed Comparison

Again, this tries to smooth the transition between abstractions and ease of use. One common use case for a type system is to define enum types; a comparison is either less than, greater than, or equal to. In a language like Haskell, these are different constructors of the same type. In Effes, they would be defined as the union type of the three traits, and one would almost definitely want a nickname for that union type. This sugar allows us to emphasize the enum-like characteristics of the union of stateless, methodless traits.

The use case for this sugar is definitely enum-like types, so I'm tempted to declare that the sugar only works if all of the data types are stateless. This feels slightly more hacky, but it's also easier to reverse: generalizing the syntax will be backwards compatible, whereas restricting it (from all data types to just stateless ones) in the future could break code. I don't anticipate that backwards compatibility will be a major problem for Effes, but I think I'll take the safer approach for now, as an exercise in language evolution if nothing else.

Monday, June 24, 2013

Introducing: Effes traits

Over the past few points, I've gone over some of my ideas for data types and assumption-types in Effes. The latter were originally intended to be a generalization of the standard concept of statically-checked types, but in my last post I talked about giving up on that idea. In the post before that, I ended things by saying that I wanted to unify some of my types of types, and I also got into some of the function resolution issues that have come up. In this post, I'll try to unify all of those concepts under a new concept that I'm calling a trait.

Effes' traits are different from normal traits in two important ways. Firstly, they're not just add-ons for fundamental types — they are fundamental types. Secondly, whereas traits in statically compiled languages are usually added to types ("Cars are Resellable"), in Effes they can be added to individual objects ("this Car is Resellable"). This is to encourage a dynamic, composition-focused type system.

Here are some examples of traits, using examples I've shown before. In many cases, the examples are unchanged.

-- abstract trait
Sizeable: -- abstract trait
  size : Int

-- another abstract trait
Stack[A]:
  push A : Stack[A]
  pop : Stack[A]
  head : Possible[A]

-- "class-based" implementation of Sizeable
Stack[A] is Sizeable where
  size = case head of
    Nothing : 0
    _ : 1 + pop

-- "object-based" implementation of Sizeable
QuickSize Stack[A]:
  let s : Int = size -- "size" given by "Stack[A] is Sizeable"
  push _ : QuickSize Stack[A] where
    s' = size + 1
  pop: QuickSize Stack[A] where
    s' = size - 1
  size = s

We start off with two abstract traits, which are similar to interfaces in Java. We then add a "class-based" implementation of Sizeable, which says that anything which is Stack[A] is also Sizeable. This is class-based because it applies to all objects whose type is (or includes, in a composite type) Sizeable. Next, we introduce a (conjunctive) composite type QuickSize Stack[A] that provides an O(1) implementation of size

My previous posts had a data type, but I'm now unifying those with traits. This declaration is still legal:

data One[A] = value : A

... but it is now just sugar for a stateful trait:

One[A]:
  let value : A
  value : A = value

Fields in a stateful trait are private to the scope that declared them ("QuickSize Stack[A]:" in the first example, "LinkedNode[A]:" in the second), and within that scope, names resolve to fields before functions (that is, a field always hides a function).

While we're the topic of stateful traits' fields, note that they start with the keyword let and may optionally be assigned a value. If they're assigned a value, this value can't be set except within the scope that defined the field; if they're not, this value must be set when the object is created. This can be done using the syntax TypeName(fieldName = value) or TypeName where fieldName = value. In the first form, multiple fields are delimited by commas, and the field name and = operator are optional if there is exactly one field. In the second form, each assignment must be on a new line, indentented relative to the first type name, but the whole thing can be on one line if there is exactly one field. Some examples:

a = One(value=27)
b = One(27)
c = One where
  value = 27
d = One where value = 27
e = Pair(first=23, second=8)
f = Pair where
  first = 23
  second = 8
-- notice that the two "inlined" form are not
-- available to Pair because it has more than
-- one field

The data syntax is mostly just sugar, but it does allow the creation of stateless, methodless traits like data Nothing.

With this new, unified type system, the function resolution rules I described earlier no longer apply. I think a new system shouldn't be hard, but I'll leave that for the next few posts in the interest of keeping this one from snaking off too far.

Wednesday, June 19, 2013

Assumption by any other name make an ass of u and mptions

Until now, I've been using the term "assumption" to describe several ideas: interfaces that define behaviors, stateful traits that include implementations, polymorphism and more. Why haven't I used more standard terminology?

Before I get there, a slight diversion. People who work in Java will sometimes ask a question along the lines of, "I want a Map<K,V> where the keys can be of any type, and the values will depend on the key type." For instance, an Integer key would correspond to a value of MyVal<Integer> (for both gets and puts), a String key would correspond to MyVal<String> values, and so on.

The short answer is that you can't define a Map of that sort in Java. The next question is: why not? Isn't that reasonable? And then the real answer comes in: a type system is just a limited theorem checker, and we've known since Turing that we can't come up with an algorithm that will prove everything you want to prove; so we'll always have to draw a type system's line at some place, and this is where we happened to draw it. If Java allowed for those kinds of types, there'd always a slightly more sophisticated use case that you could ask about and wonder why not.

That got me thinking: what if I designed a type system that, though still limited, had an expanded scope? Most type systems define what types a given object can work with (based on its type). What if I designed one that defined what values an object can work with?

Take a quicksort as an example. The "main" recursive step will look something like:

return (quicksort left) + pivot + (quicksort right)

Well, what happens if you get confused (it's late and you're watching TV while coding) and instead flip the two sides:

return (quicksort right) + pivot + (quicksort left)

My idea was that you could define an assumption called Sortable that would describe which values can be, for instance, pushed into a stack:

Sorted Stack[A] requires A :: Ordered st
    push a requires
        size == 0 or
        a >= pop

Now, in order to push into a Sorted Stack[A], firstly the A type has to have an ordering defined (as it does in any statically typed language that would deal with sorted structures), and secondly, you must have proven in the code that the input is >= the stack's head. For instance:

A :: Ordered ->
badPush(s :: Stack[A], v :: A) :: Sorted Stack[A] st
    push s v -- compilation error!

A :: Ordered ->
tryPush(s :: Stack[A], v :: A) :: Sorted Stack[A] st
    if (size s == 0) or (v >= pop s)
        push s v
    else
        s

In the first example, the code couldn't prove that the assumption required of a Sorted Stack[A] is true, so the code failed to compile. In the second example, it could prove it, and everything's fine.

So, that's why I went with the term "assumption." The idea was that the basic components of a program wouldn't be types, but a bunch of assumptions of a more general nature asserted on objects.

The more I played with it, though, the less promising it looked. All but the most trivial examples became too difficult to express, and I kept needing an "escape hatch" for assumptions that would be cumbersome or impossible to prove in the code. The escape hatch would be in the form of telling the compiler, "I know you can't prove this, but trust me on it." Basically, I felt that the escape hatch would be needed so much that it would become the primary form of typing, in which case the language effectively becomes a dynamically typed language that requires static compilation — the worst of both worlds.

So, I've decided to abandon this effort, and instead focus on a more standard definition of types. I'm going to call these traits, though they're different from traits in some other statically compiled languages in that they're attached to individual objects, and not to other types (as they are in Scala, for instance).

Monday, June 17, 2013

Stateful assumptions

The last major component of Effes' data types is the concept of stateful assumptions. As the last few posts have discussed, assumptions can be used to declare what Java would call an interface — a set of functions. The Stack[A] assumption I've been using as an example was satisfied ("implemented") by a nickname LinkedList[A], which stood in for a union type of (Nothing | Node[A]). Let's add into the mix another assumption, which says that an item has a size.

The Sizeable assumption just declares that something has a size. We can easily declare that being a Stack[A] implies being Sizeable:

Sizeable -> size :: Int

Stack[A] -> Sizeable st
    size = case head of
        Nothing -> 0
        _ -> 1 + (size pop)

This works, but it's O(N). Let's say we want to make this O(1); in this case, we'll need to maintain the size as a piece of state. Here's how we can do it:

QuickSizeable Stack[A] -> Sizeable st
    s :: Int initially (size it)
    pop -> s' = s - 1
    push _ -> s' = s + 1
    size = s

This defines a new assumption, QuickSizeable, and says that being a QuickSizeable Stack[A] implies being Sizeable (which the Stack[A] already was) with a given implementation. Note that QuickSizable Stack[A] is a composite type. Until now, we've seen composite union types; this is our first composite conjunctive type. In this example, implementation says that:

  • When you initially declare a value as being QuickSizeable Stack[A], QuickSizeable will initialize an s :: Int with the size of the Stack[A], however it determines it. At worst, it will be the generic, O(N) implementation.
  • When you pop from the Stack[A], the result's s' is one less than the original s. Remember that the apostrophe means "the un-apostrophe'd name within the context of the result."
  • When you push to the Stack[A], the result's s' is one more than the original.
  • The QuickSizeable Stack[A]'s size method simply returns s

The field s :: Int doesn't belong to either QuickSizeable or Stack[A]; it belongs to the composite type QuickSizeable Stack[A]. This is significant: composite types are "real" types that can define new state or new methods. (We've seen this before, when the LinkedList[A] nickname for the union type Nothing | Node[A] defined implementations of Stack[A] methods.)

This all makes sense, but there's a function resolution problem. Consider the following:

a :: Stack[Foo] = createSomeStack()
b :: QuickSizeable Stack[Foo] = a
c :: Stack[Foo] = b
a.size
b.size
c.size

What happens in each of the three size invocations? a.size is easy: the only method available is the O(N) version that any Stack[A] gets by the first bit of code, above. b.size is also easy: use the O(1) version defined by QuickSizeable Stack[A]. For the third version, we'd like to use the O(1) version — it's more efficient and intuitively feels like polymorphic overriding in OO languages — but we need a rule to allow this. The function resolution rules proposed in the last post are ambiguous.

The solution I have in mind, though I haven't formalized it yet, is that if a type A implies that all As are also B, then A's methods override B's. In this case, QuickSizeable Stack[A] -> Sizeable means that all QuickSizeable Stack[A]s are also Sizeable, so the implementation of size in QuickSizeable Stack[A] overrides the implementation that "belongs" to Stack[A], which we defined above.

What if we now define another sizer:

StupidSizer Stack[A] -> Sizeable st
    size = 1234

What happens with a type StupidSizer QuickSizeble Stack[A]? Does the size method act like a StupidSizer Stack[A] or a QuickSizeable Stack[A]? The call is ambiguous, and is thus disallowed. The type itself is allowed, and you can invoke any unambiguous methods on it; but attempting to invoke ambiguous methods, such as size in this case, will result in a compiler error. To fix it, you must first cast the object to a type with an unambiguous size.

Hm, I think I can unify some of the concepts in the last few posts. Wait for it...

Tuesday, June 11, 2013

Nicknames, function resolution and edge cases

In my first post about the Effes type system, lied a bit in my last post when I said that nicknames are just typing shortcuts. They also provide function resolution rules, in case a data type satisfies assumptions with conflicting methods. For instance, let's say we had the following type and assumption:

data PoppedBalloon (color :: Color) -- or something
Balloon -> :: PoppedBalloon

In the last post, I introduced a Node[A] that satisfies the Stack[A] assumption from a couple posts ago. Now, I also want to say that a Node[A] and Nothing both satisfy the Balloon assumption. Easy enough:

Node[A] -> Balloon st pop _ = PoppedBalloon(Red)
Nothing -> Balloon st pop _ = PoppedBalloon(GhostGray)

This is obviously a strained example, but besides the fact that these implementations are useless, here's the real problem:

foo :: (Nothing | Node[A]) = optionallyGetFoo()
bar = pop foo -- what is bar's type?

In the first line, we try to get a Node[A], but the method's signature tells us we might not be able to (maybe a lookup fails, for instance). If it fails, the method will return a Nothing, and so our foo has to be typed to accept either result value. So far, so good. The question is, what's bar? We can think of foo in two ways:

  • It's either a Node[A], which satisfies Balloon, or it's a Nothing, which also satisfies Balloon. Either way, foo is a Balloon, and pop foo returns a PoppedBalloon
  • It's the union of (Nothing | Node[A]), which satisfies Stack[A], meaning that pop foo returns a (Nothing | Node[A])

I haven't yet nailed down how I want this to work, but my current thinking is that if there is ambiguity, the programmer will have to be explicit about the intent. Something like:

bar1 = pop (foo :: Stack[A]) -- bar1::Stack[A]
bar2 = pop (foo::LinkedList[A]) -- bar2::LinkedList[A]

This has a couple interesting edge cases. Firstly, what happens if a union type (such as LinkedList[A] satisfies an assumption, and one (but not both) of its composite types defines a method that conflicts. For instance, Stack[A] defines a method head. What if you also provided a function on Node[A] alone that conflicts with this? In fact, that method already exists! When we defined the Node[A] data type as:

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

the compiler automatically created two functions:

head Node[A] :: A
next Node[A] :: Nothing | Node[A]

A type foo :: Node[A] cause a conflict with Stack[A], because (as mentioned in the previous post) a Node[A] is a subtype of Nothing | Node[A], which satisfies Stack[A]. The solution here is that Effes will take the most specific function it can; in this case, the one declared to take only a Node[A], that is, the auto-generated getter.

Okay, so foo :: Node[A] means that head foo invokes the getter, while foo :: Nothing | Node[A] means that head foo invokes the Stack[A] method. But what if we additionally define a method that takes Nothing:

head (_ :: Nothing) :: Int  = -1

Now we're back to an ambiguity in the case of foo :: Nothing | Node[A]. The compiler can say that head foo invokes the Stack[A] version of head and thus return a Possible[A]; or that it will switch at runtime between two specific functions, head Node[A] :: A and head Nothing :: Int, and thus return a A | Int. Again, the rule is to favor the specific calls; the compiler will chose the second of those two options.

Finally, let's say we define a method that takes a union type:

head (a :: Nothing | Node[A]) :: (String | Float) =
    case a of
        Nothing -> "I am a fish"
        Node[A] -> 3.14

Now what does head foo return? In this case, it invokes that new method, and thus returns a type of String | Float. This seems a bit inconsistent — aren't I now picking a less specific type? Yes, but it's one that is otherwise impossible to name, so this is the only way I have to invoke it! Whereas before, I could "cast" the Nothing | Node[A] to a LinkedList[A] or even a Stack[A], here I have nothing other than Nothing | Node[A] to cast it to in order to tell the resolution engine to pick this new (and really useless) method. If I want to invoke the two specific methods, I have to manually invoke case:

barUseless = head foo -- bar :: String | Float
barSlightlyLessUseless = case foo of
    Nothing -> head foo -- :: Int
    Node[A] -> head foo -- :: A
-- barSlightlyLessUseless :: Int | A

This is admittedly awkward, but I think it's an edge case that won't come into play very often. I hope.

In summary, functions are resolved in this order:

  1. union types
  2. data types
  3. nicknames
  4. assumptions

That last one may strike you as a bit odd. After an assumption is just a contract, not a specific implementation, right? So far, yes; but in the next post, I'll talk about stateful assumptions that do have implementations.

Monday, June 10, 2013

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.

Thursday, June 6, 2013

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.

Monday, June 3, 2013

Elegance with a balance

In my introduction to Project Effes, I talked a bit about why I want to create a new programming language (tl;dr: because I think it'd be fun). I didn't talk much about what I'd want that language to look like, though. Time to start building.

So to start, let me say that I like languages with an ethos. Haskell is a great example of such a language; it takes just a few core concepts and runs with them in a very elegant way. Where the concepts are different, they're often parallel; you can curry functions, but you can also curry generic types. Pretty cool!

That makes for a beautiful language, but can also make it hard to use. As powerful as the abstractions are, sometimes you want a cigar to just be a cigar. To that end, Haskell does make some concessions in the name of usability. Its do notation makes functional programming seem imperative-ish, and its record syntax is a bit of a hack.

Ruby, on the other hand, feels like it's almost all hack. Lambdas, procs and blocks are kindasorta similar, but they don't quite fit together; it feels like the language didn't know which direction it wanted to go in, so it chose to go in all of them and didn't care that it got pulled apart. The decision to make everything an expression seems principled in a Haskell-type way, except that a lot of those expressions are actually pretty meaningless; a for loop isn't something you'd typically expect to have a value, and it's not clear to me what that value should be, anyway. Other than the ability to say "neat, everything is an expression," what does that actually buy you?

Then there are languages that draw lines in the sand and immediately tip-toe over them. Scala seems to do this by declaring that static functions are Wrong and Can't Be Done In Scala, but then inventing companion objects that let you define singletons with instance methods. Am I crazy, or does that sound very static-function-esq? (Full disclosure: I haven't actually used Scala yet, and I'm sure there are subtle differences between companion objects and static functions; I don't know if they're enough to justify crossing over the philosophical line in the sand. It could also be that I've misinterpreted how strong of a line that is.)

I think it comes down to picking a few abstractions — resisting the temptation to force everything into a single, base concept — and ensuring that they're cohesive and complementary. Features that are similar should be similarly constructed; those that are fundamentally different should be treated as such; and if you have a set of features that are so similar that they're basically a bikeshed problem, just pick a color and go with it. There's a balance to be struck between a Haskell-like level of abstraction and the simplicity of adding a couple more base concepts. Easier said than done.

What I think this means for Effes is a blend of functional and imperative programming styles. I want each one of those components to work well on its own, and I hope they work well together, but I don't want to artificially define either one in terms of the other. A fold and a for loop are different. They feel different, they act different, and they make you think differently. I want each to be a well-formed, first-order construct. Going back to the Haskell case of do notation, rather than having sugar that makes a functional idea look kind of imperative, I'll create a context where the design is imperative, with all of the bells and whistles you'd expect.