Write a function that produces an Ion deserializer for a given Type

[keyboardDrummer]

Write a function that produces an Ion deserializer for a given Type

Write a function with a signature like def getIonDeserializer (a : Type) : ByteArray -> Except Format a

You can find the Ion documentation here: https://amazon-ion.github.io/ion-docs/

[keyboardDrummer-bot]

I'd like to clarify a few things before implementing this:

1. Which Type is meant? The signature def getIonDeserializer (a : Type) : ByteArray -> Except Format a takes a Lean Type as a runtime argument. However, the existing FromIon.deserialize already provides {α} [FromIon α] (bs : ByteArray) : Except String α, which works for any Lean type with a FromIon instance. Are you looking for something different from what FromIon.deserialize already provides? For example:

   • A function that takes a Strata type (e.g. TypeExprF / PreType) at runtime and deserializes an Ion value according to that Strata type schema (returning a dynamically-typed result like Arg)?
   • Or a wrapper/rename of the existing FromIon.deserialize?

2. Error type: The signature mentions Except Format a, but the existing Ion deserialization infrastructure uses Except String. Should I use Except String a to stay consistent, or do you specifically want Std.Format as the error type?

3. Where should this live? Should it go in Strata/DDM/Ion.lean alongside the existing FromIon infrastructure, or in a separate file?

[keyboardDrummer]

Which Type is meant?

A lean Type. But I want the new (additional) getIonDeserializer to work for types that don't have a FromIon instance.

Error type:

I prefer Format

Where should this live?

In Strata/Util

[keyboardDrummer-bot]

I have a few questions before implementing this:

1. Runtime type inspection: In Lean, Type is erased at runtime, so a function with signature def getIonDeserializer (a : Type) : ByteArray → Except Format a can't pattern match on a to decide how to deserialize. How should this work? Some options:

   • Use a type representation: Take a Strata PreType or TypeExprF (which are data you can pattern match on) instead of a Lean Type, and return a dynamically-typed result (e.g., wrapping the result in an Ion SymbolId or a custom DynValue type).
   • Use metaprogramming: Generate FromIon instances at compile time via a macro/elaborator for types that don't have one.
   • Use unsafe: Use unsafeCast or similar to work around erasure.

2. Which types should be supported? For types without a FromIon instance, what's the expected set? For example:

   • Strata DDM types defined via #dialect (like mytype, bool, etc.)?
   • Arbitrary Lean inductive types?
   • Product/sum types?

3. What should the return value look like? Since the Lean type a is erased, the function can't actually produce a value of type a without some form of type evidence. Should the return type be something like Ion SymbolId (a generic Ion value), or do you want actual typed Lean values?

4. Error type Format: The existing FromIonM uses Except String. Should getIonDeserializer use Except (Std.Format) (the pretty-printing Format), or did you mean a different Format type? If Std.Format, should I also add a conversion from the existing String errors?

Understanding these will help me pick the right approach. My best guess is that you want something that takes a Strata type representation (like PreType or TypeExprF) and deserializes Ion bytes into a generic value, but I'd rather confirm than guess wrong.

[keyboardDrummer]

1. Use metaprogramming
2. Arbitrary Lean inductive types. Ideally also structure types
3. Actual values of type a. Can this be solved with the metaprogramming approach?
4. Std.Format. You don't need to change any of the existing code. The new getIonDeserializer will be in addition to what exists.

[keyboardDrummer-bot]

I've opened a draft PR #7 with an initial implementation.

Approach

Since Type is erased at runtime in Lean, I implemented getIonDeserializer% as a term-level elaborator that inspects the type at compile time and generates the deserializer via syntax quotations. The result has type ByteArray → Except Std.Format α.

Ion encoding conventions

• Structures → Ion structs with field names as keys
• Single-constructor inductives → Ion structs with positional keys _0, _1, …
• Multi-constructor inductives → Ion sexps (ConstructorName arg₁ arg₂ …)

Current limitations

• Supported leaf types: Nat, Int, String, Bool
• No support for nested/recursive types yet (would need mutually recursive deserializers)
• No support for parameterized types

Questions for you

1. Are the Ion encoding conventions above what you had in mind, or did you want a different mapping?
2. Should I prioritize adding support for nested types (e.g., a structure containing another structure)?
3. The file lives at Strata/Util/IonDeserializer.lean — is that the right location?