zwei Listen gleicher Größe zur Compile-Zeit

Question

In Idris Hinzufügen kann ich zwei Vektoren gleicher Größe über hinzufügen:

module MatrixMath 

import Data.Vect 

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

Nachdem es auf dem REPL Kompilieren:

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

ich kann nennen es dann mit zwei Vektoren der Größe 3:

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

Aber, wird es nicht kompilieren, wenn ich versuche addHelper auf zwei Vektoren zu nennen verschiedene Größen:

*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 

Wie kann ich das in Scala schreiben?

Answer 1

Shapeless können Sie helfen Ihnen, dass:

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) 

Hinweis, wie die Methode csv Einschränkungen sowohl Sized von N <: Nat, die gleiche Art und Weise in ihr Beispiel, dass Sie durch Num n Zwang.

Ich habe diesen Code von Shapeless examples kopiert, wenn es nicht kompiliert, wie es ist, könnte ich sehr gut etwas verpasst haben.

Answer 2

Für diese Art von Problem ist shapeless sehr oft das Richtige zu wenden. Shapeless hat bereits Typennummern (shapless.Nat) und eine Abstraktion für eine Sammlung mit einer bekannten Kompiliergröße (shapeless.Sized).

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 

Während dies sieht aus wie es funktioniert, ist es einen ernsthaften Nachteil - Sie sicherstellen haben:

Ein erstes Klappen bei einer Implementierung so etwas wie diese

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

Und seine Nutzung aussehen könnte dass die angegebene Länge und die Anzahl der Argumente übereinstimmen, andernfalls erhalten Sie einen Laufzeitfehler.

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 

Wir können es besser machen. Sie können Sized direkt anstelle eines anderen Konstruktors verwenden. Auch wenn wir add mit zwei Parameterlisten definieren, können wir eine bessere Fehlermeldung erhalten (es ist nicht so schön wie das, was Idris bietet, aber es ist nutzbar):

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

Aber wir können weiter gehen. Shapeless bietet auch eine Umwandlung zwischen Tupeln und Sized, so konnten wir schreiben:

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

Und das funktioniert, ist die Größe aus dem bereitgestellten Tupel abgeleitet wird:

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

Leider ist die Syntax aus dem Beispiel nur funktioniert dank einer Funktion namens argument adaption, bei der scalac automatisch die Argumente von Vect in das benötigte Tupel konvertiert.Da dieses "Feature" auch zu sehr unangenehmen Fehlern führen kann, finde ich es fast immer deaktiviert mit -Yno-adapted-args. Mit dieser Flagge, müssen wir ausdrücklich das Tupel selbst schreiben:

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) 

Auch wir Länge nur bis zu 22 verwenden könnte, hat scala keine Unterstützung für größere Tupel.

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

Also, können wir die etwas schönere Syntax bekommen? Stellt sich heraus, wir können. Shapeless kann für uns die Verpackung tun, eine hList anstelle:

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

Und es funktioniert:

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) 

Sie von dort weiter gehen könnte, für die Sized in Ihrer eigenen Klasse Einwickeln Beispiel

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) 

Im Wesentlichen läuft alles auf Sized und Nat für die Typ-Einschränkungen.