3 ms·

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 ca

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.

hither_shores 5y ago
Haskell has full type erasure.
- munificent 5y ago
  It still has to carry around enough information to detect non-exhaustive matches and throw at runtime, no?
  - dllthomas 5y ago
    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.
    - whimsicalism 5y ago
      But what are you performing the "if else" on? Type level information stored at runtime, no?
      - dllthomas 5y ago
        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.
  - tome 5y ago
    Yes, but those aren't types, they're values.
whimsicalism 5y ago
I am unfamiliar with Haskell and Go. What you are saying is not true for OCaml
- munificent 5y ago
  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.
  - octachron 5y ago
    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.
    - whimsicalism 5y ago
      But how is Match_failure detected at runtime unless type information is passed around?
      - octachron 5y ago
        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.

hither_shores 5y ago

Haskell has full type erasure.

munificent 5y ago
It still has to carry around enough information to detect non-exhaustive matches and throw at runtime, no?
- dllthomas 5y ago
  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.
  - whimsicalism 5y ago
    But what are you performing the "if else" on? Type level information stored at runtime, no?
    - dllthomas 5y ago
      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.
- tome 5y ago
  Yes, but those aren't types, they're values.

whimsicalism 5y ago

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

munificent 5y ago
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.
- octachron 5y ago
  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.
  - whimsicalism 5y ago
    But how is Match_failure detected at runtime unless type information is passed around?
    - octachron 5y ago
      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.