Simplifying (un)contractive and (un)inhabitable types

[DavePearce]

(follows on from #631, #406 and is based on work @richdougherty is doing)

Simplifying recursive types in the presence of uncontractive or otherwise uninhabitable types presents something of a challenge. There are two main phases:

1. Contractivity testing is the process of checking whether a type (or a component thereof) is contractive or not. A type is not contractive, for example, there is a path from a given node back to itself without passing through a concrete constructor (e.g. record type, array type, etc). Non-contractive types should be reported as an error by the compiler.
2. Simplification is the act of applying simple rewrites to reduce the term as much as possible. Ideally, we can implement subtyping just using simplification, where T1 <: T2 becomes T1&!T2 which we try and simplify to void.
3. Inhabitability testing is the process of checking whether a type (or a component thereof) is inhabited or not. A type is not inhabited if, for example, if it only accepts infinite-sized values (e.g. InfList from Checking for Uninhabitable Types #631). At this stage, it's unclear what to do upon detection of an uninhabited type. Ideally, a warning of some sort would be produced. In practice, we may just treat them as void.

We have three steps here and, unfortunately, it seems the latter two may depend on each other:

• Contractivity can be completed prior to simplification and inhabitability checking. This test is done using a graph propagation algorithm (e.g. depth-first search). However, it cannot be implemented (as far as I'm aware) using simplification based on rewrite rules.

• Simplification cannot be completed until non-contractive types are reduced to void. For example, consider this type:

  type InfList is { InfList next, int data }
  type NullInfList is InfList | null
  

  In this case, the type NullInfList should reduce to null. This can only happen after InfList has been identified as non-contractive and, hence, equivalent to void.

• Inhabitability cannot easily be tested before simplifications. The general pattern here is that we have a union between recursive type, and something which appears to be inhabited. For example:

  type Empty is int & !int
  type InfList is { InfList | Empty next }
  

  In this case, Empty should be simplified to void. However, the contractivity test is going to treat Empty as a simple primitive type which seems to be inhabited.

Thus, we can see that we need to iterate these two mechanisms together in unison until a fixpoint is reached.

Functions/Methods

Some types cause a few problems here. In particular, function or method types are interesting because (in some sense) it can make sense for them to be non-contractive. For example, consider this method:

type Func is function() -> Func

This type is inhabited by the following implementation (for example):

function f() -> Func:
   return f

An interesting question here is whether or not such an implementation can ever really be considered as useful ... ?

[richdougherty]

@DavePearce, thanks for the great write up.

I agree that the existing algorithm will be much simpler and clearer if split into separate—but interdependent—simplification and contractivity testing phases. I know that's what you suggested before I made the changes in #631, and I regret that I implemented a single combined phase. I may revert some parts of my change to recover the original simplification algorithm that was there before #631, then create a separate contractivity testing phase.

I think I should also simplify #631's contractivity testing implementation to use fewer labels. The existing implementation uses four different labels for nodes—unlabeled, none, some, all. Yesterday, when we talked, you advocated using simpler binary labels: contractive, non-contractive. Now that I think about it, I think binary labels would work well and would be better. So I'll put that on my todo list too!

Function/method types

Regarding functions types, I think we may be able to deal with them with two rules in our type simplification and contractivity testing. How do the following rules sound? (My thoughts about appropriate rules change daily, but these rules are where I'm at with my thinking right now!)

1. In the simplification phase, have a rule that replaces function types with void if they have one or more void output parameters. We don't care about void input parameters because input parameters are contravariant.
2. In each contractivity testing phase, simply mark function types as contractive. I googled for "contractivity" and found at least one example where function types are defined as contractive (paper), so maybe this is OK!

Examples:

type F is function() -> void // converted to void by simplification rule
type F is function(void) -> () // OK, not converted to void
type F is function() -> F // OK, contractive
type F is function(F) -> () // OK, contractive

Function/method values

The rules above permit function types with void parameters. This may seem a bit paradoxical because what's the use of a function with void parameters? The reason it makes sense is that functions types with void parameters have subtypes with normal, non-void parameters, and those subtypes have values that are normal, useful functions.

However, just because we permit function types with void parameters doesn't mean we should permit function values with void parameters. The lambda void x -> 1 should perhaps be considered illegal, since it cannot be called. We could modify the type checker to forbid function values with void parameters, even though their types are perfectly valid.

[DavePearce]

Hey @richdougherty ... I updated my original discussion to identify three distinct phases, not two as originally stated. This is good .. we are making progress!!!

[DavePearce]

At this stage, I am now going to close this issue. The latest develop snapshot contains the latest iteration of my subtype algorithm, and it is by far the best so far. In addition, the compiler now checks for both non-contractive and empty types and reports errors for them.

[richdougherty]

❤️