Making Wrong Code Look Wrong (2005)

Re:Making Wrong Code Look Wrong (2005) by touisteur on Saturday November 09, 2019 @05:24PM (#21494851)

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 :-)

[ Parent | on HN ]

Re:Making Wrong Code Look Wrong (2005) by lifthrasiir on Saturday November 09, 2019 @09:57PM (#21496120)

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

[ Parent | on HN ]

Re:Making Wrong Code Look Wrong (2005) by touisteur on Sunday November 10, 2019 @02:33AM (#21496913)

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.

[ Parent | on HN ]