Hi Roman, On Tue, Oct 9, 2012 at 12:11 PM, Roman Cheplyaka <r...@ro-che.info> wrote: > 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
