Recursive types

[ChristopherRabotin]

Hi there,

I'm trying to use dada to represent a recursive type. Specifically, I have the two following types in Rust:

enum NodeType {
    Leaf { kind: String, key: String },
    Sequence { children: Vec<Node> },
    Fallback { children: Vec<Node> },
}

struct Node {
    node_type: NodeType,
    name: String,
}

This allows me to represent behavior trees.

@sellout, the author of dada, was kind enough to write a recursion Dhall type to represent this.

let Rec = https://sellout.github.io/dada/Mu/Type

let NodeType =
      λ(a : Type) →
        < Leaf : { kind : Text, key : Text }
        | Decorator
        | Sequence : { children : List a }
        | Fallback : { children : List a }
        >

let Node = λ(a : Type) → { type : NodeType a, name : Text }

let Tree = Rec Node

Where the Mu/Type is defined as:

λ(f : Type → Type) → ∀(a : Type) → (f a → a) → a

Here is how I tried to build up this type in Rust:

let ty: serde_dhall::SimpleType = serde_dhall::from_str(
        r#"let Rec = λ(f : Type → Type) → ∀(a : Type) → (f a → a) → a

        let NodeType =
              λ(a : Type) →
                < Leaf : { kind : Text, key : Text }
                | Decorator
                | Sequence : { children : List a }
                | Fallback : { children : List a }
                >
        
        let Node = λ(a : Type) → { type : NodeType a, name : Text }
        
        let Tree = Rec Node"#,
    )
    .parse()
    .unwrap();

which leads to the following error:

called `Result::unwrap()` on an `Err` value: Error(Dhall(Error { kind: Parse(Error { variant: ParsingError { positives: [import_alt, bool_or, natural_plus, text_append, list_append, bool_and, natural_times, bool_eq, bool_ne, combine, combine_types, equivalent, prefer, arrow, let_binding], negatives: [] }, location: Pos(444), line_col: Pos((13, 28)), path: None, line: "        let Tree = Rec Node", continued_line: None }) }))

From the documentation (https://docs.rs/serde_dhall/latest/serde_dhall/enum.SimpleType.html#type-correspondence), I understand that SimpleType does not support the T -> U operation. Does that also apply to lambdas ? (I'm a novice in Dhall, so my apologies if I'm not using the correct terms.) Is there a way I could build this simple type "by hand" using the HashMap and provided enums method?

If this is not yet supported, do you have an idea of what changes that would be required and whether I could work on that? I'm a Dhall novice but quite competent in Rust.
Thanks

[Nadrieril]

Hi, a SimpleType doesn't support any kind of function types; it's only for simple non-recursive structs and enums. To get any more than that you have to use dhall-rust directly (instead of serde_dhall). Problem is, dhall-rust doesn't have a sane API (it was my first non-trivial rust project 😅), and I'm not maintaining it anymore. If you want to do the work to clean it up and figure out an API that can support your type, I''m happy to chat!

[ChristopherRabotin]

Sure, I'd be keen to learn how the API works and make changes to maintain it. I guess I don't quite know where to start though... What's Nir and Hir for example?

I'm also trying to understand how the Parsed structure of dhall works. It's straightforward to parse the Dhall from above into a Parsed structure, but now I don't know what to do with it... Can Parsed be used to serialize structures? It seems that serde_dhall re-implements this and only SimpleValue can be serialized? As you can tell, I'm new of Dhall!

[sellout]

I can add a Topo = λ(f : Type → Type) → List (f Natural) API to Dada (like the one in https://recursion.wtf/posts/rust_schemes/), and then Topo Node should work with serde_dhall/SimpleType. I already have this code somewhere. I’m surprised it hasn’t been published in Dada yet.

On the Dhall side, there should be no change to the code other than s/Mu/Topo/.

[ChristopherRabotin]

Yes! That is indeed compatible with SimpleType! The following works for the initialization of a SimpleType:

let ty: serde_dhall::SimpleType = serde_dhall::from_str(
        r#"let NodeType =
              λ(a : Type) →
                < Leaf : { kind : Text, key : Text }
                | Decorator
                | Sequence : { children : List a }
                | Fallback : { children : List a }
                >
        
        let Node = λ(a : Type) → { type : NodeType a, name : Text }

        let Topo = λ(f : Type → Type) → List (f Natural)
        
        let Tree = Topo Node
        
        in Tree"#,
    )
    .parse()
    .unwrap();

However, trying to serialize the root node leads to

dhall-rust/serde_dhall/src/serialize.rs

Line 202 in d8c2e65

"Unsupported data for serialization: struct variant".to_owned(),

. Maybe that's something I could tackle as a first issue.

[Nadrieril]

Nice :) Yes, we don't support struct variants apparently, this shouldn't be too hard

[ChristopherRabotin]

Nearly 18 months later, I finally got around to trying to implement this. I've tried implementing it identically to the SerializeStruct master...ChristopherRabotin:dhall-rust:gh-242-recursive-types/gh-242-recursive-types .

Here is the example I'm testing against:

#[derive(Clone, Serialize, Deserialize, Debug, PartialEq)]
pub enum VectorExpr {
    Fixed {
        x: f64,
        y: f64,
        z: f64,
    }, // Unitless vector, for arbitrary computations
    Position {
        from_frame: FrameUid,
        to_frame: FrameUid,
    },
    Velocity {
        from_frame: FrameUid,
        to_frame: FrameUid,
    },
    CrossProduct {
        a: Box<VectorExpr>,
        b: Box<VectorExpr>,
    },
}

Here is the very early test case:

#[test]
    fn test_vector_expr_fixed() {
        let v = VectorExpr::Fixed {
            x: 1.0,
            y: 2.0,
            z: 3.0,
        };
        let v_str = serde_dhall::serialize(&v).to_string().unwrap();
        println!("{v_str:?}");
        let v_deser: VectorExpr = serde_dhall::from_str(&v_str).parse().unwrap();
        assert_eq!(v_deser, v);
    }

The serialization returns "{ x = 1.0, y = 2.0, z = 3.0 }" ... which seemed correct until I tried the deserialization as it returned an error Error(Deserialize("invalid type: map, expected enum VectorExpr")).

So obviously, I haven't implemented this correctly.

What should be the correct Dhall for this serialization? It seems that the Enums require listing out all variant: is that correct? Your answers will help me correctly implement this.

Thank you

[sellout]

Yeah, you do need all the variants, but it’s generally behind a binding when you write it directly:

let Rec = https://sellout.github.io/dada/Mu/Type

let FrameUid = <>

let VectorExpr =
      \(r : Type) ->
        < Fixed : { x : Double, y : Double, z : Double }
        | Position : { from_frame : FrameUid, to_frame : FrameUid }
        | Velocity : { from_frame : FrameUid, to_frame : FrameUid }
        | CrossProduct : { a : r, b : r }
        >

in  (VectorExpr (Rec VectorExpr)).Fixed { x = 1.0, y = 2.0, z = 3.0 }

You can see the complexity the recursive type adds. I’d recommend getting this working without that bit first.

If we remove the CrossProduct case, it’s simply

let FrameUid = <>

let VectorExpr =
        < Fixed : { x : Double, y : Double, z : Double }
        | Position : { from_frame : FrameUid, to_frame : FrameUid }
        | Velocity : { from_frame : FrameUid, to_frame : FrameUid }
        >

in  VectorExpr.Fixed { x = 1.0, y = 2.0, z = 3.0 }

When serializing it from Rust, you’d probably fully inline it:

< Fixed : { x : Double, y : Double, z : Double }
| Position : { from_frame : <>, to_frame : <> }
| Velocity : { from_frame : <>, to_frame : <> }
>.Fixed
  { x = 1.0, y = 2.0, z = 3.0 }

Anyway, I imagine dhall-rust already handles that bit somewhere. The recursive bit is orthogonal to the enum serialization.

Recursive types are generally enums, but nothing prevents something like

pub struct Stream<T> { head: T, tail : Box<Stream<T>> }

To get the serialization of any recursive type, you need to extract the underlying functor, but that shouldn’t be too different from dealing with any other type parameter (like T in Stream<T>), just involves matching on Box<_> where _ is the name of the type we’re serializing.¹

\(t : Type) -> \(r : Type) -> { head : t, tail : r }

But that still leaves some pieces to connect …

Footnotes

1. It can definitely get hairy here, with other forms of indirection than Box or types like

   enum PerfectTree<T> {
     zero: T,
     succ: Box<PerfectTree<(T, T)>>
   }
   

   which would need to be serialized like

   \(t : Type) -> \(r : Type -> Type) -> < zero : T, succ : r (T, T) >
   

   but I don’t think those need to considered maybe ever. ↩

[ChristopherRabotin]

Thanks for the details, @sellout .

The serde enum documentation, and a quick test I ran yesterday, indicates that when serializing a specific variant, one does not have access to all the variants of the enum, only to the enum name and the variant currently being serialized.

Hence, I'm considering implementing the variant by defining a new enum for each serialization. For example, instead of serializing two variants of the same enum, fixed and position, I was going to implement it as two separate enums:

let fixed = < Fixed : { x : Double, y : Double, z : Double }
>.Fixed
  { x = 1.0, y = 2.0, z = 3.0 }

let position = < Position : { from_frame : Natural, to_frame : Natural }
>.Position
  { from_frame = 399, to_frame = 0 }
  
  in {fixed, position}

The major downside with this approach is the lossy serialization: there is no indication that Position and Fixed are actually variants of the same enum. Are there another downsides I'm missing? In my application, even this non-conforming serialization would be good enough (most of my users won't be editing the Dhall config themselves, but instead rely on a GUI).

[sellout]

Another downside is that a Vec<VectorExpr> won’t serialize to valid Dhall.

E.g., if you change your example to end with in [fixed, position], it evaluates to

[ < Fixed : { x : Double, y : Double, z : Double } >.Fixed { x = 1.0, y = 2.0, z = 3.0 }
, < Position : { from_frame : Natural, to_frame : Natural } >.Position { from_frame = 399, to_frame = 0 }
]

which won’t typecheck because the elements have different types. At least if the config is GUI-managed, no one will have to read the extremely noisy

[ < Fixed : { x : Double, y : Double, z : Double }
  | Position : { from_frame : Natural, to_frame : Natural }
  | Velocity : { from_frame : Natural, to_frame : Natural }
  >.Fixed
    { x = 1.0, y = 2.0, z = 3.0 }
, < Fixed : { x : Double, y : Double, z : Double }
  | Position : { from_frame : Natural, to_frame : Natural }
  | Velocity : { from_frame : Natural, to_frame : Natural }
  >.Position
    { from_frame = 399, to_frame = 0 }
]

unrelated tangent

But that raises a readability issue that I hadn’t considered in Dhall before (which doesn’t affect your GUI-managed stuff). I wonder if Dhall libraries in general (and dhall-rust in particular) could/should offer a post-processing step, where you can take the dhall.Expr that results from serde and do

simplify_types(
    // using `parse` here to avoid writing the Dhall using the Rust type’s
    // constructors, but I would do it the safer way in actual code.
    dhall.parse(
        "
let VectorExpr =
      < Fixed : { x : Double, y : Double, z : Double }
      | Position : { from_frame : Natural, to_frame : Natural }
      | Velocity : { from_frame : Natural, to_frame : Natural }
      >
in  {}
",
        expr)
)

where simplify_types mostly reuses the machinery required for normalization in order to find occurrences of types that have bindings and replace them with the bound name. So if simplify_types was run on that list I included above, the result would be

let VectorExpr =
      < Fixed : { x : Double, y : Double, z : Double }
      | Position : { from_frame : Natural, to_frame : Natural }
      | Velocity : { from_frame : Natural, to_frame : Natural }
      >

in  [ VectorExpr.Fixed { x = 1.0, y = 2.0, z = 3.0 }
    , VectorExpr.Position { from_frame = 399, to_frame = 0 }
    ]

In practice, I would expect to use something more like

let myproject = https://myproject.com/v1.0.0/types.dhall

in  [ myproject.VectorExpr.Fixed { x = 1.0, y = 2.0, z = 3.0 }
    , myproject.VectorExpr.Position { from_frame = 399, to_frame = 0 }
    ]

but I think that dhall-rust doesn’t currently resolve imports?

[ChristopherRabotin]

Excellent point.

Maybe I can implement this manually, i.e. not in the serde_dhall crate, by implement a custom serializer for the VectorExpr enum that first serializes the full enum as valid Dhall (starting with serialize_str) and then use the TupleVariant serialization).

[ChristopherRabotin]

The serializer takes care of fully defining the type if type annotations are given!

I will try the recursion in the morning for the CrossProduct, but it works great for the other enum variants.

The following test code outputs what follows it.

#[test]
    fn test_vector_expr_fixed() {
        let v = VectorExpr::Fixed {
            x: 1.0,
            y: 2.0,
            z: 3.0,
        };
        let v_str = serde_dhall::serialize(&v)
            .type_annotation(&build_type())
            .to_string()
            .unwrap();
        println!("{v_str:?}");
        let v_deser: VectorExpr = serde_dhall::from_str(&v_str).parse().unwrap();
        assert_eq!(v_deser, v); // This fails because I am not serializing it correctly.
    }

    #[test]
    fn test_vector_expr_state() {
        let pos = VectorExpr::Position {
            from_frame: FrameUid {
                ephemeris_id: 399,
                orientation_id: 0,
            },
            to_frame: FrameUid {
                ephemeris_id: 301,
                orientation_id: 0,
            },
        };

        let pos_str = serde_dhall::serialize(&pos)
            .type_annotation(&build_type())
            .to_string()
            .unwrap();
        println!("{pos_str:?}");
        let v_deser: VectorExpr = serde_dhall::from_str(&pos_str).parse().unwrap();
        assert_eq!(v_deser, pos);
    }

< Fixed: { x : Double, y : Double, z : Double } | Position: { from_frame : { ephemeris_id : Integer, orientation_id : Integer }, to_frame : { ephemeris_id : Integer, orientation_id : Integer } } | Velocity: { from_frame : { ephemeris_id : Integer, orientation_id : Integer }, to_frame : { ephemeris_id : Integer, orientation_id : Integer } } >.Position { from_frame = { ephemeris_id = +399, orientation_id = +0 }, to_frame = { ephemeris_id = +301, orientation_id = +0 } }

and

"< Fixed: { x : Double, y : Double, z : Double } | Position: { from_frame : { ephemeris_id : Integer, orientation_id : Integer }, to_frame : { ephemeris_id : Integer, orientation_id : Integer } } | Velocity: { from_frame : { ephemeris_id : Integer, orientation_id : Integer }, to_frame : { ephemeris_id : Integer, orientation_id : Integer } } >.Fixed { x = 1.0, y = 2.0, z = 3.0 }"

Recursion might be more challenging, we'll see.

@Nadrieril , if I get this to work in the serde-dhall crate, would you like me to open a PR? I'm asking because I know this crate isn't actively maintained.

[ChristopherRabotin]

Are only simple values and simple types supported in the Dhall library for now? I'm hitting a snag when trying to deserialize the type from @sellout : [this is neither a simple type nor a simple value:](https://github.com/Nadrieril/dhall-rust/blob/master/serde_dhall/src/value.rs#L229

If this is a limitation of the library, I think it may be more work than just adding the struct variants. That latter part is ready for a PR.

Although my understanding of Dhall is quite limited, I'm happy to help maintain the publication and upkeep of this library. It's used in production in several companies, so I'm happy to spend time helping out.

Edit: for my initial need, I can move the CrossProduct variant to its own VectorMath enum. This works for my use case even though it limits the recursion depth to 1.

[sellout]

Yeah, I think for dhall_serde, you’ll need to use the Topo encoding I mentioned before to get recursion to work with SimpleValue.¹

Footnotes

1. Topo won’t be able to encode pub struct Stream<T> { head: T, tail : Box<Stream<T>> }, in general, since it’s infinite. It could only encode a circular stream. ↩

[sellout]

The easiest would be to use Topo directly in Rust (like in https://recursion.wtf/posts/rust_schemes/), then dhall_serde doesn’t need to have some idiosyncratic Dhall types – it can stick with just matching the primitive types.

[Nadrieril]

Yep I would welcome a PR. Regarding the limitation to simple values, that's only a serde_dhall limitation; the dhall crate itself handles the full complexity of dhall (expect imports and anything that was added to dhall after I stopped maintaining the crate).