在編譯時添加相同大小的兩個列表

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作爲類型約束。