在编译时添加相同大小的两个列表

Question

在伊德里斯，我可以通过添加相同大小的两个向量：

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

我可以：

module MatrixMath 

import Data.Vect 

addHelper : (Num n) => Vect k n -> Vect k n -> Vect k n 
addHelper = zipWith (+) 

编译它的REPL后然后用3号的两个向量称之为：

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

但是，当我尝试调用addHelper上的两个向量它将无法编译不同的尺寸：

*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 

我该如何在Scala中编写它？

Answer 1

Shapeless你可以帮助你在：

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) 

注意该方法如何csv约束双方Sized由N <: Nat，以同样的方式在你的例子，您可以通过Num n约束。

我从Shapeless examples复制了这段代码，如果它不是这样编译的，我可能错过了一些东西。

Answer 2

对于这种问题，shapeless通常是正确的选择。 无形状已具有类型级别编号（shapless.Nat），并且具有编译时已知大小（shapeless.Sized）的集合的抽象。

第一放的实现可能是这个样子

import shapeless.{ Sized, Nat } 
import shapeless.ops.nat.ToInt 
import shapeless.syntax.sized._ 

def Vect[A](n: Nat)(xs: A*)(implicit toInt : ToInt[n.N]) = 
    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)) 

及其用法：

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 

虽然这看起来像它的工作原理，它严重的缺点 - 你必须确保提供的长度和参数的数量相匹配，否则你会得到一个运行时错误。

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 

我们可以做得比这更好。您可以直接使用Sized而不是另一个构造函数。 此外，如果我们有两个参数列表定义add，我们可以得到一个更好的错误信息（这不是像你一样什么伊德里斯提供，但它是可用）：

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)) 

但是，我们可以走得更远。无形还提供元组和Sized之间的转换，所以我们可以这样写：

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)) 

而且这个作品中，尺寸从提供的元组推断：

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)) 

不幸的是，从例子中的语法只由于有一个称为参数自适应的功能，因此scalac会自动将多个参数从Vect转换成我们需要的元组。由于这个“功能”也可能导致非常讨厌的错误，我发现自己几乎总是用-Yno-adapted-args来禁用它。使用这个标志，我们必须明确地写出自己的元组：

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) 

而且，我们只能用长度可达22，Scala有较大的元组的支持。

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)) 

那么，我们可以得到稍微好一些的语法吗？原来，我们可以。无形能为我们做包装，使用HList代替：

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)) 

而且它的工作原理：

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) 

你可以从那里走的更远，在自己的类包装的Sized例如

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) 

实质上，所有归结为使用Sized和Nat作为类型约束。