Recursive algebraic data types

[oxinabox]

I would like to create e.g. a linked list. But the following doesn't work:

data LinkedList a:Type = 
    Nil
    Cons val:a tail:LinkedList

:p Cons 1 Nil

the declaration gives a

Error: variable not in scope: LinkedList

    Cons val:a tail:LinkedList
                    ^^^^^^^^^^

[dougalm]

Yes, we don't have either recursive functions or recursive ADTs yet. It was a deliberate choice to de-prioritize them. They're fundamental to traditional functional programming, but Dex emphasizes arrays and iteration instead of linked lists and recursion. We want to add them at some point. Let's keep this open to track it.

[tscholak]

Hi, before the holidays I finally found some time to read all of the dex papers. I understand that there are quite a few obstacles to general recursion due to the approach taken by dex. Where would one start? If general recursion proves too difficult to achieve, would it makes sense to look at recursion schemes first/instead?

[apaszke]

Great question! Dex already features a while loop, which is kind of like recursion if you squint hard enough. Certainly all tail recursive functions could be translated into a while loop. More general recursion should be possible to handle too, but it will likely require generating stack-like data structures that will be modified in the loop. Some time ago I've been pointed to this nice writeup that outlines how a similar transform could be performed.

I haven't thought too much about recursion schemes yet, but it might actually be a very promising direction. We might be able to get nice things (e.g. predictable nested data parallelism) out of the additional regularity we wouldn't get in the general case.

In any case, I'd love us to get moving on this issue. Let's talk if you're interested!

[tscholak]

Hi Adam, I've had a look at the writeup you linked to. I'm familiar with defunctionalization. It's used to get around a long-standing ghc limitation of not being able to partially apply type families. The singletons library makes heavy use of this and has automated it. The article also talks about the CPS transformation and the defunctionalization of the continuation. To me, this looks suspiciously like trampolining, which underlies the Free monad. I'd be happy to talk more about this!