church-encoded Free monad

[mstksg]

Just following up on FormationAI/dhall-bhat/pull/48 :) Tried my best to shift this to match the format of dada. From the original PR, I've also added corecursive and a FreeF base functor, although I'm not sure where the best place to put FreeF is, or also the best name (I've noticed yaya/dada prefer to have more descriptive names than just MyFunctorF). Let me know if there's anything I can fix!

One exception to the explicit style guide mentioned in FormationAI/dhall-bhat/pull/49 is that I sometimes use inline imports in situations that parallel other similar usages in the rest of the repo.

[sellout]

I'm not sure where the best place to put FreeF is, or also the best name

This is actually 80% of the reason Free doesn’t yet exist in this repo 😆 – I’m not happy with any of the names for it. But FreeF is fine for now. It deserves to exist at least.

[sellout]

Thanks, @mstksg, looking forward to getting this in.

We’re in the right ballpark now. I showed some ways to integrate this more into the generalized recursion approach. Definitely haven’t done all the work for you, and I can help walk through some of the changes if they’re not clear.

And I know it looks like a bunch of changes, but it’s mostly just taking advantage of the existing library – your semantics stay the same.

[sellout]

This should now look like

λ(f : Type → Type) → λ(a : Type) → ../../Mu/Type (../../FreeF/Type f a)

Also, it doesn’t exist on master yet, but I’ve started putting types like this (i.e., recursive types) into a “data/” directory, so this would then be “data/Free/Type”. There are some examples of this on the kind-polymorphism branch.

[mstksg]

Hm, even though the two types are the same, I think there's some benefit in separating the fixed-point from the base functor. Basically like how we have List a and XNor, and we have Natural with Maybe, and we have NonEmpty and AndMaybe. And one benefit in implementing Free directly is that we can work directly with Free as a "normal function", instead of importing an intermediate data type to use it.

(edit: Although, now that I think about it, merge doesn't require importing constructor names, so it'd be possible to "make" a Free value without importing FreeF, but you'd need to import FreeF to use a Free value.)

In the end it might just be a stylistic thing, and I think there could be benefits both ways.

[sellout]

And this can be

  λ(f : Type → Type)
→ ../../Mu/functor (../../FreeF/Type f) (../../FreeF/bifunctor f)

[mstksg]

Trying this out with the alternative representation; this doesn't quite work because it requires Functor f. We can implement it directly using the FreeF implementation, but we just can't do it through Mu FreeF, unfortunately :(

[sellout]

This can be

  λ(f : Type → Type)
→ λ(a : Type)
→  ../../Mu/recursive (../../FreeF/Type f a)

[sellout]

  λ(f : Type → Type)
→ λ(monad : Monad f) -- note instance immediately after type
→ λ(a : Type)
→ ./recursive.cata
  a
  (  λ(free : ../../FreeF/Type f a (f a))
   → merge { Pure = monad.pure, Free = join } free)

and the merge would be cleaner if I ever got my changes into the spec, then it could be

→ ./recursive.cata (f a) (merge { Pure = monad.pure, Free = join })

[sellout]

Basically, anything that applies m is going to instead do ./recursive.cata … merge

[sellout]

  λ(f : Type → Type)
→ λ(a : Type)
→  ../../Mu/steppable (../../FreeF/Type f a)

[sellout]

This should probably look similar to the Free/retract one I proposed.

[mstksg]

I've made some stylistic adjustments re: imports, and added bifunctor for FreeF.

I've held back from changing Free f to be Mu (FreeF f a), since we can't actually implement most things in terms of Mu, which requires Functor f for most things. It also complicates functor a lot even if we write it in scratch without going through Mu/functor. However, I did take some inspiration using Mu's instances to implement Free's instances; I added toMu and fromMu, which are used to implement recursive and steppable in terms of Mu's instances. This is fine because recursive and steppable already require Functor anyway, and there's no way to get around the constraint even working with the original representation.

[sellout]

@mstksg Sorry, I didn’t mean to let this languish after your previous response, but I haven’t had a chance to get back to it.

To address your most recent point:

The requirement of Functor f is a bug. I have a different branch with a better Mu/functor, but even that currently requires Functor f in the case of FreeF, because it uses Bifunctor/first, and FreeF/bifunctor (correctly) requires Functor f.

Instead, Mu/functor should require Functor (\(a : Type) -> f a b) which can be satisfied by FreeF/bifunctor, or can be implemented directly, which would allow us to avoid the Functor f requirement imposed by FreeF/bifunctor.