More consistent naming scheme for type parameters in Cryptol prelude.

[brianhuffman]

Since 0bf3680, defaulting warnings and type error messages now display the type argument names from the type schemas of the functions involved. The usefulness of the error messages can be further improved by choosing descriptive type argument names that follow a consistent naming scheme.

Here's an example of a prelude function with nice type names:

take : {front,back,elem} (fin front) => [front + back] elem -> [front] elem

And here's an example of not-so-nice names:

(@@) : {a, b, c, d} (fin d) => [a]b -> [c][d] -> [c]b

With @@, the type parameter names don't even suggest the kind (numeric vs value) of the types, let alone their purpose.

Here are some initial observations:

• Type names should suggest their kinds: We shouldn't use a,b,c,d for both numeric and value types, for instance.
• Descriptive names are more important for functions with multiple type parameters; functions with only one type argument are probably OK with a short name.
• Several prelude functions (shifts, rotates, and indexing functions) take a numeric parameter that is the bitwidth of the index type. We should give all of these the same name.

[brianhuffman]

836771a updates a bunch of type variable names. We're mostly using short names for now, with a, b, c used only for value types and n and k used for numeric types. We use ix to indicate the bit-width of an index argument (for shift/rotate/lookup/update functions).

For variable order, we mostly try to put numeric types first, followed by value types. If a function's result type is not determined by its arguments, then we order variables so that positional partial type application is most useful. (For example, we have error : {a, n} [n][8] -> a with the value type argument first, so that we can write e.g. error`{[32]} "foo".)

Let's give these types a try, and see if we like how they look in :help and also in type error messages.

@yav also suggested that we could follow similar naming conventions for inferred type schemas, where numeric types would come first and have names like i,j,k,m,n; value types would come later and have names like a,b,c,d,e.

[brianhuffman]

Revision 4c6a69c implements the other type-variable-name-related improvements that we had planned, so I'm closing the ticket.