Recursive functions are usually defined by directly calling a function inside its own body.
Nat = Z | S Nat double Z = Z double (S x) = S (S (double x)))
What if, instead of defining them this way, we just enumerated two recursive datatypes and zipped them?
To be more descriptive, mind the following functions/types:
enum Nat = [Z, S Z, S S Z, S S S Z ...] elem (S S S Z) (enum Nat) = 3 [4,5,6] !! 1 = 5 zip [1,2,3] [4,5,6] = [(1,4), (2,5), (3,6)] # a b = \x -> (zip (enum a) (enum b)) !! (elem x (enum a))
enum enumerates elements of a recursive datatype,
zip are just as defined by Haskel. Now, using #, there is an interesting way to define some recursive functions.
Even = Z | S (S Even) double = Nat # Even
double equivalent to:
double x = [(0,0),(1,2),(2,4),(3,6)...] !! x
In other words, instead of defining the function recursively, we just created an infinite list with the input/output pairs of that function, by zipping two recursive datatypes together. I never heard of this approach being used, so my question is: this there a name for this? Any relevant papers? What kinds of functions can be defined this way?