If you keep going in this direction then you get something like Opaleye’s “named template” system. It’s also something I’m exploring pretty heavily with the Scala version of Maia.
“named template” system
I like that name! Less of a mouthful than “fully polymorphic product”.
I struggled for a solid 30 seconds on what to call them. I’m happy where I landed :)
Also for anyone out of the loop, talking about one of these guys: https://github.com/tomjaguarpaw/haskell-opaleye/blob/master/Doc/Tutorial/TutorialBasic.lhs#L572
This is a great trick and shows the value a good type system can add. One can use this trick to ensure that their value has gone through various steps in the program. Perhaps the step is implemented wrong but it at least guarantees it has happened.
An applied example of this can be found in this blog post:
The gist of it is that there is a bug in the code given. However the bug will never happen because the value happens to go through a check earlier in the program. Then the question becomes: should we remove the redundant check? But what then if someone refactors earlier up and removes the check. Type variables to the rescue! This code could be construct such such that verifying the value produces a value of a new type that is the proof that the value when through the verification code. This means if someone refactors the check out, the compiler will complain. What would this look like? Well in Ocaml we could use a phantom type (which is a type variable that is not used in the value). So the length check could look like:
val check_length : 'a t -> [`Length_verified] t
Then the code in the blog post could look something like:
val ssl_bytes_to_cipher_list : [> `Length_verified ] t -> unit
This will ensure that the input value to the function has had its length verified.