hard to wrap around the concept of 0*n matrix

[Ashwin Bhaskar]

There is matrix transposition exercise in the book type driven development. It starts with the signature of the function

transposeMat : Vect m (Vect n elem) -> Vect n (Vect m elem)

And from here on the we use shortcuts and let the compiler generate code. At one point of time we arrive at the following expansion

transposeMat : Vect m (Vect n a) -> Vect n (Vect m a)
transposeMat [] = ?what
transposeMat (x :: xs) = let xsTrans = transposeMat xs in
                             transposeHelper x xsTrans

The type of what, according to the compiler, is:

Vect m (Vect 0 a)

which is the transpose of Vect 0 (Vect m a). But what exactly is this. How is this even possible? And why does []  not satisfy Vect 0 (Vect m a)  ?

Regards

Ashwin

[Ohad Kammar]

Hi,

The type of what according to the compiler should be

Vect n (Vect 0 a)

Here's one (and the only) such matrix in the case (n = 3): the (Vect 3 (Vect 0 a)) [[], [], []]

The value:

the (Vect 0 (Vect m a)) [] is fine, but it won't fit in the hole what, because you need

the (Vect n (Vect 0 a)) ?what

If you are using idris2, you'll also need to make sure the implicit argument m  is available at runtime, like so:

transposeMat : {m : Nat} -> Vect m (Vect n elem) -> Vect n (Vect m elem)

I hope I helped,

Ohad.

--
You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/0e40b4bf-ed41-4ed3-8db7-4d4f5cdb5f6fn%40googlegroups.com.

[Ohad Kammar]

Sorry, I renamed m and n wrongly. Here's the correction version:

On Sun, 16 May 2021 at 17:05, Ohad Kammar <ohad....@gmail.com> wrote:

Hi,

The type of what according to the compiler should be

Vect n (Vect 0 a)

Here's one (and the only) such matrix in the case (n = 3): the (Vect 3 (Vect 0 a)) [[], [], []]

The value:

the (Vect 0 (Vect n a)) [] is fine, but it won't fit in the hole what, because you need

the (Vect n (Vect 0 a)) ?what

If you are using idris2, you'll also need to make sure the implicit argument n  is available at runtime, like so:

transposeMat : {n : Nat} -> Vect m (Vect n elem) -> Vect n (Vect m elem)

I hope I helped,

Ohad.

[Ashwin Bhaskar]

Thanks you for the answer, Ohad:) I got your point that

Vect 0 (Vect m a) does not fit into a hole of type Vect m (Vect 0 a)

but my confusion is around what is Vect 0 (Vect m a) ? Is such a value possible?

the function definition

transposeMat [] = ?what

says that it has matched an empty list. But why does the empty list turn out to be of the type Vect 0 (Vect m a) ?

Regards

Ashwin

[Ohad Kammar]

but my confusion is around what is Vect 0 (Vect m a) ? Is such a value possible?

But why does the empty vector turn out to be of the type Vect 0 (Vect m a) ?

We have empty vectors [] of type Vect 0 t for every type t. One of those t can be Vect m a .

In that case, we have: [] : Vect 0 (Vect m a).

Does this help?

Ohad.