[Haskell-cafe] How to convert a list to a vector encoding its length in its type?

[David Menendez]

On Fri, Aug 21, 2009 at 2:50 PM, Jason Dagit<dagit at codersbase.com> wrote:
>> On Fri, Aug 21, 2009 at 2:03 PM, David Menendez<dave at zednenem.com> wrote:
>>>
>>> The problem is that the parameter, n, is part of the input to toPeano,
>>> but you need it to be part of the output. To rephrase slightly, you
>>> have
>>>
>>>    toPeano :: forall n. (Nat n) =>  Int -> n
>>>
>>> but you need,
>>>
>>>    toPeano :: Int -> exists n. (Nat n) => n
>
> Yes, that's exactly what I meant by my verbage above :)  Guess I
> should have explicitly used the forall/exists terminology.
>
>>>
>>> which states that toPeano determines the type of its return value. In
>>> Haskell, you can encode this with an existential data type,
>>>
>>>    data SomeNat where SomeNat :: (Nat n) => n -> SomeNat
>>>    toPeano :: Int -> SomeNat
>
> Okay, that's what we did with AnyVector.  What I don't understand is
> how you'll actually use this.  Once you create SomeNat, the type
> system no longer remembers which Nat.  So to me, you're back where you
> started.

I'm assuming you want toPeano and fromList to work on any possible
input. In that case, the context has to be able to work for any nat
type.

It's not quite true that the type system doesn't remember the nat:
it's bundled inside the data type, along with the class instance.
Depending on what operations are available, you can recover the type
as specifically as you want.

For example, it's perfectly valid to write a function with this type:

    testLength :: (Nat n) => SomeVector a -> Maybe (Vector a n)

which can then be used for distinguishing vectors of different lengths.

It's also possible to prove that two vectors have the same (unknown)
length and then use that fact elsewhere.

data a :==: b where Eq :: a :==: a

eqLengths :: Vector a n -> Vector b m -> Maybe (n :==: m)
eqLengths Nil Nil = Just Eq
eqLengths (_ :*: as) (_ :*: bs) = do
    Eq <- eqLengths as bs
    return Eq
eqLengths _ _ = Nothing


zipVectors :: Vector a n -> Vector b n -> Vector (a,b) n


foo v1 v2 =
    case v1 of
        SomeVector v'1 ->
            case v2 of
                SomeVector v'2 ->
                    case eqLengths v'1 v'2 of
                        Nothing -> error "Something has gone wrong!"
                        Just Eq -> let v3 = zipVectors v'1 v'2 in ...

>>> or, equivalently, by using a higher-order function.
>>>
>>>    toPeano :: Int -> (forall n. Nat n => n -> t) -> t
>
> This looks a bit more promising.

It's an illusion; the two forms are inter-convertible.

toPeanoX :: Int -> SomeNat
toPeanoK :: Int -> (forall n. (Nat n) => n -> t) -> t

toPeanoX n   = toPeanoK n SomeNat
toPeanoK n k = case toPeanoX n of (SomeNat n) -> k n

> I guess you end up writing your program inside out in a sense which is
> fine, but then how do you address the forgetfulness?

You can't forget something you never knew in the first place. At
compile-time, the length of the list isn't known, so it can't be
reflected in the type.

-- 
Dave Menendez <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>