[Ur] Thoughts on cryptographic hashing for Ur/Web standard library?

[Adam Chlipala]

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.