Sorry for a late reply. > There are of course more total functions of type `[a]^n -> [a]` than of type > `[a] -> [a]`, in the sense that any term of the latter type can be assigned > the > former type. But, on the other hand, any total function `f :: [a]^n -> [a]` > has an "equivalent" total function > > g :: [a] -> [a] > g xs | length xs == n = f xs > | otherwise = xs
That is correct. It is also correct that f has another "equivalent" total function g2 :: [a] -> [a] g2 xs | length xs == n = f xs | otherwise = xs ++ xs and another, and another... That is the problem. The point of the original article on eliminating translucent existentials was to characterize scramblings of a list of a given length -- to develop an encoding of a scrambling which uses only simple types. Since the article talks about isomorphisms, the encoding should be tight. Suppose we have an encoding of [a] -> [a] functions, which represents each [a] -> [a] function as a first-order data type, say. The encoding should be injective, mapping g and g2 above to different encodings. But for the purposes of characterizing scramblings of a list of size n, the two encodings should be regarded equivalent. So, we have to take a quotient. One may say that writing a type as [a]^n -> [a] was taking of the quotient. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe