Checking for Uninhabitable Types #631

Closed
DavePearce opened this Issue Apr 21, 2016 · 6 comments

Projects

None yet

2 participants

@DavePearce
Member
DavePearce commented Apr 21, 2016 edited

At the moment, the Whiley compiler does not really check for uninhabited types. For example, these types should generate a syntax error:

type Invisible is Invisible | Invisible

We say that the above type is not contractive. Likewise, the following one is uninhabited:

type InfList is { InfList next, int data }

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

The checks for these need to be added at some point, so the compiler at least produces a warning.

@richdougherty has been working on this. See #406 for some more discussion.

@richdougherty
Contributor

I think I've got it working now. The original algorithm I wrote up had a bug. I needed to be more careful about inhabitation for negations.

The inhabitation information for negations is imprecise. Sometimes we will get more precise information about their inhabitation after more simplifications have occurred or after any cyclic uninhabited types have been pruned. However, if we have already labeled our negations with imprecise inhabitation information, then this imprecise information may prevent more precise information from flowing through the type graph.

Here's an example of a type that has this problem:

X<(!(!X|!Y))[]+> where Y is inhabited and X ≤ Y.

Since !Y ≤ !X we can simplify the union to get:

X<!(!X))[]+>

Then we can further reduce this to:

X<X[]+>

Which is uninhabited, so we can convert it to void. However… by this time in the simplification algorithm we may have marked X as inhabited because we incorrectly assumed at an earlier point that !(!X|!Y)) is inhabited (an assumption we made because Y is inhabited).

My "solution" at the moment is to run multiple simplifications, with fresh inhabitation labels for each run, until both the simplifications and the inhabitation labels reach a fixpoint. This means more precise inhabitation information has a chance to flow through once more simplifications have occured.

A nicer way to implement this might be to have more labels for inhabitation so we can more accurately track our knowledge about inhabitation. Then we could label states for which we have uncertain knowledge (such as !(!X|!Y))). For states where all inhabitation is certain we could finish simplification quickly. If there is uncertain inhabitation we could run until the simplification and inhabitation labels both reach a fixpoint.

Anyway, here is my progress at the moment. All tests pass, including the test from #406. It should be finished after I clear out the debugging code, unless we decide the implementation needs to be rethought or tidied up.

develop...richdougherty:bug/406-intersect-uninhabited

@richdougherty
Contributor
@richdougherty richdougherty added a commit to richdougherty/WhileyCompiler that referenced this issue Apr 24, 2016
@richdougherty richdougherty Prune some uninhabitable types
Modify the simplification algorithm so that it propagates
inhabitation information through compound types like arrays,
unions and negation. This allows some uninhabitable types to
be reduced to void and pruned from the type.

Fixes #631, fixes #406.
33318ae
@richdougherty
Contributor

Pull request submitted: #640.

I tried the "nicer" way, but it wasn't much nicer. Even with more types of inhabitation labels you still need to check that they reach their fixpoint, so it's not really faster or better than just clearing the labels before each simplification. So I just stuck with the existing way I'd written it.

@richdougherty richdougherty added a commit to richdougherty/WhileyCompiler that referenced this issue Apr 25, 2016
@richdougherty richdougherty Prune some uninhabitable types
Modify the simplification algorithm so that it propagates
inhabitation information through compound types like arrays,
unions and negation. This allows some uninhabitable types to
be reduced to void and pruned from the type.

Fixes #631, fixes #406.
f490c1e
@DavePearce DavePearce closed this in #640 Apr 25, 2016
@DavePearce
Member

Nice work @richdougherty

@DavePearce
Member

I will have a think about what's the best algorithm for doing this. I'm wondering whether we need a fixpoint computation or not ...

@richdougherty
Contributor

Great! I'd be interested in discussing improvements. I feel there's the potential to find something better and more elegant, but I'm not sure what that would be.

@DavePearce DavePearce modified the milestone: v0.3.40 May 27, 2016
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment