Open uncomputable opened 1 year ago
I propose we use the word const
for this new concept, since it isn't overloaded with anything internal to the Haskell library or to the specification of the const-word jets.
It would be a strict generalization of our current use of const
, which is just for single constant-word jets.
Scribe is pretty useless now that we have word jets. It's basically only useful for values that are not strings of bytes. With that in mind, I propose we redefine scribe to greedily use word jets. That is, if we have a left sum value of some byte string, we use injl on a word jet, and so on. (We can choose a different name for this operation if it is confusing. But the pure scribe is really only useful for the completeness theorem and for test cases.)