Make `length` return the dedicated type
Clarification and motivation
There is an acknowledged issue (I heard at least two mentions, one is here) that length returns exactly Int - too often we want a different type and have to convert explicitly. In #423 (closed) this problem has raised with new rigor, Unsafe.fromIntegral @Int @a . length got a de-facto common pattern.
I suggest to re-implement length in morley-prelude package as follows:
newtype Len = Len Int
type instance IntBaseType Len = FixedWordTag 29 -- think which number to put here
length :: (Container t, IsIntSubType Len l ~ 'True) => t -> l
and probably Len should be assumed to be of 29-bytes. We can assume that length of any container is not larger, and casting to wider types is safe (currently a similar assumption is made anyway - length returns Int).
The only perfect solution would be to make length return Natural, but I suspect we don't want to go there. In either way, if lists turns to be larger than we expected, the solution above allows making the restriction on length's return type stricter (allowing only larger values) anytime.
Also, in this issue I propose to look at usages of take and drop - whether are they often used with an explicit cast, and probably update them as well (in their case, I think we could even accept an arbitrary Integral number).
Acceptance criteria
-
lengthis updated so that the following explicitfromIntegralis necessary only when the target type is too narrow. - Whether
takeanddrop(and maybe other similar functions) are worth making accept various numeric types - is considered.