# Type of scramblings

3 messages
Open this post in threaded view
|

## Type of scramblings

 I am reading through Oleg's "Eliminating translucent existentials"[1]. [1]: http://okmij.org/ftp/Computation/Existentials.html#eliminating-translucentHe 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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe