To install and tinker:
cd your-scratch-directory
mkdir gpif-datakinds
cd gpif-datakinds
cabal sandbox init
git clone [email protected]:pbl64k/gpif-datakinds.git
cabal install gpif-datakinds/gpif-datakinds.cabal
Control.IxFunctor.Examples.Examples contains a few really sketchy examples,
Control.IxFunctor will import most of the stuff you need if you want to
tinker with your own data types, while Control.IxFunctor.Nat,
Control.IxFunctor.List, Control.IxFunctor.Rose and
Control.IxFunctor.EvenOdd contain sample definitions, isomorphisms and
concrete maps/recursion schemes for corresponding data types.
To generate some documentation of questionable utility:
mkdir docs
haddock -h -o docs/ `find gpif-datakinds/src/ -name '*.hs'`
Note that haddock seems to get a little confused by all of the extensions
this library is using, so some signatures look quite nonsensical. When in
doubt, look in the sources.
It's the same thing as Edward A. Kmett's recursion-schemes,
only more general and less practical. The problem is that Functors
(Bifunctors etc.) in Haskell sense of the word are not closed under Fix.
Not to mention the fact that it's not clear how to generalize to arbitrary
arities, apart from going the "no one's going to need a 15-tuple" route.
Mutual recursion also presents some problems.
I mused about this idly on reddit, when SUDDENLY, Conor McBride showed up and pointed me towards his slides on precisely this issue. I also found the unfinished Slicing It! of his. All of that was more than a little mind-boggling and seemed to require non-standard extensions I've never even heard of before.
Further research led me to Generic Programming with Indexed Functors by Andres Löh and José Pedro Magalhães (see also). That was in Agda, though, which has a strictly more powerful type system than Haskell, and which I'm not particularly familiar with.
Anyway, I tinkered with GPIF and Idris a bit
(that implementation is extensively commented, and could probably serve as introductory
reading on this topic), time passed, and meanwhile, nponeccop
suggested to me that DataKinds do the same thing as the relevant SHE features.
Unsurprisingly, I later found out that McBride has earlier suggested using DataKinds
for these purposes somewhere on SO as well.
But nothing that would qualify as even a remotely complete implementation
appeared to be available in Haskell. So I decided to suck it up and follow
the combination of Slicing It! and GPIF programs spiced up by DataKinds
myself. This is the end result of that effort.
The generality of this fascinates me. It also works quite well in simple cases. Conversions between host types and indexed functors can be encoded very neatly using the generic cata- and anamorphisms. Concrete maps and recursion schemes fall out of it simply by specifying the right types and letting the isomorphisms do the work.
Nevertheless, it's not very practical even in those simple cases. It's
just less work to write the recursion schemes needed from scratch. And the
going gets much, much tougher when we get to mutually recursive types,
as EvenOdd here illustrates...
So, this isn't intended for any kind (pardon the pun) of practical use, but I think that the insight into the nature of certain sorts of algebraic data types and their associated recursion schemes was entirely worth the trouble.