Would it be possible to make a typelevel fix point...

# functional

[tschuchort]

Would it be possible to make a typelevel fix point combinator in Kotlin? (Similar to Haskell's `Fix`/`Mu`). I'm think about implementing something like data types à la carte.

[raulraja]

I’m sure we can figure it out with a compiler plugin. What is the data types a la carte encoding with Fix/Mu look like?

[raulraja]

I’m encoded data types a la carte with coproducts and Free but not sure how it deffers from the encoding you are looking at

[raulraja]

The encoding with Coproduct is very inefficient dispatching ops

[pakoito]

we have them already in arrow-recursion

[tschuchort]

The basic idea is this: You have a recursive data type of some kind:
data Exp = Const Int | Add Exp Exp
Later on you want to have another data type, that is very similar to your existing data type, except you want to add some information. For example wrap all value constructors in another type to annotate every "node" of the "tree" that is an instance of this data type. If the data type were not recursive you could just do:`data LineNr a = LineNr Int a` But this annotates only one level of the tree. All inner nodes will still be just Exp not LineNr. The core idea is to solve this by wrapping Exp in LineNr before the recursive knot is tied, and then do the recursion later with `Fix`:

data ExpF a = Const Int | Add a a
data LineNr a = LineNr Int a
type Exp = Fix (LineNr ExpF)

The rest of "data types a la carte" is to define each case as it's own type (instead of a type constructor in one larger type) and combine them using a coproduct type. Interpreters for each case are defined as a type class. You can then get an interpreter for any arbitrary coproduct using the initial F-algebra IIRC.

[raulraja]

We have these in the recursion schemes lib

[raulraja]

https://arrow-kt.io/docs/0.10/recursion/intro/

[raulraja]

In which you'd use the Coalgebra and Algebra of the recursive ADT to derive the more concrete ops in the tagless final interpreter. You can use IO and Traverse instances of the algebra in the encoding as well since the last is Foldable.

[raulraja]

Same as with Free monads that make any F stack safe even for eager data type at the cost of extra allocations

[Jannis]

Recursion schemes changed a bit a while ago and I did not document them that well yet, there are examples but that's about it. If you have any questions how it works feel free to ask me ^^