Whiley / RFCs

Request for Comment (RFC) proposals for substantial changes to the Whiley language.
3 stars 2 forks source link

Intersection Types (Again) #72

Open DavePearce opened 4 years ago

DavePearce commented 4 years ago

(see also #68)

There is an interesting use case for intersection types arising from real-world library code. Specifically, when I want one type to "inherit" another. For example, we currently have something like this in DOM.wy:

public type Node is &{
    // Identifies what kind of node this i
    int nodeType,
    // Read only property returns node name
    string nodeName,
    ...
}

public type Element is &{
    // Identifies what kind of node this i
    int nodeType,
    // Read only property returns node name
    string nodeName,
    ...
    // Access children
    (Element)[] children,
    ...
}

The intention is that an Element is a Node. One way to support this would using intersection types as follows:

public type Element is &{
    // Access children
    (Element)[] children,
    ...
} & Node

This then (effectively) expands to the original type we had for Element. There are a bunch of obvious and immediate issues:

NOTE: One of the key challenges with intersection types is how they interact with the existing compiler infrastructure.

For example, we need to check whether an intersection is sensible or not (e.g. int&bool is not). Secondly, is the question of how we represent them within the compiler. We could, for example, always expand them to their full (semantic) type. This would work for everything except type variables, but leads to less comprehensible error messages. If we keep them at the semantic level, then we have to think about what happens when we need to e.g. extract a record type using Type.as().