[Haskell-cafe] Type of scramblings
roma at ro-che.info
Tue Oct 9 11:11:11 CEST 2012
I am reading through Oleg's "Eliminating translucent existentials".
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?
More information about the Haskell-Cafe