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.