> most modern statically typed languages maintain soundness through a combination of compile time and runtime checking.

Rust, C, C++ - all do not keep around this information.

You're right that the JVM languages (and thus, naturally, C#) do it differently. I think it is a bit silly to name out each of the JVM languages separately.

Haskell, Go, and I think OCaml also rely on some amount of runtime checking for soundness.

I think basically every managed statically typed language ends up carrying around runtime representation and uses some amount of runtime checks.

Haskell has full type erasure.

It still has to carry around enough information to detect non-exhaustive matches and throw at runtime, no?

Only in the same way that "if ... else if ... else" needs to know about types, which is to say mostly not.

AFAIK - and this might be either dated or just wrong - the two places GHC doesn't fully erase are 1) polymorphic recursion (where if we squint it's probably not unreasonable to treat the dictionaries as type tags), and 2) when the programmer explicitly asks for run-time type information with Typeable.

But what are you performing the "if else" on? Type level information stored at runtime, no?

Value level information. The compiler statically knows the type that's being matched on. It's true that the generated code depends on the type, but that's not any more true than when a C compiler generates an integer comparison vs a float comparison in the conditional of that "if". All that's looked at at runtime is the data.

Yes, but those aren't types, they're values.

I am unfamiliar with Haskell and Go. What you are saying is not true for OCaml

My understanding is that you can have non-exhaustive matches which the compiler won't always catch statically and will throw a Match_failure at runtime if no case matches.

Non-exhaustive matches are always detected statically in OCaml.

However, such matches are considered valid code: "non-exhaustive match" is a warning by default, even if most people advise to turn that warning into an error.

In other words, the `Match_failure` exception is part of OCaml non-typed semantics and there is no soundness issue involved here.

But how is Match_failure detected at runtime unless type information is passed around?

There is no type information at runtime at all in OCaml. Once the program has been typed, the program is translated into an untyped lambda-calculus and all type information is throw away. In particular, pattern matching is compiled into this untyped lambda-calculus using if/then/else (and switch statement, and exception and exceptions handlers, ...). The type system is sufficient to detect before this compilation if the pattern is total or if it need to add a failure case. In this case, the `Match_failure` is just a catch-all term in this conditional expression.

For instance

  let f x = match x with
  | [] -> ()

is translated into

    (is_empty/267 =
       (function x/269 : int
         (if x/269
           (raise (makeblock 0 (global Match_failure/18!) [0: "r.ml" 1 17]))
           1)))

where you can see the exception being build and raised in the `then` branch of the test. Contrarily, the total function

  let is_empty x = match x with
  | [] -> true
  | _ :: _ -> false

becomes

  (let (is_empty/267 = (function x/269 : int (if x/269 0 1)))

And since the function doesn't need to handle the failure case, it doesn't have that `(raise ...)` case.

Another important point is that type system information is only needed to check the exhautiveness of pattern matching in presence of GADTs. Otherwise the exhautiveness of pattern matching can be checked using syntatic criteria on the pattern matching and type definitions.

Yes, sorry I meant in the context of GADTs. Is it really full type erasure if that GADT information is passed aorund?

No type information is ever passed to a compilation phase lower than the typechecker in the OCaml compiler pipeline.

In the GADTs case, the type system is only used to remove the failure branch. For instance,

    type 'a t = A: int t | B: float t
    let always_a (x:int t) = match x with
    | A -> ()
    | _ -> .

is translated to

  (let (always_a/270 = (function x/272[int] : int 0))

because the typechecker can prove that the `B` case is impossible. In other words, GADTs are yet another instance where the type system can be used to eliminate dead code in the untyped IR.

I see, so you can never really get a match_failure due to type level mismatch with GADT because it would be caught by the compiler.

Makes sense to me.

You know, that's a solid question that I don't know the answer to.

C++ community is split by the RTTI compiler flags

Rust standard library includes RTTI support, though it's very rarely used.