Type of scramblings

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

Type of scramblings

Roman Cheplyaka-2
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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type of scramblings

Marcelo Sousa-3
Hi Roman,

On Tue, Oct 9, 2012 at 12:11 PM, Roman Cheplyaka <[hidden email]> 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type of scramblings

oleg-30
In reply to this post by Roman Cheplyaka-2

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.


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe