recursive data type - Dhall

I'm a Dhall newbie and am already stuck with recursive data types. I've tried reading https://docs.dhall-lang.org/howtos/How-to-translate-recursive-code-to-Dhall.html#recursive-record and https://docs.dhall-lang.org/howtos/How-to-translate-recursive-code-to-Dhall.html#recursive-sum-type and neither of them make sense to me. The unicode characters in the code-snippets are making things even harder.

What's going on there? Is that using RankNTypes or something in Dhall?

Are there any more examples available elsewhere? If I'm creating a config-file that I want end-users to use, do they have to deal with this complication? Can it be hidden away? And if it can, is there some library or function that already does this? And gives a straighforward way to use recursive data-types in Dhall?

It's been a while since I looked at this stuff but maybe I can help

What's tripping you up exactly?

It's not any easier but might be fun to look at. My friend Greg did up a recursion-schemes approach to recursive data types in Dhall: https://github.com/sellout/dada

Also, something to think about is that you may not _want_ to write a recursive type because you'll have to jump through these hoops

Maybe your config could be simplified

I'm writing a config file that needs to represent the navigation structure of a website. Which means that a Page type needs to have Page children. Is there any way to avoid recursion in the first place?

@Fintan Halpenny is this what you're referring to - https://github.com/sellout/dada/blob/master/Recursive/Type ? This is equally opaque to me :-(

Ya, maybe don't use dada :sweat_smile:

Maybe you could have Link which is a morally a pointer to a Page and a Page is just a List Link?

But let's say you do have a Page that has children, then it sounds exactly like the Person example you linked above

What part of that example is tripping you up?

the entire syntax. What's going on with the type declaration _conceptually_ and then what's going on when example is being declared. Why is the entire type reproduced there?

Is this using RankNTypes?

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

what is the exact Haskell transliteration of that snippet? Probably that will make it click for me.

my brain seems to be switching off as soon as I see ∀

Haha ok, so let's break it down into it's parts

let Person : Type a thing called Person that is a Type

If we look later in the post it says that the ∀(Person : Type) is different from the let Person

So this actually says ∀(_Person : Type): for all _Person which is a Type

The next line says ∀(MakePerson : { children : List _Person, name : Text } → _Person): We have a constructor MakePerson which consists of two components

The first is children, which is a List _Person. So, a list of the types we passed in originally with the ∀(_Person : Type)

And a name of type Text

Finally, we return this type _Person

What this translates into in Haskell is something like:

data Person person = { name: Text, children = [person] }

But if we try to use Person within Person we'd get Person (Person (Person ....)))

So the trick is that we need some sort of fixpoint structure that hides this away from us:

data Fix f = MakeFix { unFix :: f (Fix f) }

So, now we can say Person' = Fix Person

The final piece of the puzzle is that we want to "interpret" this structure into some target. To do this we fold over the Fix structure, peeling each layer off and applying some function to that layer

In the Dhall example, they're doing this by just collecting the names

Is any of that unclear to you?

To understand this more you may want to look up material on recursion schemes

this looks like a free monad of sorts to me.

at the end, will the end-user (writing the config file) need to deal with all this complexity?

so, Person is a type-level function that takes a type X another type-level function that uses that type X and finally gives as the type X

is that valid Dhall ^^

It's sort of related. You can imagine it's Free without the Pure constructor

I think you'd need the for all symbols for it be valid

I'm on the verge of giving up. Is there an example of a config file that uses recursive data-types? How much complexity is leaked to the end-users? Because if this makes things complex for the end-users as well, it's not worth the effort at all. I will be unable to use Dhall for my project.

Well, what are you trying to do?

Because if you're supplying dhall to the end user you're expecting them to also know how to work with Dhall

But only for defining config files. Which for most parts is defining records & lists, and probably using a few let bindings to reduce duplication.

I mean, isn't that one of the implicit (or explicit?) goals of Dhall? It should be easy to define configuration for casual users.

I don't foresee casual users defining their own types and suchlike.

or am I viewing Dhall the wrong way?

Nah, that makes sense :)

But if you want recursion you're going to have to jump through these hoops because Dhall is total

And so can't express recursion as we're used to

I mean if recursion is possible in any other way, then it is technically possible to have infinite recursion, right?

What you could do is make it easy to build up Pages and expose ways to interpret them into some final form

so being total, or not, doesn't really help.

Not _quite_. You can _represent_ structure that's infinite.

But whatever program that ingests the Dhall needs a way to interpret that infinite structure

But from Dhall's point of view, this all total and non-Turing complete

is it possible to have a polymorphc type such as data Page x = Page { title :: Text, children :: [x]} and later substitute x for Page?

That's exactly what the Dhall example is doing

but it seems way too complicated. I'm trying a simple version -- probably if I write it from scratch myself, it might make more sense.

what's the void / () type in Dhall?

You could make it simpler by having some function makePage which takes a title and a continuation of children

It's the empty record {}

what's the newbie error in this?

I'm not actually sure. It's been too long since I worked with Dhall

Started off with somthing like this

Ok, I think I cracked it

That'll be $100 for Dhall consultancy fees :stuck_out_tongue_closed_eyes:

Actually, you want to delay the x: Type even more

So that way you can keep chaining without adding specifying the x : Type

I can't seem to get this working:

let Site = ∀(x : Type) → { root : Text, pages : List x }

let Page = λ(root : Text) → λ(x : Type) → { root = root, pages = [] : List x }

let addPage =
        λ(parent : Site)
      → λ(root : Text)
      → λ(x : Type)
      → { root = (parent x).root, pages = [ Page root ] # (parent Site).pages }

let addPages =
        λ(parent : Site)
      → λ(pages : List Site)
      → λ(x : Type)
      → { root = (parent x).root, pages = pages # (parent Site).pages }

in  addPages (addPage (Page "abc") "def") [ Page "boo", Page "foo" ]

But maybe you play around with and get it going

There's also Dhall folks in the fpchat slack that are smart and know this stuff well. Including sellout :)

I tried playing around with it more and couldn't really make it usable

dada is where it's at but I can't remember how to use it :joy:

Did you notice this section in the documentation: https://docs.dhall-lang.org/howtos/How-to-translate-recursive-code-to-Dhall.html#smart-constructors

The smart constructors at least to me seem a lot more ergonomic

Ah I missed that section. But I think I ended up trying that. The issue was making a person with children

I'll take a closer look again when I'm back at a keyboard