scalar multiplication of `DataArrayN` in sciLean

Stream: general

[Asei Inoue]

I'm learning sciLean. I would like to implement a scalar multiplication of SciLean.DataArrayN but I get an error.

import SciLean.Data.DataArray

open SciLean

def A := ⊞[1.0, 2.0; 3.0, 4.0]

variable {α : Type} [pd : PlainDataType α] {ι : Type} [IndexType.{0,0} ι]

scoped instance [Mul α] : HMul α (DataArrayN α ι) (DataArrayN α ι) where
  hMul x xs := ⊞ i => x * xs[i]

/-
failed to synthesize
  OfScientific (DataArrayN Float (Fin 2 × Fin 2))
use `set_option diagnostics true` to get diagnostic information
-/
#check 10.0 * A

[Asei Inoue]

In contrast, the following code raises no error:

def A := [1, 2, 3, 4, 5]

-- we cannot perform scalar multiplication...
#check_failure 2 * A

variable {α : Type} [Mul α]

instance : HMul α (List α) (List α) where
  hMul (x : α) (xs : List α) := xs.map (x * ·)

-- works!!
#eval 2 * A

[Asei Inoue]

The motivation is to see how the same thing can be achieved with SciLean as with NumPy.

[Asei Inoue]

strangely, this works!

/-
{ hMul := fun x xs => xs.mapMono fun x_1 => x * x_1 }
-/
#whnf (inferInstance : HMul Float (DataArrayN Float (Fin 2)) (DataArrayN Float (Fin 2)))

[Asei Inoue]

but this does not work!

def C := ⊞[1.0, 2.0]
#eval 10.0 * C

[Tomas Skrivan]

Elaboration of arithmetic operations and numerical constants is a deep mystery to me.

Note that if you specify that 10.0 is really just a Float then it works

#check (10.0 : Float) * A -- works no problem

If you do not force 10.0 to be Float then Lean tries to look for homogeneous multiplication and tries to figure out if 10.0 can be understood as DataArrayN Float (Fin 2 × Fin 2).

Btw. SciLean uses • for scalar multiplication and this work out of the box

#check 10.0 • A

[Asei Inoue]

@Tomas Skrivan Thank you!!!