Portability | non-portable (rank-2 polymorphism) |
---|---|
Stability | experimental |
Maintainer | Edward Kmett <ekmett@gmail.com> |
Martin Erwig's metamorphisms for indexed data types.
ADT fusion: snd c . fst c == id => erwig d id c . erwig c id d' = erwig d id d'
FreeMeta: l strict, snd c == snd c' == phi', fst d == fst d' == alpha, l . fst c = fst c' . fmap l, snd d' . rr = fmap r . snd d ==> l . (erwig d id c) = (erwig d' id c') . r