8 Mar
2009
8 Mar
'09
4:16 a.m.
R J wrote:
Here's another Bird problem that's stymied me:
The function "inits" computes the list of initial segments of a list; its type is inits :: [a] -> [[a]]. What is the appropriate naturality condition for "inits"?
Just use the free theorem associated to type [a] -> [[a]] in Janis Voigtlaender’s free theorem generator http://linux.tcs.inf.tu-dresden.de/~voigt/ft and see the outcome when all permissible relation variables are functions (at the bottom of the screen). jno