oleg at okmij.org oleg at okmij.org
Sat Oct 13 00:20:19 CEST 2012

```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.

```