Open robin-aws opened 7 months ago
We haven't been super consistent about having two variants of most operations: a partial one with pre-conditions and a complete one that can fail. If we consider the problem holistically we might be able to just have complete versions with lemmas/smart compilation to avoid handling failures when they are not possible.
I'd expect you to have a partial version that is called by a complete version, so that if you can satisfy the precondition you can call the partial version to get the best performance, and otherwise you call the complete version.
Several ideas that came up while wrapping the standard libraries up for 4.4 and writing up a blog post about them:
FileIO
) and one using bounded ints (Unicode
), especially since the blog post uses them together and has to manually convert. At a minimum we should provide convenient alternatives to cast between sequences of both forms and/or variants of current utilities that work with the other form (e.g. something likeReadBytesFromFileAsUint8s
). Going deeper we may want to find a way to avoid the casting/copying data within the language itself: one idea is to optimize the compilation of sequence constructions likeseq(|bs|, i requires 0 <= i < |bs| => bs[i] as BoundedInts.uint8)
so that it is a cheap proxy rather than a full copy.Std.Strings
toStd.String
. :P I don't see a way of easily setting up a "module alias" with the current export set feature, perhaps we could improve that?Strings
functionality inSeq
instead, but ONLY having such things inSeq
makes them harder to discover. We may just want aliases inStrings
somehow, or perhaps we can invest in tools for finding the things you want based on desired signature ala Coq'sSearch
command.