How to use function withSizedList?

Question

I know this is a little vague question but I have tried to find an answer and I couldn't.

Can any one provide a single reasonable example on how to use the function withSizedList from vector-sized package?

The context is that I am building some french deck package. I've decided to go into type level programming with this, moving from vector to vector-sized... Obviously, all my code broke after the change, but I manage to fix it except for the test suit. I have some quickcheck tests checking things like sort (shuffle deck) == sort deck.

This is very simple to do with regular vector as you can make and Arbitrary instance for Card and then quickcheck provides the instance for [Card]; and finally you just write a property like deck -> let vdeck = V.fromList deck ... This becomes pretty much impossible with vector-sized as the sized is unknown at compile time... Apparently this can be overcome with the function withSizedList which up to the documentation

converts a list into a vector with the proper size parameter, determined at runtime

(rant on) The problem is that I couldn't find a reverse dependency using such a function and the type signature is more of an Egyptian Jerogliphic than actual usefull information (rant off). I'd say that the way to use it is something like

-- within the conext of defining a quickcheck property. Card has a good Arbitrary instance
-- shuffle :: KnownNat n => Vector n Card -> Vector n Card (there is a random generator irrelevant for the example)
-- sort :: KnownNat n => Vector n Card -> Vector n Card

prop $ \(deck :: [Card]) -> 
   let shuffled_sized_deck = deck `VSized.withSizedList` shuffle
       sorted_sized_deck   = deck `VSized.withSizedList` sort
    in sort shuffled_sized_deck == sorted_sized_deck


-- In case you wonder, shuffle is implemented using withVectorUnsafe so
-- the type (Vector n) doesn't guarantee they have the same length

But I get the error

• Couldn't match type ‘r’ with ‘Vector n ’
  Expected: V.Vector n Card -> r
   Actual: V.Vector n Card -> V.Vector n Card

So... why not r ~ V.Vector n Card?? I hope the question is well explained. Type level programming breaks my head so badly, I don't know if the question is stupid or not.

Answer 1

Conceptually, the type of that function is

sizedList :: ∀ a . [a] -> (∃ n. KnownNat n => Vector n a)  -- not legal Haskell

i.e. it gives a vector of some length that is not a-priori known, or in other (admittedly strange) words: there will exist a number n such that the type of the returned vector is n.

Haskell doesn't have such existential types though, at least not anonymously, you would need to define it separately:

data DynVector a where
  DynVector :: Vector n a -> DynVector a

sizedList :: [a] -> DynVector a

The standard trick for using existential types on the fly is to apply continuation-passing expansion. You can always transform a function f :: A -> B into a function

fCPS :: ∀ r . A -> (B -> r) -> r
fCPS x φ = φ (f x)

and vice versa you could retrieve the original form

f' :: A -> B
f' x = fCPS x id

or

f' x = x `fCPS` \y -> y

For a monomorphic function like f this is just a silly way of making the signature more complicated, but for something like sizedList it has the effect of moving the ∃ quantor from a covariant position (the result of the function) into a contravariant position (the argument of the continuation φ). And this change turns the existential quantor into a universal quantor.

Ehm, huh... what?

See, sizedList returns a vector of some length. That is equivalent to saying whoever accepts this vector (namely, the continuation) must be able to deal with an input of any length. IOW, the continuation must be a polymorphic function over the length. And that's exactly what the signature

withSizedList :: ∀ a r . [a] -> (∀ n . KnownNat n => Vector n a -> r) -> r
withSizedList φ l = φ (sizedList l)
          -- N.B. this can NOT be written  φ $ sizedList l

expresses.

So how do you use it? Actually what you tried was close, but the problem is that the concrete type-value n cannot escape the continuation – it must always be r, which can be any type but needs to be chosen up-front. The result of deck `VSized.withSizedList` sort would however again need to be an existential type, and even if that was supported then it wouldn't help with the fact that deck `VSized.withSizedList` shuffle would give another existential value, with no way for the type system to know that they both have the same length.

The type you need to choose as r instead is the final result of the whole computation, i.e. simply Bool. That means you need to wrap everything that deals with the polymorphic length into one single continuation, rather than having multiple separate continuations:

prop $ \(deck :: [Card]) -> deck `VSized.withSizedList` \deckV ->
          shuffle deckV == sort deckV

or shorter

prop (`VSized.withSizedList` \deck -> shuffle deck == sort deck)

Answer 2

Let me try to explain things in plain English!

The short answer

The function withSizedList takes two arguments: a list, and a "processing function." It takes the list, converts it into a vector, passes that vector into the processing function, and then returns whatever the processing function returned.

The tricky part is that the processing function needs to have exactly the same return type regardless of the length of the vector that's passed into it. That's why you're encountering an error message when you try to use shuffle or sort as the processing function: those functions both take Vector n Card and return Vector n Card, so the return type differs depending on the length of the vector that's passed into them.

The solution, as pointed out in leftaroundabout's answer, is to write a function of type KnownNat n => Vector n Card -> Bool which does all the important stuff, and then use withSizedList to convert that into a function of type [Card] -> Bool.

Why it works that way

All right... but how were you supposed to know that the processing function needs to have the same return type regardless of the length of the vector?

Let's take a close look at the type signature of withSizedList:

withSizedList :: forall a r. [a] -> (forall n. KnownNat n => Vector n a -> r) -> r

This type signature essentially describes a protocol that you use for interacting with withSizedList. Here's how the protocol goes:

• First, you tell withSizedList what type you want to use as a.
• Then, you tell withSizedList what type you want to use as r.
• Next, you give it a list of type [a].
• After that, you give it a "processing function" of type... uh, we'll talk about that in a moment.
• Finally, withSizedList gives you a value of type r.

Okay, now let's take a close look at the type of the processing function, which is forall n. KnownNat n => Vector n a -> r. This type signature describes a protocol that withSizedList uses for interacting with your processing function. Here's how the protocol goes:

• First, withSizedList tells your function what number it wants to use as n.
• Next, withSizedList gives your function a vector of type Vector n a (where a is whatever you chose earlier).
• Finally, your function gives withSizedList a value of type r (where r is whatever you chose earlier).

Let's see how your original code interacts with this protocol. First, you tell withSizedList that you want a to be Card. So far, so good. Then, you tell withSizedList that you want r to be Vector n Card. But hang on, there's a problem: we don't know what n is yet. According to the above protocols, you have to choose r first, and then withSizedList will choose n after you've done that. You can't base your choice on a decision that hasn't been made yet.

(Now, we humans know that n is always going to be the length of the list. But the typechecker doesn't know that. As far as the typechecker knows, withSizedList could choose anything for n; it could even call your function several times, with a different value of n each time.)

Another way of thinking about this is that n can't escape from the parentheses. What I mean by that is that the notation (forall n. ...) creates a little environment where the variable n is meaningful, but the variable n is meaningless outside of that environment, so it's illegal for n to show up again outside of the parentheses.

On the other hand, if you write a function of type KnownNat n => Vector n Card -> Bool and use that as your processing function, everything will work just fine. First, you tell withSizedList that you want a to be Card. Then, you tell it that you want r to be Bool. Next, you give it your list, and after that, you give it your processing function. It'll do its thing, and finally, it will give you a value of type Bool.