Breaking recursion

[davidweichiang]

data Thing = One | Two;
define f: Thing -> () = \x. case Thing of One -> f Two | Two -> ();
f One

Currently the FGG backend sees that f is recursive and uses matrix inversion to find the sum-product. It would be nice if somehow it could recognize that the recursion is bounded and therefore avoid the matrix inversion.

An example of how the recursion could be transformed away is to specialize f for different arguments:

define f_One = f_Two;
define f_Two = ();
f_One

Maybe there are other ways too.

[davidweichiang]

Or maybe this would be better in the FGG backend.