The Delve Type System

(EDIT: bogus logic fixed)

I've been working on the type system for Delve. Here lie the innovative features of the language.

It would be nice to infer the interface of objects, rather than an exact name. This is a much more Smalltalkish approach - an untyped language considers only the interface - the names are irrelevant. Consider this example: ( Warning, I haven't actually tested the examples - it's of little importance to the thought really )

In Haskell, consider the silly ADT

data Tree = Branch { tree :: Tree }

And the Haskell function, bound to the variable f:

let f = \ b -> tree b

Now say we have a Delve object corrosponding to the Tree adt.

(: Tree (Object.new))
(: Tree.tree
   (me ()
       (self)))

See here * for an example which constructs a class using the meta-object model.

And the corresponding Delve function, bound to the variable f:

(: f (fu (b) ((b.tree))))

Now with Haskell, the type checker will say: what is the type of 'tree'? It's 'Tree -> Tree'. Therefore f is of type 'Tree -> Tree'

Now what I'm trying to do with Delve is for Delve to say "b is a new mutant object of which I know nothing. However, it must have the method tree. Therefore, the type of f is 'Mutant with method tree, where tree is of type a -> a'

I think that's pretty cool.

To get this magic to work however, I have given Delve four type constructs. Firstly to explain the key concepts of unification and domination.

In Delve, a type is unified with another type if one type can be used in the place of another. This is a separate notion from equality - equality is a subset of unification.

Domination is where one type, (a type which is more concretely defined) actually replaces the other type in the type system. What seems to the type-checker as an initially polymorphic variable can be dominated into becoming a concrete variable in this manner.

So this is a first attempt at describing the various types.

An object: an object is a value of indisputable type.

For unification with another type, the two types must be objects, the objects must have the same name, and the types of both objects members must all be the same ( recursively considering these types ).

A mutant: a mutant is a value of disputable type.

A mutant can be unified with another mutant if the members of the first mutant are a subset of the second mutant of the same name - in that they set of the names of the first mutant is a subset of the second, all also that each of the intersection of the two sets of members unify.

A mutant also unifies with an object, if the above restrictions are met, but an object will dominate a mutant - that is, an object can be used as a function argument where a mutant is expected, but if an object is assigned to a mutant variable - the variable will become an object.

Mutants which unify can be merged, by safely putting the member types of both mutants into one new mutant. The changes must be propagated to any mutants which unified with the old type.

A function: Delve is strict and does not support curried function application, therefore a function can be simply represented by a list of types.

A function unifies with another function only if each of their types unify.

A polymorph: a polymorph will unify with any type, will be dominated by any other type.

The types arranged then in order of concreteness

Object, Function
Mutant
Polymorph

Now for an example, back back to our function:

(: f (fu (b) ((b.tree))))

The type checker will then type check this as follows – try to imagine you are the Delve type checker – this will be your thought process.

A function will be assigned to the variable f.

f will have the type of this function.

Since this function has one argument, the initial type which we will consider will be “Polymorph called a → Polymorph called b” (to use a Haskelly sort of notification”

So open a new scope, and let b be a new polymorph called a.

Now look at the code for this function.

A member of b, called tree, is being called.

So the type of b might be a “Mutant with with a member tree, where tree is a Polymorph called x”

This is ok, because this new type unifies with b's old type, since everything unifies with a polymorph.

Also, this type dominates b's old type. So b's new type is “Mutant with member tree, where tree is a Polymorph called x”

Tree is called of b, which is a polymoph called x.

So the return type of this function is a polymorph called x.

So the type of this function is 'Mutant with member tree, where tree is a polymorph called x → x'

So the type of f is 'Mutant with member tree, where tree is a polymorph called x → x'

Which is what we want. I think this is cool – but it has some problems. First, the rules for assignment and application will be formalized – this is useful – also it reveals the problems.

Assignment – assignment assigns a result to a variable. Assignment is correct if the type of the result unifies with the type of the variable. The type of the variable is always dominated by the type of the result. This means a polymorphic variable will be erased if say, an object is assigned to its place.

Application – actual arguments are applied to a function. The types of the functions formal arguments have already been decided and are not changed in a global sense.. The types of the actual arguments must unify with the types of the formal arguments. However, if the type of an actual argument dominates a polymorphic type in the formal arguments, all occurrences of the polymorphic type in the resultant type (local to this computation) are changed into the dominating type.

Say for our example, where f is 'Mutant with member tree, where tree is a polymorph called x → x'

If f is applied to a “Mutant with a member tree, where tree is of type Tree”, then locally, the type of f will become “Mutant with a member tree, where tree is of type Tree → Tree”. The result will then be of type “Tree”. However, when f is next used, its type will still be 'Mutant with member tree, where tree is a polymorph called x → x'.

Member lookup – looking up a member of a polymorph dominates the polymorph with a mutant type which possesses this member, and gives the member a new polymorphic type. Looking up a member of a mutant succeeds with the unification of the mutant with a new mutant as before. Looking up the member of an object succeeds if the object has this member. The resultant type, ie, the type of the member lookup, is the type of the member, once the appropriate unification (and perhaps domination ) has been applied.

Function creation – polymorphic arguments are introduced to represent each formal argument. Each formal argument is then dominated by the statements making up the body of the function. The return type is the type of the last statement in the function's body.

Method creation – same as function creation – exception the method imposes domination on the “self” - it can be only be assigned to an object, or within the local scope of that object, where the object unifies with this self.

*Delve has no class macro yet, so here is code which manipulates the meta-object model, allowing for the silly Tree class.

(: Tree (Object.new))
(: Tree.instance_methods (Object.new))
(: Tree.instance_methods.tree
   (me ()
       ((Tree.new))))
(: Tree.new
   (me ()
       ((: instance (Object.new))
        (: instance.class self))))

Either that or just use an object


Hmm, I must write a HTML pretty printer for delve...