I am reading through Oleg's "Eliminating translucent existentials"[1]. [1]: http://okmij.org/ftp/Computation/Existentials.html#eliminating-translucent He draws a distinction between forall a . [a] -> [a] and forall a . [a]^n -> [a] as types of "scramblings". This is something I'm struggling to understand. First of all, I think here we're talking about total functions, otherwise there's no point in introducing dependent types. 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 (The condition `length xs == n` can be replaced by a similar condition that also works for infinite lists.) The functions `f` and `g` are equivalent in the sense that for any list `xs` of length `n` `f xs === g xs`. Thus, even though it seems that we allow more total functions by replacing `[a]` with `[a]^n`, that doesn't buy us any additional expressiveness. What am I missing? Roman
Hi Roman,
On Tue, Oct 9, 2012 at 12:11 PM, Roman Cheplyaka
I am reading through Oleg's "Eliminating translucent existentials"[1].
[1]: http://okmij.org/ftp/Computation/Existentials.html#eliminating-translucent
He draws a distinction between
forall a . [a] -> [a]
and
forall a . [a]^n -> [a]
as types of "scramblings". This is something I'm struggling to understand.
First of all, I think here we're talking about total functions, otherwise there's no point in introducing dependent types.
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
(The condition `length xs == n` can be replaced by a similar condition that also works for infinite lists.)
The functions `f` and `g` are equivalent in the sense that for any list `xs` of length `n` `f xs === g xs`. Thus, even though it seems that we allow more total functions by replacing `[a]` with `[a]^n`, that doesn't buy us any additional expressiveness.
What am I missing?
[a]^n -> [a] is a refinement of [a] -> [a]. The dependent type allows you to infer the number of transformations possible. In this case, the useful case is when n == 0, since with [a]^0 you know that there is only one possible transformation, namely id. In the case where n > 0 there is an infinite number of transformations because you can do countless drops and/or duplications so I think you don't get any additional expressiveness between both types. Regards, Marcelo
Roman
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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.
participants (3)
-
Marcelo Sousa -
oleg＠okmij.org -
Roman Cheplyaka