Recursive data types

[dhall-lang]

Recursive data types

[Gabriella439]

@mwgkgk: You might also find these resources helpful, too:

• Automatic synthesis of typed Λ-programs on term algebras - The original paper that this is based on
• Data is Code - A post I wrote describing this trick in the context of morte/annah (the predecessors of dhall)

[jberryman]

Is there any way (in theory) to hide the complexities of translating recursive types in some syntactic sugar or language feature? I'm just getting started with dhall and have a really poor intuition for this.

[ocharles]

I just ran into this and would love for this to be at least documented somewhere, perhaps a FAQ?

My use case was wanting to encode what a Nix derivation is, in Dhall. I started with (in Derivation.dhall)

{
  require : List ./Derivation.dhall
}

and got immediately stuck.

In my case, knowing how to translate

data A = A { as :: [a], b :: B }

Would be very helpful.

[Gabriella439]

I added a guide on how to do this to the Dhall wiki:

https://github.com/dhall-lang/dhall-lang/wiki/How-to-translate-recursive-code-to-Dhall

... and I also mention this in the Haskell tutorial's FAQ section in this pull request:

dhall-lang/dhall-haskell#223

This is part of an effort to get more documentation migrated to the language-independent Dhall wiki

Once that pull request is merged then I'll mark this closed

[Gabriella439]

@jberryman: There might be some things we could do to make the type-level representation easier to read, but the term-level implementation stuff is going to be difficult to simplify

[Gabriella439]

@kevroletin: There is a special tree-like recursive structure which dhall-to-yaml supports which is the Prelude.JSON.Type type:

https://store.dhall-lang.org/Prelude-v20.2.0/JSON/Type.dhall.html

… so this is one way that you could encode a Dhall data structure that produces that result:

-- ./example.dhall

let JSON = https://prelude.dhall-lang.org/JSON/package.dhall

let MakePerson
    : { children : List JSON.Type, name : Text } → JSON.Type
    = λ(x : { children : List JSON.Type, name : Text }) →
        JSON.object
          ( toMap
              { children = JSON.array x.children, name = JSON.string x.name }
          )

let example
    : JSON.Type
    = MakePerson
        { name = "John"
        , children =
          [ MakePerson { name = "Mary", children = [] : List JSON.Type }
          , MakePerson { name = "Jane", children = [] : List JSON.Type }
          ]
        }

in  example

$ dhall-to-yaml --file example.dhall

children:
  - children: []
    name: Mary
  - children: []
    name: Jane
name: John

[Profpatsch]

My use case is specifying a small eDSL for (reactjs) slides in dhall and translating them to HTML afterwards.

[Gabriella439]

It is definitely possible! Although the language doesn't provide built-in support for recursive types, you can still encode them within the language using a mechanical translation process, like this:

$ cat Node 
    let Node : Type =
            ∀(Node : Type)
        →   ∀(  Recurse
            :   < Plain   : Text
                | Heading : { level : Natural, heading : Text }
                | Listing : List Node
                >
            →   Node
            )
        →   Node
in  Node

$ cat Plain
    let Plain : Text → ./Node =
            λ(x : Text)
        →   λ(Node : Type)
        →   λ(  Recurse
            :   < Plain   : Text
                | Heading : { level : Natural, heading : Text }
                | Listing : List Node
                >
            →   Node
            )
        →   Recurse
            < Plain   = x
            | Heading : { level : Natural, heading : Text }
            | Listing : List Node
            >
in  Plain

$ cat Heading 
    let Heading : { level : Natural, heading : Text } → ./Node =
            λ(x : { level : Natural, heading : Text })
        →   λ(Node : Type)
        →   λ(  Recurse
            :   < Plain   : Text
                | Heading : { level : Natural, heading : Text }
                | Listing : List Node
                >
            →   Node
            )
        →   Recurse
            < Heading = x
            | Plain   : Text
            | Listing : List Node
            >
in  Heading

$ cat Listing 
    let map = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/map

in  let Listing : List ./Node → ./Node =
            λ(x : List ./Node)
        →   λ(Node : Type)
        →   λ(  Recurse
            :   < Plain   : Text
                | Heading : { level : Natural, heading : Text }
                | Listing : List Node
                >
            →   Node
            )
        →   let f : ./Node → Node =
                λ(x : ./Node) → x Node Recurse
        in  Recurse
            < Listing = map ./Node Node f x
            | Plain   : Text
            | Heading : { level : Natural, heading : Text }
            >
in  Listing

... and here is an example of how a user would use this:

$ cat example
./Listing
[   ./Plain "ABC"
,   ./Listing
    [   ./Heading { level = +0, heading = "foo" }
    ,   ./Listing
        [   ./Heading { level = +1, heading = "bar" }
        ]
    ,   ./Plain "DEF"
    ]
,   ./Plain "GHI"
]

... which normalizes to:

$ dhall <<< './example'
∀(Node : Type) → ∀(Recurse : < Heading : { heading : Text, level : Natural } | Listing : List Node | Plain : Text > → Node) → Node

λ(Node : Type) → λ(Recurse : < Heading : { heading : Text, level : Natural } | Listing : List Node | Plain : Text > → Node) → Recurse < Listing = [Recurse < Plain = "ABC" | Heading : { heading : Text, level : Natural } | Listing : List Node >, Recurse < Listing = [Recurse < Heading = { heading = "foo", level = +0 } | Listing : List Node | Plain : Text >, Recurse < Listing = [Recurse < Heading = { heading = "bar", level = +1 } | Listing : List Node | Plain : Text >] : List Node | Heading : { heading : Text, level : Natural } | Plain : Text >, Recurse < Plain = "DEF" | Heading : { heading : Text, level : Natural } | Listing : List Node >] : List Node | Heading : { heading : Text, level : Natural } | Plain : Text >, Recurse < Plain = "GHI" | Heading : { heading : Text, level : Natural } | Listing : List Node >] : List Node | Heading : { heading : Text, level : Natural } | Plain : Text >

... or formatted for readability:

    λ(Node : Type)
→   λ(Recurse : < Heading : { heading : Text, level : Natural } | Listing : List Node | Plain : Text > → Node)
→   Recurse < Listing =
        [ Recurse < Plain = "ABC" | Heading : { heading : Text, level : Natural } | Listing : List Node >
        , Recurse < Listing =
            [ Recurse < Heading = { heading = "foo", level = +0 } | Listing : List Node | Plain : Text >
            , Recurse < Listing =
                [ Recurse < Heading = { heading = "bar", level = +1 } | Listing : List Node | Plain : Text >
                ] : List Node | Heading : { heading : Text, level : Natural } | Plain : Text >
            , Recurse < Plain = "DEF" | Heading : { heading : Text, level : Natural } | Listing : List Node >
            ] : List Node | Heading : { heading : Text, level : Natural } | Plain : Text >
        , Recurse < Plain = "GHI" | Heading : { heading : Text, level : Natural } | Listing : List Node >
        ] : List Node | Heading : { heading : Text, level : Natural } | Plain : Text >

[Gabriella439]

Actually, thinking about this more, it might be easier to just hand-write the latter form. In other words, just introduce the two bound variables:

    λ(Node : Type)
→   λ(Recurse : < Heading : { heading : Text, level : Natural } | Listing : List Node | Plain : Text > → Node)
→   ...

... and then wrap each level of nesting in Recurse when defining the nested data type

[Gabriella439]

I forgot to mention that if you don't care about using anonymous unions specifically, there is a less verbose encoding:

    λ(Node : Type)
→   λ(Plain : Text → Node)
→   λ(Heading : { level : Natural, heading : Text } → Node)
→   λ(Listing : List Node → Node)
→   Listing
    [   Plain "ABC"
    ,   Listing
        [   Heading { level = +0, heading = "foo" }
        ,   Listing
            [   Heading { level = +1, heading = "bar" }
            ]
        ,   Plain "DEF"
        ]
    ,   Plain "GHI"
    ]

That's probably easier to read and directly manipulate

[Profpatsch]

Oh! That looks like a GADT.

[Profpatsch]

Wait; how can I create something → Node then? e.g. what would a valid definition of Plain be?

Update: And how would I marshal it into a Haskell data afterwards?

[Gabriella439]

So the type of ./Node would be:

-- ./Node

    ∀(Node : Type)
→   ∀(Plain : Text → Node)
→   ∀(Heading : { level : Natural, heading : Text } → Node)
→   ∀(Listing : List Node → Node)
→   Node

... and then you would implement Plain as:

-- ./Plain

let Plain : Text → ./Node =
        λ(x : Text)
    →   λ(Node : Type)
    →   λ(Plain : Text → Node)
    →   λ(Heading : { level : Natural, heading : Text } → Node)
    →   λ(Listing : List Node → Node)
    →   Plain x

in  Plain

Marshaling it into Haskell data via Interpret would be trickier, but still possible. You wouldn't be able to do it by just deriving Generic and Interpret. Instead, you would have to hand-write the Interpret instance that loops over the syntax tree, like this:

data Node
  = Plain Text
  | Heading { level :: Int, heading :: Text }
  | Listing [Node]

instance Interpret Node where
    autoWith options = Type {..}
      where
        -- Actually, this is not completely correct as you need to handle the more general case where
        -- `"Node"` is α-renamed to another type variable
        expected =
            Pi "Node" Type (Pi _ (Pi _ Text "Node") ...)

        -- Same thing here: you need to handle the more general case where the lamba-bound
        -- variables are renamed, or if any of the names shadow each other
        extract (Lam "Node" _ (Lam "Plain" _ (Lam "Heading" (Lam "Listing" _ e0)))) = buildNode e0
        extract _ = Nothing
          where
            buildNode (App (Var (V "Plain 0)) (TextLit t)) = Just (Plain t)
            ...
            buildNode _ = Nothing

The basic idea is that once you skip all the lambdas in the syntax tree it's basically a very verbose encoding of your data type using Dhall's syntax tree and buildNode just loops over that and marshals it into the Haskell Node type, returning Nothing if it runs into something unexpected

[Profpatsch]

That’s all very verbose. I definitely wouldn’t have found out how to unmarshal into Haskell.

I suspect the explicit Recurse method above would involve a similar manual Interpret instance as well?

[Gabriella439]

Yes, the explicit Recurse method would also require a manual Interpret instance, too

[Profpatsch]

Hm, do you think it would be possible to write these instances once for any kind of correctly formatted Dhall-expression? e.g. by interpreting into Fix?

[Gabriella439]

I don't think it's possible mainly due to a limitation in how GHC.Generics work. In fact, you'll notice that the dhall library actually already lets you derive an Interpret instance for a recursive type without any complaints, but if you try to use the instance the program will crash with a stack overflow

The problem is that GHC.Generics has a very simplistic way of dealing with recursion so that if you define a type like:

data Stream = Stream { head :: Integer, tail :: Stream }

... then the derived Interpret implementation will try to decode the following infinite type:

{ head : Integer, tail : { head : Integer, tail : { head : Integer, tail : ...

As far as I can tell there is no way to do something smarter with the GHC.Generics machinery

[ocharles]

Ok, I think it's this:

Derivation.dhall:

let Derivation : Type =
      forall (Derivation : Type) ->
	  forall (MkDerivation : List Derivation -> Derivation) ->
	  Derivation
in Derivation

And derivation.dhall:

let map = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/map 
in  
let derivation : List ./Derivation.dhall -> ./Derivation.dhall =
      \(inputs : List ./Derivation.dhall) ->
      \(Derivation : Type) ->
      \(MkDerivation : List Derivation -> Derivation) ->
      let f : ./Derivation.dhall -> Derivation = 
            \(x : ./Derivation.dhall) -> x Derivation MkDerivation in
      MkDerivation (map ./Derivation.dhall Derivation f inputs)
in derivation

[Gabriella439]

@ocharles: Yes, that's correct. You basically assume that you have the constructor for the recursive type.

I would only suggest a slightly different approach that is a little simpler to encode. Using a modified version of the example you asked for:

data A = MkA { children :: [A], name :: Text }

The Dhall encoding of that type would be:

∀(A : Type) → ∀(MkA : { children : List A, name : Text } → A) → A

And this would be an example value of that type:

  λ(A : Type)
→ λ(MkA : { children : List A, name : Text } → A)
→ MkA
  { children =
      [ MkA { children = [] : List A, name = "John" }
      , MkA { children = [] : List A, name = "Mary" }
      ]
  , name     = "Ted"
  }

I can add an example like that to the FAQ section

[ocharles]

Ah yes, that makes sense. 👍 to a FAQ entry, if we don't get some first class syntax for this.

[mwgkgk]

Is it possible to import children in the above example?

  λ(A : Type)
→ λ(MkA : { children : List A, name : Text } → A)
→ MkA
  { children =
      [ ./value2.dhall
      , MkA { children = [] : List A, name = "Mary" }
      ]
  , name =
      "Ted"
  }

Where value2.dhall is simply

MkA { children = [] : List A, name = "John" }

This throws Unbound variable MkA.

I cannot say that I'm 100% confident in what's going on though, and how to achieve uniform look for values that form a dependency graph while spread over a catalogue of files.

[Gabriella439]

@mwgkgk: Dhall does not support importing "open" expressions (i.e. expressions with free variables), but there might be another solution to what you have in mind

You can create separate importable files that behave equivalently to the corresponding types and constructors. The general trick for this is known as Boehm-Berarducci encoding and was created for the purpose of being able to separate each type and term into its own "closed" expression (i.e. an expression with no free variables) while still supporting things like recursion.

Using the example you gave, the way you would split this into multiple files would be:

-- ./A

    let A
        : Type
        = ∀(A : Type) → ∀(MkA : { children : List A, name : Text } → A) → A

in  A

-- ./MkA

    let map =
          https://raw.githubusercontent.com/dhall-lang/Prelude/e44284bc37a5808861dacd4c8bd13d18411cb961/List/map

in  let MkA
        : { children : List ./A, name : Text } → ./A
        =   λ(oldInput : { children : List ./A, name : Text })
          → λ(A : Type)
          → λ(MkA : { children : List A, name : Text } → A)
          →     let adapt : ./A → A = λ(a : ./A) → a A MkA

            in  MkA
                (   { children = map ./A A adapt oldInput.children }
                  ∧ oldInput.{ name }
                )

in  MkA

-- ./example

    let example : ./A = ./MkA { children = [] : List ./A, name = "John" }

in  example

-- ./example2

    let example2
        : ./A
        = ./MkA
          { children =
              [ ./MkA { children = [] : List ./A, name = "John" }
              , ./MkA { children = [] : List ./A, name = "Mary" }
              ]
          , name =
              "Ted"
          }

in  example2

$ dhall <<< './example'
∀(A : Type) → ∀(MkA : { children : List A, name : Text } → A) → A

  λ(A : Type)
→ λ(MkA : { children : List A, name : Text } → A)
→ MkA { children = [] : List A, name = "John" }

$ dhall <<< './example2'
∀(A : Type) → ∀(MkA : { children : List A, name : Text } → A) → A

  λ(A : Type)
→ λ(MkA : { children : List A, name : Text } → A)
→ MkA
  { children =
      [ MkA { children = [] : List A, name = "John" }
      , MkA { children = [] : List A, name = "Mary" }
      ]
  , name =
      "Ted"
  }

[mwgkgk]

This is sort of amazing. I find that I struggle a lot with the signatures here, but it is likely expected.

(Commenting to express appreciation rather than request further help.)

[denizdogan]

Are improvements to this aspect of Dhall on a roadmap somewhere? I don't mean to complain at all, and this is a bit over my head when it comes to type theory, but this is the first time I think "well...that's a bummer."

The smart constructor feature goes a long way for the end-users, but if you're working with complex record structures, the smart constructors themselves can become unreadable to the point where I almost go "you can't do that in Dhall".

So having imagined that this should be possible:

let Person = { name : Text, children: List Person }

...this doesn't taste quite as good:

let Person
    : Type
    = ∀(Person : Type) →
      ∀(MakePerson : { children : List Person, name : Text } → Person) →
        Person

let MakePerson
    : { children : List Person, name : Text } → Person
    = λ(x : { children : List Person, name : Text }) →
      λ(_Person : Type) →
      λ(MakePerson : { children : List _Person, name : Text } → _Person) →
        let adapt
            : Person → _Person
            = λ(y : Person) → y _Person MakePerson

        in  MakePerson
              (x with children = List/map Person _Person adapt x.children)

[Gabriella439]

@denizdogan: Yeah, the main issue is that it's really difficult to add language support for recursion while keeping the language total. This is compounded by the fact that we need to support multiple language bindings and it's already hard enough as it is to implement a new language binding

[kevroletin]

@Gabriel439
AFAIU in the examples above

• in dhall we represented a recursive data structure as code
• in dhall we interpreted "data as code" into a flat list
• in Haskell we interpreted "data as code" into a recursive tree

I am trying to generate a config like the below from dhall. Can I do it without using Haskell just with dhall-to-yaml? The resulting yaml (or json) contains a representation of a tree:

- name: John
  children: 
    - name: Mary
      children: []
    - name: Jane
      children: []

The imaginary use cases for such configs are:

• build pipelines : one might represent parallel build steps as children of a parent node
• expressing inclusion relationships for events (for example a monitoring tool might use it to produce reports)

I am very new to dhall but I see that it supports a list (which is a recursive data structure). Maybe there might be a [magic] implementation of a tree data structure?