All geek questions in one place

Adding two lists of the same size at compile time

In Idris, I can add two vectors of the same size with:

module MatrixMath import Data.Vect addHelper : (Num n) => Vect kn -> Vect kn -> Vect kn addHelper = zipWith (+)

After compiling to REPL:

 *MatrixMath> :l MatrixMath.idr Type checking ./MatrixMath.idr

Then I can call it two vectors of size 3:

 *MatrixMath> addHelper [1,2,3] [4,5,6] [5, 7, 9] : Vect 3 Integer

But it does not compile when I try to call addHelper on two vectors of different sizes:

 *MatrixMath> addHelper [1,2,3] [1] (input):1:20:When checking argument xs to constructor Data.Vect.::: Type mismatch between Vect 0 a (Type of []) and Vect 2 n (Expected type) Specifically: Type mismatch between 0 and 2

How can I write this in Scala?

+5
source share
2 answers

Shapeless is very suitable for this kind of problem. Shapeless already has level numbers ( shapless.Nat ) and abstractions for a collection with a known compile-time size ( shapeless.Sized ).

The first take in an implementation might look something like this.

 import shapeless.{ Sized, Nat } import shapeless.ops.nat.ToInt import shapeless.syntax.sized._ def Vect[A](n: Nat)(xs: A*)(implicit toInt : ToInt[nN]) = xs.toVector.sized(n).get def add[A, N <: Nat](left: Sized[Vector[A], N], right: Sized[Vector[A], N])(implicit A: Numeric[A]) = Sized.wrap[Vector[A], N]((left, right).zipped.map(A.plus))

And its use:

 scala> add(Vect(3)(1, 2, 3), Vect(3)(4, 5, 6)) res0: shapeless.Sized[Vector[Int],shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]]] = Vector(5, 7, 9) scala> add(Vect(3)(1, 2, 3), Vect(1)(1)) <console>:30: error: type mismatch; // long and misleading error message about variance // but at least it failed to compile

Although this seems to work, this is a serious flaw - you have to make sure that the provided length and number of arguments match, otherwise you will get a runtime error.

 scala> Vect(1)(1, 2, 3) java.util.NoSuchElementException: None.get at scala.None$.get(Option.scala:347) at scala.None$.get(Option.scala:345) at .Vect(<console>:27) ... 33 elided

We can do better than that. You can use Sized directly instead of another constructor. In addition, if we define add with two lists of parameters, we can get a better error message (this is not as good as Idris suggests, but it can be used):

 import shapeless.{ Sized, Nat } def add[A, N <: Nat](left: Sized[IndexedSeq[A], N])(right: Sized[IndexedSeq[A], N])(implicit A: Numeric[A]) = Sized.wrap[IndexedSeq[A], N]((left, right).zipped.map(A.plus)) // ... add(Sized(1, 2, 3))(Sized(4, 5, 6)) res0: shapeless.Sized[IndexedSeq[Int],shapeless.nat._3] = Vector(5, 7, 9) scala> add(Sized(1, 2, 3))(Sized(1)) <console>:24: error: polymorphic expression cannot be instantiated to expected type; found : [CC[_]]shapeless.Sized[CC[Int],shapeless.nat._1] (which expands to) [CC[_]]shapeless.Sized[CC[Int],shapeless.Succ[shapeless._0]] required: shapeless.Sized[IndexedSeq[Int],shapeless.nat._3] (which expands to) shapeless.Sized[IndexedSeq[Int],shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]]] add(Sized(1, 2, 3))(Sized(1))

But we can go further. Shapeless also offers a conversion between tuples and Sized , so we could write:

 import shapeless.{ Sized, Nat } import shapeless.ops.tuple.ToSized def Vect[A, P <: Product](xs: P)(implicit toSized: ToSized[P, Vector]) = toSized(xs) def add[A, N <: Nat](left: Sized[Vector[A], N], right: Sized[Vector[A], N])(implicit A: Numeric[A]) = Sized.wrap[Vector[A], N]((left, right).zipped.map(A.plus))

And this works, the size is inferred from the provided tuple:

 scala> add(Vect(1, 2, 3), Vect(4, 5, 6)) res0: shapeless.Sized[Vector[Int],shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]]] = Vector(5, 7, 9) scala> add(Vect(1, 2, 3))(Vect(1)) <console>:27: error: type mismatch; found : shapeless.Sized[scala.collection.immutable.Vector[Int],shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]]]] required: shapeless.Sized[Vector[Int],shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]]] add(Vect(1, 2, 3))(Vect(4, 5, 6, 7))

Unfortunately, the syntax from the example only works thanks to a function called argument adaptation, where scalac automatically converts several arguments from Vect to the set we need. Since this “feature” can also lead to very unpleasant errors, I found that I almost always disabled it with -Yno-adapted-args . Using this flag, we must explicitly write the tuple itself:

 scala> Vect(1, 2, 3) <console>:26: warning: No automatic adaptation here: use explicit parentheses. signature: Vect[A, P <: Product](xs: P)(implicit toSized: shapeless.ops.tuple.ToSized[P,Vector]): toSized.Out given arguments: 1, 2, 3 after adaptation: Vect((1, 2, 3): (Int, Int, Int)) Vect(1, 2, 3) ^ <console>:26: error: too many arguments for method Vect: (xs: (Int, Int, Int))(implicit toSized: shapeless.ops.tuple.ToSized[(Int, Int, Int),Vector])toSized.Out Vect(1, 2, 3) ^ scala> Vect((1, 2, 3)) res1: shapeless.Sized[scala.collection.immutable.Vector[Int],shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]]] = Vector(1, 2, 3) scala> add(Vect((1, 2, 3)))(Vect((4, 5, 6))) res2: shapeless.Sized[Vector[Int],shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]]] = Vector(5, 7, 9)

In addition, we could only use lengths up to 22; scala does not support large tuples.

 scala> Vect((1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23)) <console>:26: error: object <none> is not a member of package scala Vect((1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23))

So, can we get a more pleasant syntax? It turns out we can. Shapeless can do a wrapper for us, use an HList instead:

 import shapeless.ops.hlist.ToSized import shapeless.{ ProductArgs, HList, Nat, Sized } object Vect extends ProductArgs { def applyProduct[L <: HList](l: L)(implicit toSized: ToSized[L, Vector]) = toSized(l) } def add[A, N <: Nat](left: Sized[Vector[A], N])(right: Sized[Vector[A], N])(implicit A: Numeric[A]) = Sized.wrap[Vector[A], N]((left, right).zipped.map(A.plus))

And it works:

 scala> add(Vect(1, 2, 3))(Vect(4, 5, 6)) res0: shapeless.Sized[Vector[Int],shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]]] = Vector(5, 7, 9) scala> add(Vect(1, 2, 3))(Vect(1)) <console>:27: error: type mismatch; found : shapeless.Sized[scala.collection.immutable.Vector[Int],shapeless.Succ[shapeless._0]] required: shapeless.Sized[Vector[Int],shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]]] add(Vect(1, 2, 3))(Vect(1)) ^ scala> Vect(1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23) res2: shapeless.Sized[scala.collection.immutable.Vector[Int],shapeless.Succ[shapeless.Succ[... long type elided... ]]] = Vector(1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23)

You can go further from there by wrapping Sized in your own class, for example

 import shapeless.ops.hlist.ToSized import shapeless.{ ProductArgs, HList, Nat, Sized } object Vect extends ProductArgs { def applyProduct[L <: HList](l: L)(implicit toSized: ToSized[L, Vector]): Vect[toSized.Lub, toSized.N] = new Vect(toSized(l)) } class Vect[A, N <: Nat] private (val self: Sized[Vector[A], N]) extends Proxy.Typed[Sized[Vector[A], N]] { def add(other: Vect[A, N])(implicit A: Numeric[A]): Vect[A, N] = new Vect(Sized.wrap[Vector[A], N]((self, other.self).zipped.map(A.plus))) } // ... scala> Vect(1, 2, 3) add Vect(4, 5, 6) res0: Vect[Int,shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]]] = Vector(5, 7, 9) scala> Vect(1, 2, 3) add Vect(1) <console>:26: error: type mismatch; found : Vect[Int,shapeless.Succ[shapeless._0]] required: Vect[Int,shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]]] Vect(1, 2, 3) add Vect(1)

Essentially, it all comes down to using Sized and Nat for type constraints.

+5
source

Shapeless you can help you with this:

 import shapeless._ import syntax.sized._ def row(cols : Seq[String]) = cols.mkString("\"", "\", \"", "\"") def csv[N <: Nat](hdrs : Sized[Seq[String], N], rows : List[Sized[Seq[String], N]]) = row(hdrs) :: rows.map(row(_)) val hdrs = Sized("Title", "Author") // Sized[IndexedSeq[String], _2] val rows = List( // List[Sized[IndexedSeq[String], _2]] Sized("Types and Programming Languages", "Benjamin Pierce"), Sized("The Implementation of Functional Programming Languages", "Simon Peyton-Jones") ) // hdrs and rows statically known to have the same number of columns val formatted = csv(hdrs, rows)

Notice how the csv method restricts both Sized to N <: Nat , and in your example, that you restrict Num n .

I copied this code from Shapeless examples , if it does not compile the way it is, I could well have missed something.

+4
source

Source: https://habr.com/ru/post/1240970/

More articles:


All Articles