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.

"…except for the test suit" – french decks have four suits that I know, a "test" card is none of them! SCNR — 7 hours ago

score 11 · Accepted Answer · 2023-07-04 20:04:35Z

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)

Note that OP actually wanted to test sort (shuffle deck) == sort deck. Does not diminish the superb explanation though! — 7 hours ago
ok… after a few readings I think I get it. So this high rank foralls make the result "undependable" from the bounded variable isn't it?? Just to give a easier example. If we have f :: [a] -> (forall b. [b] -> r) -> r, the continuation can only be things like length or const 42 which do not depend on the type of the value inseide the list. I've check with ghci and seems true — 6 hours ago

How to use function withSizedList?