Naturality condition for inits
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"? The only discussion in the text concerning naturality conditions concerns map, where the naturality conditions are stated in what seem to be quasi-commutativity laws over the composition operator, as follows: f . head = head . map f, where f is strict (i.e., f _|_ = _|_) map f . tail = tail . map f map f (xs ++ ys) = map f xs ++ map f ys map f . reverse = reverse . map f map f . concat = concat . map (map f) I believe that none of the following naturality conditions, extrapolated from those above, hold: a. head . inits = inits [head] b. tail . inits = inits . tail c. reverse . inits = inits . reverse d. concat . inits = inits . concat In case the definition of "inits" is relevant, my definition is: inits :: [a] -> [[a]] inits xs = [take n xs | n <- seglengths] where seglengths = [0..length xs] Thanks. _________________________________________________________________ Windows Live™: Life without walls. http://windowslive.com/explore?ocid=TXT_TAGLM_WL_allup_1a_explore_032009
On Sat, 2009-03-07 at 22:18 +0000, 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"?
A natural transformation is between two Functors f and g is a polymorphic function t :: (Functor f, Functor g) => f a -> g a. The naturality condition is the free theorem which states*: for any function f :: A -> B, t . fmap f = fmap f . t Note that fmap is being used in two different instances here. For lists, fmap = map and so we have for any polymorphic function [a] -> [a] using reverse as a representative, map f . reverse = reverse . map f. inits is a natural transformation between [] and [] . [] (where . is type-level composition and not expressible in Haskell). Functors compose just by composing their fmaps, so fmap for [] . [] is simply map . map, therefore the naturality condition for inits is the following: for any function f :: A -> B, inits . map f = map (map f) . inits which you can easily prove. * Actually there are some restrictions relating to bottom.
Am Samstag, 7. März 2009 23:18 schrieb R J:
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"?
The only discussion in the text concerning naturality conditions concerns map, where the naturality conditions are stated in what seem to be quasi-commutativity laws over the composition operator, as follows:
f . head = head . map f, where f is strict (i.e., f _|_ = _|_) map f . tail = tail . map f map f (xs ++ ys) = map f xs ++ map f ys map f . reverse = reverse . map f map f . concat = concat . map (map f)
I believe that none of the following naturality conditions, extrapolated from those above, hold:
a. head . inits = inits [head] b. tail . inits = inits . tail c. reverse . inits = inits . reverse d. concat . inits = inits . concat
How does inits interplay with (map f)? Though inits . tail =/= tail . inits, there is an interesting relation between inits (tail xs) and inits xs, which? When you also consider the function tails, there is an interesting relation involving inits and reverse, too.
In case the definition of "inits" is relevant, my definition is:
inits :: [a] -> [[a]]
inits xs = [take n xs | n <- seglengths]
where
seglengths = [0..length xs]
Better define it recursively. inits [] = [[]] inits (x:xs) = []:map (x:) (inits xs)
Thanks.
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
participants (4)
-
Daniel Fischer -
Derek Elkins -
J.N. Oliveira -
R J