¿Es Validated un Applicative?

Preguntas y respuestas sobre las sesiones live coding de Arrow.

La siguiente pregunta fue realizada durante la tercera sesión. Os dejamos también el enlace directo a la discusión en Github y el enlace del vídeo en el momento de la pregunta.

Pregunta

Hoy nos toca una pregunta cerrada: ¿es Validated un Applicative?. Intentaremos desarrollar un poco la respuesta.

Respuesta

Durante la sesión no respondimos por varias razones: la primera es que intentamos guiar estas sesiones explicando el porqué y cómo introducir Arrow en nuestro código Kotlin en el back-end. Hemos preferido centrarnos en las características que nos ofrecen tipos cómo Either, Validated o NonEmptyList en nuestro trabajo diario con código OOP y cómo incorporarlos a nuestro código base, que en la teoría matemática formal que los sustenta, la Teoría de categorías. La segunda es que durante las primeras dos sesiones, no queríamos hablar de FP. Nos lo reservamos para las siguientes sesiones.

De hecho, estas sesiones pretender simular un caso de uso sintético de migración iterativa, más o menos exportable a nuestro día a día, desde OOP a FP usando Kotlin y Arrow. Lo hacemos, no porqué creamos que un paradigma de programación sea mejor que el otro en términos absolutos, sino porqué pensamos que en el contexto del desarrollo de aplicaciones en Internet escalables de ciertas dimensiones y cambio constante, la FP puede ayudar mucho a entender el código y a aumentar su rendimiento de forma, creemos, más sencilla que la OOP.

Volviendo a la pregunta, ¿es Validated un Applicative?

La única forma de demostrarlo es haciendo una verificación formal, comprobando que Validated cumple con las leyes matemáticas cómo Functor así cómo también cumple con las leyes matemáticas de Applicative Functor.

Hemos creado un pequeño test ValidatedAsApplicativeTest con Kotest para comprobar estas propiedades. De todos modos, Validated además de ser un Functor y un Applicative, es también un Type Constructor, concretamente construye Coproducts o Sum types del tipo Valid o Invalid para pares de tipos concretos. Los test que hemos hecho utilizan Validated<Nothing, String?> y ValidatedNel<String?, String?>. Ésta es una desventaja que tiene la programación en Kotlin con las matemáticas. Debo crear instancias concretas de tipos para poder utilizarlos en test y por tanto, estoy comprobando únicamente esas leyes para esos tipos concretos, y no para todos los tipos que Validated puede construir.

• Conservación de los morfismos de identidad.

"Validated functor must preserve identity arrows" {
  checkAll(genNullableString) { a ->
    identity(a.valid()) shouldBe identity(a).valid()
    identity(a.invalid()) shouldBe identity(a).invalid()
  }
}

• Conservación de la composición de morfismos.

"Validated functor must preserve function composition" {
  checkAll(genNullableString) { a ->
    val f = { b: String? -> "PRE-APPENDED${b}" }
    val g = { b: String? -> "${b}POST-APPENDED" }
    g.compose(f)(a).valid() shouldBe a.valid().map(g.compose(f))
    g.compose(f)(a).invalid() shouldBe a.invalid().mapLeft(g.compose(f))
  }
}

• Identidad.

"Validated applicative must satisfy identity law" {
  checkAll(genValidated) { validated ->
    val validatedId = Validated.lift<NonEmptyList<String>, String?, String?>{ a -> identity(a) }
    validatedId(validated) shouldBe validated
  }
}

• Homomorfismo.

"Validated applicative must satisfy homomorphism law" {
  checkAll(genNullableString) { a ->
    val f = { b: String? -> "PRE-APPENDED${b}" }
    val validatedF = Validated.lift<Nothing, String?, String?>(f)
    validatedF(a.valid()) shouldBe f(a).valid()
  }
}

• Intercambio.

 "Validated applicative must satisfy interchange law" {
  checkAll(genNullableString) { a ->
    val f = { b: String? -> "PRE-APPENDED${b}" }
    val validatedF1 = Validated.lift<Nothing, String?, String?>(f)
    val validatedF2 = Validated.lift<Nothing, (String?) -> String?, String?> { f -> f(a) }
    validatedF1(a.valid()) shouldBe validatedF2(f.valid())
  }
}

• Composición.

"Validated applicative must satisfy composition law" {
  checkAll(genNullableString) { a ->
    val f = { b: String? -> "PRE-APPENDED${b}" }
    val g = { b: String? -> "${b}POST-APPENDED" }
    val validatedF1 = Validated.lift<Nothing, String?, String?>(f)
    val validatedF2 = Validated.lift<Nothing, String?, String?>(g)
    (validatedF2.compose(validatedF1))(a.valid()) shouldBe validatedF1(validatedF2(a.valid()))
  }
}

Hemos utilizado la función lift de Validated para comprobar estas leyes, inspirados en la definición formal de estas leyes en Haskell. Sin embargo, preguntando a la comunidad de Arrow nos comentaron que aunque son correctas, sería mas idiomático verificarlas usando la función zip de Validated. Es un ejercicio que queda pendiente.Y si queréis contribuir con ello haciendo una PR a nuestro repo será más que bienvenida.

Encontrarás las verificaciones formales matemáticas de Functor y Applicative en The Dao of Functional Programming de @BartoszMilewski. Libro que te recomiendo si te quieres introducir en Teoría de categorías.