scala specifications category-theory scalacheck

ScalaCheck de alto orden



specifications category-theory (1)

No saber exactamente con épsilon de Hilbert, tomaría un enfoque más fundamental y usaría el Gen y el Arbitral de ScalaCheck para seleccionar las funciones a usar.

Primero, defina una clase base para las funciones que va a generar. En general, es posible generar funciones que tienen resultados no definidos (como dividir por cero), por lo que usaremos PartialFunction como nuestra clase base.

trait Fn[A, B] extends PartialFunction[A, B] { def isDefinedAt(a: A) = true }

Ahora puedes proporcionar algunas implementaciones. Sobrescriba toString para que los mensajes de error de ScalaCheck sean inteligibles.

object Identity extends Fn[Int, Int] { def apply(a: Int) = a override def toString = "a" } object Square extends Fn[Int, Int] { def apply(a: Int) = a * a override def toString = "a * a" } // etc.

He elegido generar funciones únicas a partir de funciones binarias usando clases de casos, pasando argumentos adicionales al constructor. No es la única forma de hacerlo, pero me parece la más directa.

case class Summation(b: Int) extends Fn[Int, Int] { def apply(a: Int) = a + b override def toString = "a + %d".format(b) } case class Quotient(b: Int) extends Fn[Int, Int] { def apply(a: Int) = a / b override def isDefinedAt(a: Int) = b != 0 override def toString = "a / %d".format(b) } // etc.

Ahora necesita crear un generador de Fn[Int, Int] y definirlo como Arbitrary[Fn[Int, Int]] implícito Arbitrary[Fn[Int, Int]] . Puede seguir agregando generadores hasta que esté azul en la cara (polinomios, componer funciones complicadas de las simples, etc.).

val funcs = for { b <- arbitrary[Int] factory <- Gen.oneOf[Int => Fn[Int, Int]]( Summation(_), Difference(_), Product(_), Sum(_), Quotient(_), InvDifference(_), InvQuotient(_), (_: Int) => Square, (_: Int) => Identity) } yield factory(b) implicit def arbFunc: Arbitrary[Fn[Int, Int]] = Arbitrary(funcs)

Ahora puedes definir tus propiedades. Utilice intG.isDefinedAt(a) para evitar resultados no definidos.

property("left identity simple funcs") = forAll { (a: Int, intG: Fn[Int, Int]) => intG.isDefinedAt(a) ==> (fCat.compose(fCat.id[Int])(intG)(a) == intG(a)) } property("right identity simple funcs") = forAll { (a: Int, intG: Fn[Int, Int]) => intG.isDefinedAt(a) ==> (fCat.compose(intG)(fCat.id)(a) == intG(a)) }

Si bien lo que he mostrado solo generaliza la función probada, es de esperar que esto le dé una idea de cómo usar el sistema de tipo avanzado para generalizar sobre el tipo.

Considere la siguiente definición de una categoría:

trait Category[~>[_, _]] { def id[A]: A ~> A def compose[A, B, C](f: A ~> B)(g: B ~> C): A ~> C }

Aquí hay una instancia para funciones unarias:

object Category { implicit def fCat = new Category[Function1] { def id[A] = identity def compose[A, B, C](f: A => B)(g: B => C) = g.compose(f) } }

Ahora, las categorías están sujetas a algunas leyes. Relacionar composición ( . ) E identidad ( id ):

forall f: categoryArrow -> id . f == f . id == f

Quiero probar esto con ScalaCheck. Probemos funciones sobre enteros:

"Categories" should { import Category._ val intG = { (_ : Int) - 5 } "left identity" ! check { forAll { (a: Int) => fCat.compose(fCat.id[Int])(intG)(a) == intG(a) } } "right identity" ! check { forAll { (a: Int) => fCat.compose(intG)(fCat.id)(a) == intG(a) } } }

Pero estos se cuantifican sobre (i) un tipo específico ( Int ), y (ii) una función específica ( intG ). Entonces, aquí está mi pregunta: ¿hasta dónde puedo llegar para generalizar las pruebas anteriores y cómo? O, en otras palabras, ¿sería posible crear un generador de funciones A => B arbitrarias y proporcionarlas a ScalaCheck?