[TheMatten]

Very nice release, Gleam looks like a good contender for "high-level Rust".

Small nitpick:

> One drawback of this sound type system is that converting untyped input from the outside world into data of known types requires some additional code which would not be required in unsound systems.

It isn't really consequence of its sound type system, but its runtime representation - assuming it requires type information to be safely constructed and manipulated, you really need to generate code to do so, but the compiler could instead choose to use more dynamic representation, e.g. compiling to ordinary Erlang maps / JS objects.

[Ndymium]

How would this representation be converted back to known types without similar decoders? Right now Gleam compiles custom types to Erlang records (tuples) and JS classes.

[TheMatten]

The representation would be _the_ runtime representation of those types - in the same way as TypeScript objects are just JavaScript objects with static analysis. The choice of representation is a matter of performance and statically-typed languages usually choose to compile every type to custom representation simply because it makes things more efficient, not because they have to. Unless you implement some baked-in reflection mechanism, there isn't really anything that ties runtime representation to its type, which is a compile-time concept.

The other problem is ensuring that such casting is safe, but that requires runtime checking even in dynamically typed languages.

[Ndymium]

Since it requires runtime checking anyway, that code has to live somewhere. The decoders are that code. I don't understand how changing the runtime representation would allow to not have those decoders. Unless you mean they should be implicitly generated by the compiler. Or maybe I'm just missing what you're saying.

[TheMatten]

My point was about the sentence from the original post - its not the consequence of sound type system, its the consequence of choice of runtime representation. If runtime checking matters (which it does in practice), then we don't get any advantage in terms of simplicity by using "unsound" system, because we need to write that code anyway.

[Ndymium]

Ah, thanks for explaining. :)