Zulip Chat Archive

Stream: new members

Topic: SafeIdx: a beginner-friendly library

Adrien Champion (Jun 17 2023 at 13:37):

I just published my SafeIdx library :smile:

It basically generates Uid types that are just wrappers around Nat, and Uid-related mappings which are just arrays only indexable by a specific Uid type. The result is (hopefully) zero-cost arrays and indices, except that type-safety prevents from using, say, a Client index instead of a Product index in a Product-related mapping.
Because this is Lean, SafeIdx also provides dependent (length-aware) mapping types which is super fun to write.

Check out what it looks like on this example:

Adrien Champion (Jun 17 2023 at 13:38):

I'm not here to argue that's the most useful library ever :smile: But it might be interesting to others; I find the exercise of writing/reading such a library very valuable for beginners as it's not very ambitious so it's easy to grasp the concepts, but still requires playing around with types, relatively low-level array manipulations, coercion, custom-indexing, syntax extensions, and much more. It should also ideally be zero-cost, so there's even room for messing around with optimization.

There's even a (very simple) termination proof in there!

Adrien Champion (Jun 17 2023 at 13:39):

Also, I'm definitely not a Lean expert so any remarks for improving readability/ergonomics or anything else would be great.

Feel free to start with this hideous bit and let me know how to do this cleanly once you're done laughing

Last updated: Dec 20 2023 at 11:08 UTC