[HN Gopher] A type system for RCL, part 2: The type system
       ___________________________________________________________________
        
       A type system for RCL, part 2: The type system
        
       Author : todsacerdoti
       Score  : 15 points
       Date   : 2024-07-18 19:28 UTC (3 hours ago)
        
 (HTM) web link (ruudvanasseldonk.com)
 (TXT) w3m dump (ruudvanasseldonk.com)
        
       | kccqzy wrote:
       | 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.
        
       | cogman10 wrote:
       | 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...
        
       ___________________________________________________________________
       (page generated 2024-07-18 23:04 UTC)