On 05/19/2018 05:13 PM, Matt Rice wrote:
I'm not terribly enthusiastic about the string -> string -> string type signature, when we could implement so called "perfect crypto" modules in the type system itself, then implementers of this signature could back it with whichever crypto primitives they like
I'm certainly sympathetic with that strategy at an above-average level, as I do research in formal methods for cryptography, and I have an idea on the shelf (to revive some day) for more thorough use of typing to organize composition of cryptographic components.
However, I'm not sure if, for Ur/Web today, the practical value of fancier types would make up for the added standard-library complexity. In the long run, I would like to see secure applications coded with no direct use of cryptography. Rather, we would have higher-level primitives that are implemented with cryptography.
I feel like your suggestion is likely to be controversial enough that it probably belongs in a separate library, if anywhere. I'd be interested to read more opinions here.
In general though, I don't know enough about the compiler implementation to know if adding these extra layers of abstraction are going to impose runtime overhead, this way tends to add a lot of type conversions/identity function calls, which in theory could but may not be inlined across modules, in a way that can be turned into a type cast.
It's probably possible to dream up worst cases where the following is false, but in general the Ur/Web compiler can be counted on to inline all uses of identity functions. There should be no runtime overhead of phantom types.
_______________________________________________ Ur mailing list [email protected] http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
