String manipulation functions / generalize list functions?

[phile314]

I am currently writing code involving quite a lot of String manipulation, and currently agda-prelude doesn't offer much functionality for plain Strings yet. I can go via List Char, but that will definitely be slower and feels overly complicated just to e.g. split a string.

The question then is how these functions should be added. Should the existing functions in Data.List be generalized and moved to Container.Foldable? What about functions which don't find into any existing class like a monomorphic functor for strings? What about sequence-like methods?

The other option would be to have multiple distinct specialized functions. However, if we use the same
names we have to put them in a separate modules as both Prelude.String and Prelude.List are imported in Prelude. One could also add some kind of prefix to the functions, eg "s" for all String
specializations to get sLength, sDrop etc..

My preference would be to generalize the functions. This would unify the functions for all types
and one doesn't need qualified imports for all the containers data types. The main drawback
is that it complicates the types and it could make type inference harder.

Any thoughts?

Container.Foldable candidates:

• length
• null
• elem
• sum
• product
• maximum
• minimum
• any
• all

Sequence-like methods:

• take
• drop
• filter
• isPrefixOf

[UlfNorell]

String isn't a functor so how will generalise list functions to Foldable help?

[phile314]

True, that doesn't help for String. It should read MonoFoldable instead of Foldable, where MonoFoldable is the monomorphic version of Foldable. I think I will try this out in my fork and see how usable it is.