[Haskell-cafe] Type of scramblings
dipython at gmail.com
Thu Oct 11 17:15:50 CEST 2012
On Tue, Oct 9, 2012 at 12:11 PM, Roman Cheplyaka <roma at ro-che.info> wrote:
> I am reading through Oleg's "Eliminating translucent existentials".
> : http://okmij.org/ftp/Computation/Existentials.html#eliminating-translucent
> He draws a distinction between
> forall a . [a] -> [a]
> 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
> 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
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe