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 :sweat_smile:), 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 https://github.com/Nadrieril/dhall-rust/blob/d8c2e651c7eadb78a578c64ba70e3d319406b48c/serde_dhall/src/serialize.rs#L202. 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