Bad error message for null annotation

[kaeluka]

class Main {
  def main() : void {
    null;
    ()
  }
}

yields the error message:

encorec: I don't know how to translate null type to pony.c

[kaeluka]

The message is now: encorec: Don't know type of 'null'. Please annotate: 'null : someType'.

[EliasC]

I have a fix that should prevent this from happening all together! Will create PR tomorrow.

[kaeluka]

What do you mean prevent it? Do you mean to make type inference stronger?

[EliasC]

Slightly stronger, but first and foremost it will catch the error during typechecking instead of crashing the backend.

[kaeluka]

Great!

[kaeluka]

I wanted to close the PR #262, but closed this instead. Reopening.

[sophiaIC]

I thought you were at dinner?

Sophia

On 21 Oct 2015, at 18:41, Stephan Brandauer [email protected] wrote:

I wanted to close the PR #262 #262, but closed this instead. Reopening.

—
Reply to this email directly or view it on GitHub #256 (comment).

[kaeluka]

No, I'm staying home with Kim :)

See you tomorrow!

[sophiaIC]

The famous Kim. Please greet her from me

  Sophia

———•••———
Sent from mobile phone, hence succinct

On 21 Oct 2015, at 19:46, Stephan Brandauer <[email protected]mailto:[email protected]> wrote:

No, I'm staying home with Kim :)

See you tomorrow!

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/256#issuecomment-149974657.

[albertnetymk]

The program from OP doesn't compile using master. Any particular reason why null is not allowed in the middle of a sequence of expressions? I thought translating null without particular type in Encore to NULL would suffice.

[EliasC]

@albertnetymk: I agree that we could translate it to NULL, especially since the value isn't used, but the motivation for not doing so is that I'm trying to avoid leaking the null type to the backend. Translating the null type to (for example) void* would mean that potential bugs where the correct type is not inferred for null could go by unnoticed. Right now, the compiler crashes if the null type reaches the backend. We require annotating null when the type cannot be inferred (for example in let x = null in ...), so it's not that much of a stretch to require it even when the value isn't being used.

When (if) we get a common super type for all classes, we could "infer" that type for free occurrences null.

[albertnetymk]

Translating the null type to (for example) void* would mean that potential bugs where the correct type is not inferred for null could go by unnoticed.

Could you give me an example on what kind of bugs you are referring to here? I doubt there’s any.

We require annotating null when the type cannot be inferred (for example in let x = null in ...), so it's not that much of a stretch to require it even when the value isn't being used.

I see failing-compiling of the below program as incompetent inference algorithm. There’s no hard reasons to disallow this, isn’t it?

class Foo
  def f(x:Foo) :void{
    ()
  }

class Main
  def main() : void
    let
      x = null
    in {
      (new Foo).f(x);
    }

[EliasC]

Could you give me an example on what kind of bugs you are referring to here? I doubt there’s any.

The kind of bugs we would see are things like

void *x = NULL; // Should have been inferred as a enc__passive_Foo*
foo(x->f); // Error from dereferencing a void pointer.

I see failing-compiling of the below program as incompetent inference algorithm.

Well, we don't really do any non-local type inference, so I would say the algorithm is non-existing rather than incompetent (still, we infer more types than say C or Java).

There’s no hard reasons to disallow this, isn’t it?

Feel free to implement it if you have the time! François Pottier's PhD thesis could be a good place to start reading :)

[albertnetymk]

What would be the Encore code for below?

void *x = NULL; // Should have been inferred as a enc__passive_Foo*
foo(x->f); // Error from dereferencing a void pointer.

Wouldn’t this be caught by clang immediately?

Currently, since most type annotations are required, only local inference is needed, I believe. Getting back to my original question: there’s no hard reasons why both programs (the one from OP, and the one I posted) should not compile, right?

[EliasC]

What would be the Encore code for below?

let x = null : Foo in
  foo(x.f)

I'm not saying we do have this bug currently, I'm just saying what kind of bugs we could be seeing if we allowed the null type to leak to the backend. I'd rather abort early than hope that I will understand the cause of the error given by clang if the bug should happen.

Wouldn’t this be caught by clang immediately?

Absolutely, but we don't want to rely on the errors and warnings given by clang! In my opinion, the encore compiler has a bug whenever it produces C code that does not compile without warnings.

there’s no hard reasons why both programs (the one from OP, and the one I posted) should not compile

The "hard" reason is that we don't have an encore type to give to null, and thereby x.

In the example from OP, we could give it any type since we're not reading the value, but this would be a special case in our type checking algorithm as we normally do require annotations on null when the type cannot be inferred locally.

In your example, we would need to look at how x is used (i.e. non-local reasoning) in order to give it a proper type (Foo). If we reasoned that we don't dereference the value in the example and could thus give it an encore type that translated into void*, the program would suddenly stop compiling if we added the line x.f(), as f would not be in the interface of this type.

Sure, type inference is to a large extent a solved problem, even with the presence of subtyping (see my link above), but that does not make it trivial to implement. Someone would still need to put in the hours to make it work. In my opinion, the type annotations right now are few enough to not be in the way, and if the only thing we're looking to gain is that we could save some annotations of null, I'd rather spend my time on something more useful.

I was serious when I said that you are free to implement it if you have the time, but I'd rather see null go from the language completely! We have Maybe types, so why bother with null?