3 ms·
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 sub
by touisteur 7y ago
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 :-)
- lifthrasiir 7y agoI 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 https://github.com/bluss/indexing
- touisteur 7y agoMmmh 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-predicates https://blog.adacore.com/spark-2014-rationale-type-predicate... if interested.