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

# functionalt

tschuchort

04/18/2020, 11:08 AMWould 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.

r

raulraja

04/18/2020, 11:54 AMI’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

04/18/2020, 11:54 AMI’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

04/18/2020, 11:55 AMThe encoding with Coproduct is very inefficient dispatching ops

p

pakoito

04/18/2020, 12:09 PMwe have them already in arrow-recursion

t

tschuchort

04/18/2020, 12:19 PMThe 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`:
Copy code

```
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.r

raulraja

04/18/2020, 2:39 PMWe have these in the recursion schemes lib

raulraja

04/18/2020, 2:40 PMraulraja

04/18/2020, 2:47 PMIn 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

04/18/2020, 2:48 PMSame as with Free monads that make any F stack safe even for eager data type at the cost of extra allocations

j

Jannis

04/18/2020, 2:58 PMRecursion 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 ^^

3 Views