Incremental static typechecking

Crystal Contrib
1

Hello,

I am quite a newbie to Crystal. On many aspects, I find that its design is very smart. But one thing really hurts me: its type-checking is not compositional. Let me detail this on the following example:

def demo(c : Class) : Nil
  a = c.new()
  puts("demo on #{a.class}")
  (1..10).each {|x| a.push(x*x)}
  puts(a)
end

demo(Array(Int32))
demo(Array(Float64))

This program is well-typed. But, if we add the following line, it becomes ill-typed.

demo(Array(Bool))

And the type-checker declares an issue in the definition of demo and not on the call with the issue.

4 | (1..10).each {|x| a.push(x*x)}
^
Error: expected argument #1 to ‘Array(Bool)#push’ to be Bool, not Int32

In all other strongly-type language that I know, type interfaces of methods/functions are contracts: their validity is checked on function definitions - and only the type interface is used for typing function calls : this makes type-checking compositional.

This is not the case for Crystal. Type restrictions are not contract: they only restrict call contexts (and they are used as guards for multiple dispatch).

Having a non-compositional type checking has huge consequences: this makes debugging harder, this makes incremental compilation impossible, which has itself other consequences, such as very slow compilation times, and poor interactions with LSP-server.

It seems difficult to make Crystal type-checking compositional without loosing too much expressiveness. For example, on the above example we would need to make demo a generic method over a type T, such that T <= (Int32 | Float64) and c <= Array(T). Including such constraints in the language and its type-checking seems really challenging. Such complex constraints might not be inferred and should be instead provided by programmers.

Moreover, backward compatibility would be broken (which can be mitigated with a flag on the compiler). But, the benefits may worth the price of these difficulties ?

2

I am not sure to understand why you try to push an Int value inside an Array of Bool

But anyway, the raised error by the compiler is quite clear. What do you try to explain ?

3

I am trying to say that, on the contrary to most strongly-typed languages, Crystal type-checker does not check the definitions of methods, but only their call.

As a consequence, this makes debugging harder. Consider this second example, this is only when you decomment line pay(1000) that you find the bug in pay. For a similar example in Java, the compiler would reject pay directly on the definition.

def pay(x : Int32) : Nil
  if x < 0
    bug(x) # not defined will failed !
  end
end
puts("Hello!")
puts("Hey, type hello please :)")
answer : String | Nil = gets
if answer == "hello please :)"
  puts("Congrat, you win 1000$...")
  # pay(1000) # <- decommenting this line will makes the typechecking fail
              # even if the runtime-error is unreachable
end

Other consequences include non-incremental compilation for which there is another thread. My point is that you cannot have incremental compilation without incremental static typechecking. And having incremental typechecking in Crystal is challenging: see my previous example.

Is my point clearer ?

1 Like
4

I got you now thank you. I agree with you, it’s something I find a bit annoying with crystal too

5

Yea, my 2 cents on this is Crystal is somewhat unique in this regard. Types are not (always) required like they are in other strongly-typed languages. E.g. in you example the Class restriction is essentially not doing anything and would be the same as if you didn’t provide it at all. Ultimately this makes the method be duck typed to whatever types support the methods called on the argument.

This provides a lot of flexibility in that you can just write you code and the compiler will figure it out and feel more dynamic, while still preventing you from actually hitting a runtime error like you would in Ruby/Python/PHP.

If you make the method definition like def demo(c : Array(Int32 | Float64).class) : Nil then you’d get:

In test.cr:10:6

 10 | demo(Array(Bool))
           ^
Error: expected argument #1 to 'demo' to be Array(Float64 | Int32).class, not Array(Bool).class

When adding in the other type.

Technically the nature of the language makes this theoretically untrue, like a super contrived/naive example:

struct Int32
  def <(other : Int32)
    return true if self == 1000

    previous_def
  end
end

def pay(x : Int32) : Nil
  if x < 0
    pp "oops"
  end
end

I.e. given you can override the #< method, the compiler just can’t prove that 1000 < 0 at compile time. To me it just shows that static typing can only provide so much safety and isn’t an excuse to just not write tests that would have caught this, and asserted it’s doing what you expect.

1 Like
6

Yes, as far as I understand, Crystal gives this guarantee only for “complete” programs (eg with a “main” code). There is no guarantee on the classes in a well-typed program that you reuse in another context.

Thanks, for this feedback. I did not thought to this kind of typing constraint. Thus, specifying typing contracts for Crystal methods within the current type system might be easier than I initially thought.

On your last remark, what I meant in my comment, was that the runtime-error is unreachable in this particular “complete” program.

Of course, I am happy that the type-checker detects that this call to pay could lead to a runtime-error in some contexts. I would be even happier, if it could give me this information without having to write a program that calls pay.

7

I completely agree. But, strong static typing avoids the pain to write many dummy tests, that just deal with context you do not want to deal with.

For example: when developing untyped Python code (e.g. before gradual typing), you had to write many tests just to compensate the lack of typechecking. And when your code evolved, this was a pain to maintain all these tests, but necessary to keep finding stupid bugs.

In my experience, with a very strongly typed language, you also need to write a lot of tests for debugging while developing. But, after your first version is validated, you can often throw away a lot of very fined-grained tests, and only keep more coarse-grained ones. You know that stupid errors later introduced in your code will be found by the typechecker, and expect that your coarse grain ones are sufficient to cover the other ones.

8

Related: Have I hit compiler bugs? - #25 by ysbaddaden

9

Maybe this is just a misunderstanding about how typing in Crystal works.

Crystal uses strong static typing. But it works as a kind of static duck typing.

The type system does not prevent you from calling a method that is not part of the restricted type’s interface. As long as the actual type implements it, it’s fine.

This concept is pretty unique, and of course it has some downsides. But it’s also really neat. Crystal feels very dynamic because of features like this. And that makes it appealing.

10

The Earth’s ecosystem is vast, and in a zoo you can even see animals like the platypus.

Objective-C

#import <Foundation/Foundation.h>

void pay(int x) {
    if (x < 0) {
        [NSObject bug:x]; // not defined
    }
}

int main() {
    @autoreleasepool {
        NSLog(@"Hello!");
        // pay(1000); // ok
        // pay(-1);   // uncomment to fail at runtime
    }
    return 0;
}

clang demo.m -framework Foundation -o demo

A warning is printed, but it compiles. The crash happens at runtime when calling pay(-1).

Julia

function pay(x::Int)
  if x < 0
    bug(x) # not defined
  end
end

println("Hello!")
# pay(1000) # ok
# pay(-1)   # uncomment to fail at runtime

juila demo.m

I don’t really know my way around the Programming Language Zoo, so I asked AI to give me a tour.

2 Likes
11

I understand that Crystal type-checker works this way. What I don’t well-understand is that you prefer duck typing to compositional typing. For me, with duck typing, what you win in design/development time, you loose it in debugging time. And I prefer taking time to design/develop than taking time to debug.

But, that is fine. There is no obligation to have the same practices. Diversity of mind is a chance that we should leverage.

Finally, I simply refine my feature-wish as the following.

Could we imagine to have an annotation like “@[TypingContract]” on methods (or classes), such that for methods (or classes) with this annotation, the type-checker ensures that there is no context in which their body does not respect their type restrictions ?

Hence, on the first example below:

@[TypingContract]
def demo(c) : Nil
  a = c.new()
  puts(“demo on #{a.class}”)
  (1..10).each {|x| a.push(x*x)}
  puts(a)
end

where implicitly, the type of c is Object, then the compiler would complain:

3 | a = c.new()
^–
Error: undefined method ‘new’ for Object.class

On this second example below, with the typing contract:

@[TypingContract]
def demo(c : Array(Number).class) : Nil

the compiler now would complain:

5 | (1..10).each {|x| a.push(x*x)}
^
Error: expected argument #1 to ‘Array(Number)#push’ to be Number, not Int32

And hopefully, some very smart Lint tool would further help in saying For example, demo(Array(UInt8)) is ill-typed.

At, last, hopefully, the following typing contract would be validated by the compiler:

@[TypingContract]
def demo(c : Array(Int32 | Int64 | Float64).class) : Nil

I believe that such a feature would:

  • be backward compatible
  • help newbies to learn Crystal
  • give a helping tool to debug type-checking errors in large projects
  • incrementally lead to incremental compilation: on the use of a class/method with a @[TypingContract] annotation, the compiler would know that the analyses done on this component are valid in any context, and can reuse these analyses in the current context without redoing them.
12

Yeah, I understand this could be useful.
There is a similar discussion about the return types, in this case of Enumerable methods: Return types of generic interface implementations ¡ Issue #12803 ¡ crystal-lang/crystal ¡ GitHub

You can easily achieve that effect with an explicit cast to the type restriction.
This is a bit challenging with the original example because the variability of the generic is hard to describe.

So let’s use this much simpler example:

def foo(x : Float64 | Int32)
  x << 1
end
 
foo 1

#<< is only defined on Int32, not Float64. So calling the foo(Float64) signature would not compile. But the only call has a Int32 argument, and the Float64 path is never checked.

You can enforce this by explicitly casting the parameter’s type to the type restriction.

def foo(x : Float64 | Int32)
  x = x.as(Float64 | Int32)
  x << 1 # Error: undefined method '<<' for Float32 (compile-time type is (Float32 | Int32))
end
 
foo 1

This could even be abstracted with a macro, so you don’t need to repeat the same type information.

macro cast_type_restrictions
  {% for arg in @def.args %}
    {% if restriction = arg.restriction %}
      {{ arg.internal_name }} = {{ arg.internal_name}}.as({{ restriction }})
    {% end %}
  {% end %}
end

def foo(x : Float32 | Int32)
  cast_type_restrictions
  x << 1 # Error: undefined method '<<' for Float32 (compile-time type is (Float32 | Int32))
end

foo 1

Note: There may be dragons. This mechanism does not work universally because type restrictions have different semantics than casts.
In the original example, Array(Float64 | Int32).class is a valid type restriction for both, but not a valid cast target for neither Array(Float64).class nor Array(Int32).class.

1 Like
13

Great, thank you for this smart trick. This could be workaround until a more robust feature is provided by the compiler.

15

Sorry to have submitted this feature wish without enough discussion. I would love to have feedback from the community on this idea. It seems somehow related to this proposal