A type system for RCL, part 2: The type system

The author's generalized subtype check is interesting: what the author defines as "inconclusive" is clearly a type error in more traditional statically typed languages. (Traditionally the type checker is supposed to guarantee progress and preservation, so leaving something inconclusive to the runtime isn't acceptable.) And I guess the kind of differentiation the author makes between "inconclusive" and "static error" is so unusual that the normal classification of covariance and contravariance break. This reminds me of Haskell, where type variables may have user-provided annotation of whether they are representational, nominal, or phantom. Such classification affects the ability for values to be treated at runtime as a different type (using Data.Coerce). Maybe the author can come up with a similar system for classifying type variables for things like List.

However for a configuration language that is type checked and immediately run, there's not much difference between runtime type checks and pre-run static type checks. Given this escape hatch, I think the author is right to simply defer everything that cannot be checked statically into runtime checks.

Can't say I really dig using runtime type checks as a get out of jail system for harder to verify problems. The problem I have with that methodology is it creates errors that could have otherwise been caught statically.

Consider, for example, the given example

    let a: Int = 1
    let b: Any = a
    let c: Int = b

In this simple case, it seems like everything works fine. But what if instead of `b = a` we had `b = foo()`? Now all the sudden discovering whether or not `b` can be safely assigned to an `Int` depends entirely on what `Foo` returns. If foo returns `Any` then you can have a mess where some refactoring ends up having a hard to detect bug.

Consider, for example if foo is changed from

    foo() { return 1 }

to

    foo() { if(bar) return "a" else return 1 }

That could be fine given foo is already sending back `Any` but now when `bar` is true that string returned could cause a runtime exception far from where `foo` was defined.

To me, this seems like giving up a large portion of the benefits of having typing in the first place.

Dart 1.0 had a similar system with "optional typing" which was ultimately axed because of issues like these [1]. In my view, this sort of type system is `Any` creating optional typing.

[1] https://news.dartlang.org/2017/06/a-stronger-dart-for-everyo...

I enjoyed the thoughtful article.

It's interesting that type checking happens at runtime so there is no compile time, only runtime. It seems this would make it acceptable. But I wonder if the assumption will always hold.

The assumption:

> The program doesn’t even have any inputs: all parameters are “hard-coded” into it. [1]

Will that always hold? What about environment variables? If the language ever needs to handle parameters, this assumption breaks and thus compile time and runtime will be separated.

Other languages like Go would force you to insert type assertion which is the same thing just explicit. I forces you to "approve" what's happening, and that's a good thing.

There is the saying that every configuration language will eventually evolve into a full blown programming language. I guess it's all about the real world proving the underlying assumptions to be incorrect.

[1] - https://ruudvanasseldonk.com/2024/a-type-system-for-rcl-part...