New Library: ln-messagepack

Stream: general

[io.shift]

---

Hi everyone! I'm excited to share a new library I've been working on: ln-messagepack, a pure Lean 4 serialization library for MessagePack.

It provides a fast, type-safe API for encoding and decoding Lean data structures with no external dependencies (just batteries). It's also tested and benchmarked!

Key features include:

• Support for all major types (nil, bool, int, string, etc.).

• Out-of-the-box support for Array and List.

• A full implementation of the ext type family, with Timestamp included.

The only feature not yet supported is the decoding of float/double types, due to the lack of a bitwise Float.ofUInt64 primitive in Lean 4. I decided it was better to release a robust library with this known limitation than to add a fragile, custom implementation.
EDIT: I was using an old documentation as reference. The latest versions of Lean4 do indeed have such primitives. Floats will be added by Monday.

GitHub: https://github.com/ItsMeForLua/ln-messagepack

It's easy to use. Just add it to your lakefile.lean:

Lean

require «ln-messagepack» from git "https://github.com/itsmeforlua/ln-messagepack" @ "main"

And then import the main module in your file:

Lean

import LnMessagepack.MessagePack

Basic Example:

Lean

let bytes := encodeToMsgPackBytes "hello from Lean!"
match decodeFromMsgPackBytes (α := String) bytes with
| some s => IO.println s!"Decoded: {s}"
| none => IO.println "Failed!"

I'd love to get any feedback or suggestions you might have.

Have fun not using JSON :)

---

[suhr]

Here's some thoughts:

• In Rust, you can do #[derive(Serialize, Deserialize)] instead of adding ad-hoc classes for each format. There should be a way to do something similar in Lean
• Since it's Lean, one should consider not only implementing things, but also proving them against a spec
• Any plans for CBOR?

[Robin Arnez]

Not sure what lean version you're using but there should be Float and Float32 with Float.toBits, Float.ofBits, Float32.toBits and Float32.ofBits

[io.shift]

--deleted message--

[io.shift]

@suhr
Hi suhr, thanks so much for the thoughtful feedback! Those are all fantastic points.

On deriving: That's a great idea for a future version! I agree that a deriving MsgPackEncode handler would be a huge usability win. I'll add it to the long-term roadmap. It would definitely be a great idea to dive into Lean's metaprogramming. :)

On proofs: I think formally proving correctness against the spec is a great long-term vision and would be a perfect way to leverage Lean's strengths. It's a huge project, but something I would surely LOVE to see happen.(probably within the month because coding is my obsession)

In regards to CBOR: That's an interesting thought! For now, my focus is on making the MessagePack implementation as complete and robust as possible. Once it's fully mature, expanding to other formats like CBOR could be a cool direction for the future. Although, knowing how I am, I'll probably start working on that next week lol

Thanks again for the great suggestions!

[io.shift]

@Robin Arnez Hello Robin, you're right lol I just checked the official latest documentation and it's definitely there. I was clearly using an old documentation for reference. I'll add floats by Monday, once I finish my final exams this weekend.

[Robin Arnez]

For encoding, I'd use an accumulator byte array instead of allocating one every time. That means update the signature of encodeToBytes to def encodeToBytes (v : MsgPackValue) (acc : ByteArray := .empty) : ByteArray := and using push to encode bytes.

[Robin Arnez]

If you want proofs, newer versions should also allow you to get rid of the partial in encodeToBytes.

[Robin Arnez]

Also you probably want the EStateM monad for all parsing stuff, so def parse (bytes : ByteArray) : EStateM String Nat MsgPackValue := do and using get, set and modify for accessing the offset.

[io.shift]

@Robin Arnez In regards to partial's, I had tried to do it without partial, but I was getting type errors pretty consistently. I have the latest stable release, but, aren't recursions in lean that aren't descending (and/or can't be proven as such), needed to be specified as partial?

If not, then I would definitely prefer to get rid of partial haha

If there's a way to prove to lean(4) the termination of the (and other def's) recursion, let me know !
I'm still fairly new to lean4, so any "work around" would be very much appreciated by me

[suhr]

https://lean-lang.org/doc/reference/latest///Definitions/Recursive-Definitions/#well-founded-recursion

[suhr]

Parsing consumes input, so length of remaining input could be used as a measure.

[io.shift]

wow I feel stupid for not thinking of that
I'll have to update those def's today so they're a bit more reliable than how they are rn
Thank you,

[Kim Morrison]

Project is missing a lean-toolchain file, so can't be opened in VSCode.

[Kim Morrison]

lake build fails with errors in Tests.lean. You should move these to be compiled only by lake test.

[Kim Morrison]

You can remove the Batteries dependency by writing deriving instance BEq for ByteArray somewhere. We'll make sure that's available out of the box soon.

[io.shift]

@Kim Morrison You're right, thank you bringing those to my attention!
If you have anymore critical suggestions, PLEASE, let me know

[io.shift]

lean4 project structure, and how the parser handles paths, is something that's a bit new to me
Most of the issues I end up getting during development are in regards to structure and accidently confusing the parser. Which is not the fault of lean4 necesarrily, just the fact I'm used to other languages and how they expect your project's structure to be underthehood

[Robin Arnez]

soon

commits deriving instance BEq for ByteArray 2 hours later

[Robin Arnez]

Well regardless, fyi, I have a draft lean4#8165 which has some ideas for ByteArray functions that might be useful for a project like this one.

[io.shift]

For the past few hours I've been updating the code, aswel as modulating a bit more for seperation of concerns (Encoding, Decoding, etc). For some recursions, due to their complexity, I've resorted to fuel patterns, however, for lean4 specifically, I'm wondering if this could mask particular recursion errors (?) My intuition is telling me the answer is yes, but I don't have anything tangible in the front of my head yet to approach this

[io.shift]

For context, here’s a simplified version of my mutual recursion with the fuel pattern:

mutual
  def encodeValue_go (fuel : Nat) (v : Value) : String :=
    if fuel == 0 then "" else
    match v with
    | .arr a    => encodeList_go (fuel - 1) a.toList
    | .map m    => encodePairs_go (fuel - 1) m.toList
    | .int i    => toString i

  def encodeList_go (fuel : Nat) (vs : List Value) : String :=
    if fuel == 0 then "" else
    match vs with
    | [] => ""
    | v :: vs' => encodeValue_go (fuel - 1) v ++ encodeList_go (fuel - 1) vs'

  def encodePairs_go (fuel : Nat) (ps : List (Value × Value)) : String :=
    if fuel == 0 then "" else
    match ps with
    | [] => ""
    | (k, v) :: ps' =>
      let kStr := encodeValue_go (fuel - 1) k
      let vStr := encodeValue_go (fuel - 1) v
      kStr ++ vStr ++ encodePairs_go (fuel - 1) ps'
end

[io.shift]

Ah, nevermind, I found the issues that I felt intuitively
I was double-decrementing fuel, and I additionally need to add caching, and ahead of time fuel caps if I go through with using fuel patterns

[io.shift]

I'm scratching the Fuel method.....I can't apply D.R.Y, and flattening is just impractical for this method.

K.I.S.S must be central

[io.shift]

Approach will now be:
Structural Recursion for most
Tail recursion for some
And for optimization:
Automatic tail recursion optimization and type-class-based instance resolution for well-founded relations.

Additionally:
Im creating a (roswell) common lisp module(s) for debugging and error handling of ln-messagepack , but this will be in a seperate github repository, and neither userfacing nor a dependency.
Lisp, including the Roswell REPL, saves me SO much time in development.
End users will not need to install or interact with Lisp or Roswell; this is purely for my own ( and hopefully other's) development workflow.

I'm burning up energy trying to manage errors from complex recursions...Lisp will fix that.