The path through language design

Some people ask me about structural subtyping in MotionTypes. If you Google for thoses words, you’ll see a bunch of research papers and not clear-and-simple definition. That’s because structural subtyping is more convenient when you need to write a proof about a specific typing algorithms.

So what’s structural subtyping ?

Structural subtyping means that an object B is a subtype of A (notation B :> A ) iff all fields of A are in B, with same types. In languages such as Java/C++/AS2… subtyping is synonym of inheritance ( B extends A ) or prototyping ( B implements A ). While it’s very easy to check B :> A , you have to encode in your application some strict rules in order to get proper types (you have to think and build an inheritance tree correctly, as part of your application architecture).

With structural subtyping, if you have :

    class Point {
        int x;
        int y;
        void add( Point p )  {
            x += p.x;
            y += p.y;
        }
    }

Then all classes having fields int x, int y and a function void add (Point) are implictly subtypes of Point, and can then be used everywhere the program need a Point : you don’t have to extends Point or create an interface AbstractPoint.

It goes more powerful when used together with type inference. For example let’s see this function :

    function f(o) {
        o.foo(33);
    }

Typing algorithm in compiler can infer about f type that it returns void and that it has one parameter o which is an object with at least a method foo which takes an integer argument and returns whatever. Type inference then can give you a type of f :

    void f ( o : { void foo(int)  } );

And if you have structural subtyping that means that you can apply f on any object have at least a method foo which takes an integer as parameter. I recommend reading the book of Benjamin Pierce Types and Programming Languages if you’re interested in that topic. It bring together good basics about theory, mathematical models and different typing algorithms.