¿Es Validated un Applicative?

17057 단어 showdevarrowkotlin
Preguntas y respuestas sobre las live coding de Arrow .

La siguiente pregunta fue realizada durante la . Os dejamos también el enlace directo a la discusión en Github y el enlace del .

프레군타



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

레스푸에스타



Durante la sesión no respondimos por varias razones: la primera es que intentamos guiar estas sesiones explicando el porqué y cómo 소개 Arrow en nuestro código Kotlin 그리고 백엔드. Hemos preferido centrarnos en las características que nos ofrecen tipos cómo Which, 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.

그는 이전의 반복적인 마이그레이션을 사용하는 경우와 유사하게 유사한 세션을 생성하며, 새로운 기록을 내보낼 수 있는 방법은 Kotlin 및 Arrow를 사용하여 FP를 사용합니다. 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 유엔 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 테스트 ValidatedAsApplicativeTestKotest para comprobar estas propiedades. De todos modos, Validated además de ser un Applicative, es también 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 commentaron 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 드 @BartoszMilewski. Libro que te recomiendo si te quieres introducir en Teoría de categorías.

    좋은 웹페이지 즐겨찾기