compile-time nil testing

[blubb]

Hello,

I have recently heard about Cobra and was delighted that there was a language with support for nilable and non-nilable types. However, it does not perform as I expected it to: I can write code that uses only non-nilable types, does not use any casts, compiles without warnings and still throws AssertException at runtime:

Code: Select all

class Works

   var _name as String

   cue init
      base.init
      _name = "all fine here"
      
   get name from var

class Oops
   
   var _name as String
   
   get name from var
   
   cue init
      base.init      

class MainClass

   def main
      w = Works()
      s1 as String = w.name
      print s1
   
      o = Oops()
      s2 as String = o.name
      print s2


I would expect the above code to fail at compile-time, the reason being that the String var _name was not assigned a non-nil value after its constructor terminated.

Any comments, explanations?

Kind regards,

blubb

[Charles]

Cobra does not have thorough enough code flow + data flow analysis at compile time to cover all cases. I think, in more complex initializers, it may not be able to refrain from giving a false error message (without further enhancements to the flow analysis).

The fact that it asserts at run-time is still a benefit however, triggered by the type of Oops._name being "String" rather than "String?". But yes, you have to wait til run-time to discover the error and compile-time is preferable.

I'm willing to attempt adding such a check after the next release.

[Charles]

I forgot to ask: How did you hear about Cobra?

Thanks.

[blubb]

Fair enough. I can see the benefit of a runtime check at at assign-time instead of usage-time and i agree that it is already an improvement over the status quo. I am however not convinced that it is a good idea to have "a little more" compile-time checks. If the documentation says the language has compile-time nil-checks, I expect the type system to always prevent me from assigning a nil value to a non-nilable type, except when I force it to let me through a cast. After all, it doesn't let me assign a house object to a Dog variable "sometimes"

IMO, there are only two ways to satisfy the programmer:

• view non-nilable types as actual types. in other words, have the type system verify their correctness at compile-time, and do not let doubtful code compile. This has the disadvantage, that the programmer will have to provide the type system with enough information to support its decision-making process. On the other side, the disadvantage is an actual advantage: It is crystal clear to the programmer what code could actually be verified by the language and where he is on his own. However, a pretty powerful flow analysis is required for this approach, otherwise there is too much noise in the code. I have seen impressing code analysis and non-nilable types in Spec# (http://research.microsoft.com/en-us/projects/specsharp/).
  
  however, there also arises the question what to do with cases such as the following:
  
  

  class Oops
  
      var _attr as NonNil
  
      cue init
          base.init
          
          .doSomethingWithName
          
          # attr initialized in constructor, but too late
          _attr = NonNil()
          
      def doSomethingWithName
          # accesses non-initialized attr
          print _attr.name
  
  class NonNil
  
      var _name as String
      
      get name from var
      
      cue init
          base.init
          _name = "non-nil"
          
  class MainClass
  
      def main
          o = Oops()
          print o
  

  
  
  There are ways to solve these problems (I know only the term "raw types"), but these are current research topics and quite a lot of effort for both the type system and the programmer to actually understand it. Therefore if you don't position your language in a formal verification setting, it's probably not worth doing.


• view non-nilable types as an abbreviation of "argument non-nil contracts" , i.e.



t as Type = exp


is semantically equivalent to


temp = exp
assert temp not nil
t as Type? = temp



This has the advantage that the capabilities of non-nil types are perfectly well understood by the programmer, and it is very simple to implement. It will still make debugging a great deal easier since you do not have to trace your code back from the actual violating usage to the place where you wrongly assigned it to a var that should never have contained a nil in the first place. Personally I favour this approach over both the current situation and the approach described above for its sheer simplicity and consistency.

PS: I found Cobra via Wikipedia when looking for a language with Python-like syntax that is based on the .NET-framework and has support for both duck- and static typing. Guess I found it

[Charles]

Yeah the Spec# guys have done some interesting work and I've been following that project for awhile. I agree the case where you call out to another method is problematic.

Regarding "t as Type = exp", if you were referring to local code (e.g., statements in a method), I hardly ever write statements like that. Instead I rely on type inference and write:

t = exp

where exp may have a nilable type like "String?" or non-nilable type like "String". Also, if "exp" were a nilable type, but I wanted to make sure it was non-nilable at run-time, because I was expecting that, then I can write:

t = exp to !

which will throw an assertion if "exp" returns "nil".

Or perhaps you were saying that non-nil should only apply to method arguments and not elsewhere.

When writing code in Cobra, I'm reasonably happy with the status quo save for a few places where better flow analysis would improve things. I would be interested to know if, over time, you find Cobra's current approach to non-nilable useful in practice and if there are other cases in need of improvement.