As a thought experiment, I like to assume that there is a hypothetical language where everything is encoded in types, to the point where you don't have or need variable names anymore. Every typed language (and programming style) we use is some point in the spectrum of practical compromises between that hypothetical language where all pre-runtime information is in formal types and scripting languages where all pre-runtime information is in informal names.

Java for example has to leave quite a lot of that information in names because there are no type aliases and final types exist.

I'm curious what type of capabilities are lacking in the Ada or the F# type system to handle this. You can create 'new' (hear incompatible) types instead of subtypes and they won't be affectable to each other. So

   type User_Id_Type is new String;
   type User_Credential_Type is new String;

Then in your request deserializer convert once from String to the correct type, and at the use site only allow taking the correct type?

You can also add static predicates to ensure User_Id_Type doesn't contain spaces. You can also make the type 'opaque' and it won't be possible to convert to a String without a bespoke interface.

I'm not sure what's missing. I almost feel like it would be a great challenge :-)

I think in this particular case they suffice, because they are clearly different subtypes as I've mentioned.

It is much harder, if not impossible, if you have to describe a relation between two or more values of the same subtypes. For example, imagine that you already "know" certain indices never go off the boundary of given array but want to encode that information to types. Sure, there exists a Rust crate [1] that tracks a relation between indices and originating array via lifetime, but it is complicated.

[1] https://github.com/bluss/indexing

Mmmh thanks for the link and the paper about generative types. Seems very interesting!

I'm wondering if using type predicates or type invariants (+ proof for static verification, otherwise the check will mostly be at runtime) would help here.

Look up https://blog.adacore.com/spark-2014-rationale-type-predicate... if interested.