Articles

Contractive and Uninhabited Types in Whiley

An interesting feature of Whiley is that it supports true recursive types.  These are surprisingly tricky to get right, and recently we came across some interesting examples that the Whiley compiler should (but doesn’t) check for.

Recursive Types

The following illustrates the syntax for recursive types in Whiley:

type Link is {any data, LinkedList next}
type LinkedList is null | Link

The type {any data, LinkedList next} indicates a record with two fields data and next, whilst null | Link indicates a union of null and Link. So, a LinkedList is either null or a record of type {any data, LinkedList next}. A simple function operating over LinkedLists is given as follows:

function length(LinkedList list) -> int:
    //
    if l is null:
        return 0
    else:
        return 1 + length(list.next)

This returns the number of links in the list. The runtime type test operator, is, distinguishes the two cases. Since Whiley employs flow typing, variable list is automatically retyped to {any data, LinkedList next} on the false branch.

Subtyping

With this in mind, let us now think about subtyping between recursive types in Whiley:

// A linked list with at least one link
type NonEmptyList is {any data, LinkedList next}

// A linked list containing integer data
type IntList is {int data, IntList next}

Both of the above types are implicit subtypes of LinkedList} Thus, for example, any variable of type NonEmptyList or IntList can be passed into the function length().

Contractive or Uninhabitable?

The Whiley Compiler should accept the above recursive types without trouble. However, it is possible to write recursive types which should be rejected by the compiler. For example:

type Invisible is Invisible | Invisible

This type does not correspond to any possible runtime value in Whiley (i.e. is uninhabited) and, hence, the compiler should report a syntax error here. Likewise, consider another example:

type InfList is { InfList next, int data }

function get(InfList l) -> (InfList r, int d):
   return l.next, l.data

In languages with lazy evaluation (like Haskell) such a type would be pretty reasonable. However, in Whiley, all values are trees of finite height — so it is physically impossible construct an value of type InfList. So, the compiler should report an error in such case.

Conclusion

Recursive types are pretty tricky to implement and get right.  The implementation in the Whiley compiler is now almost four years old, and it generally works pretty well.  But, the compiler isn’t currently checking for types which are uninhabitable (see issue #631 raised for this).  Still work to do then …

2 comments to Contractive and Uninhabited Types in Whiley

  • MarcoServetto

    Hi Dave, Not sure you should check for Uninhabitable types,
    I have the feeling that they can be needed in conjunction with genericity (not sure how you do that in whiley),
    for example your infinite list is a generic instantiation of a reasonable type
    type StuffAndMore is {T stuff, int more}

    Ciao!

  • Hi Marco,

    Well, what you’re saying is that we need to think carefully about how to check for uninhabited types in the presence of generics. That is a fair point actually, and something I hadn’t considered. But it doesn’t mean we shouldn’t check them in general. It could be, for example, that we just produce a warning, etc.

Leave a Reply

 

 

 

You can use these HTML tags

<a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>