I recently learned a bit about F-algebras: https://www.fpcomplete.com/user/bartosz/understanding-algebras. I wanted to lift this functionality to more advanced types (indexed and higher-kinded). Furthermore, I checked "Giving Haskell a Promotion" (http://research.microsoft.com/en-us/people/dimitris/fc-kind-poly.pdf), which was very helpful because it gave names to my own vague "inventions".
However, I cannot seem to create a unified approach that works for all shapes.
Algebras need some "carrier type", but the structure we're traversing expects a certain shape (itself, applied recursively), so I came up with a "Dummy" container that can carry any type, but is shaped as expected. I then use a type family to couple these.
This approach seems to work, leading to a fairly generic signature for my 'cata' function.
However, the other things I use (Mu, Algebra) still need separate versions for each shape, just for passing a bunch of type variables around. I was hoping something like PolyKinds could help (which I use successfully to shape the dummy type), but it seems it is only meant to work the other way around.
As IFunctor1 and IFunctor2 do not have extra variables, I tried to unify them by attaching (via type family) the index-preserving-function type, but this seems not allowed because of the existential quantification, so I'm left with multiple versions there too.
Is there any way to unify these 2 cases? Did I overlook some tricks, or is this just a limitation for now? Are there other things that can be simplified?
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Rank2Types