No Nested ":" allowed?

[Gadersd]

I am new to Idris2 and am attempting to model PyTorch's broadcastable tensor dimensions with the type system. If two tensor dimensions are broadcastable and have the same length then appending the same value to both dimensions should yield two new compatible tensor dimensions. The partially written type is

import Data.Vect

data Broadcastable : (Vect n1 Nat) -> (Vect n2 Nat) -> Type where
    Empty : Broadcastable [] []
    AppendSame : (val: Nat) -> Broadcastable (v1: (Vect n Nat)) (v2: (Vect n Nat)) -> Broadcastable (val::v1) (val::v2)

However, I run into the following error:

Error: Expected end of input.

main:9:5--9:15
 5 | data DType = F32
 6 | 
 7 | data Broadcastable : (Vect n1 Nat) -> (Vect n2 Nat) -> Type where
 8 |     Empty : Broadcastable [] []
 9 |     AppendSame : (val: Nat) -> Broadcastable (v1: (Vect n Nat)) (v2: (Vect n Nat)) -> Broadcastable (val::v1) (val::v2)
         ^^^^^^^^^^

Error: Undefined name unsafePerformIO. 

(Interactive):1:1--1:1
 1 | module Main

What does this error mean and is there a resolution?

[dunhamsteve]

There is a syntax error in line 9. Due to some issues in the parser, it's getting eaten and the failure is propagating up and giving the wrong parse error.

Here, Idris is expecting a term:

    AppendSame : (val : Nat) -> Broadcastable (v1 : Vect n Nat) (v2 : Vect n Nat) -> Broadcastable (val :: v1) (val :: v2)
                                              ^^^^^^^^^^^^^^^^^

You can put v1 there. Idris automatically adds {0 v1 : _} -> at the beginning. If you want to specify that v1 and v2 are the same length, you'll have to manually write out the implicits:

import Data.Vect

data Broadcastable : (Vect n1 Nat) -> (Vect n2 Nat) -> Type where
    Empty : Broadcastable [] []
    AppendSame : {0 v1 : Vect n Nat} -> {0 v2 : Vect n Nat} -> (val : Nat) -> Broadcastable v1 v2 -> Broadcastable (val :: v1) (val :: v2)

Hopefully that unblocks you, but IMO we need a better parse error here.

[dunhamsteve]

I prefer the solution I gave above, by you could also do this:

data Broadcastable : (Vect n1 Nat) -> (Vect n2 Nat) -> Type where
    Empty : Broadcastable [] []
    AppendSame : (val : Nat) -> Broadcastable (the (Vect n Nat) v1) (the (Vect n Nat) v2) -> Broadcastable (val :: v1) (val :: v2)

The the function is identity with the type made explicit. It is used in Idris where an inline type annotation might be used in another language. If you do this, and type :ti AppendSame in the repl, you'll see that Idris adds the two implicits that I wrote above, but in the opposite order.

[Gadersd]

Thanks! Broadcastable is now working properly. However, I have one other similar issue. For my other type:

data MatrixMultiplicable : (Vect n1 Nat) -> (Vect n2 Nat) -> Type where
    Dim2 : ([r1, c1]: Vect 2 Nat) -> ([c1, c2]: Vect 2 Nat) -> MatrixMultiplicable [r1, c1] [c1, c2]

I get the error

Error: Expected a type declaration.

main:16:10--16:11
 12 |     AppendOneLeft : (right: Nat) -> (b: Broadcastable v1 v2) -> Broadcastable (1::v1) (right::v2)
 13 |     AppendOneRight : (left: Nat) -> (b: Broadcastable v1 v2) -> Broadcastable (left::v1) (1::v2)
 14 | 
 15 | data MatrixMultiplicable : (Vect n1 Nat) -> (Vect n2 Nat) -> Type where
 16 |     Dim2 : ([r1, c1]: Vect 2 Nat) -> ([c1, c2]: Vect 2 Nat) -> MatrixMultiplicable [r1, c1] [c1, c2]
               ^

Error: Undefined name unsafePerformIO. 

(Interactive):1:1--1:1
 1 | module Main

How might this be resolved?

[andrevidela]

This is because pattern matching on the left side of : is not supported.

This should work although it does not do what you're looking for wrt to line-column checking:

data MatrixMultiplicable : (Vect n1 Nat) -> (Vect n2 Nat) -> Type where
    Dim2 : (v1: Vect 2 Nat) -> (v2: Vect 2 Nat) -> MatrixMultiplicable v1 v2

The most naive way of checking that the size of two matrices match is to write multiplication directly with the following type:

Matrix : Nat -> Nat -> Type -> Type
Matrix a b ty = Vect a (Vect b ty)

multiply : Matrx a b ty -> Matrix b c ty -> Matrix a c ty
multiply = ?etc

[Gadersd]

I resolved the issue by parameterizing the matrix dimensions as follows

data MatrixMultiplicable : (Vect n1 Nat) -> (Vect n2 Nat) -> Type where
    Dim2 : (r1: Nat) -> (c1: Nat) -> (c2: Nat) -> MatrixMultiplicable [r1, c1] [c1, c2]