PBT로 FP 법칙 확인해보기 - Applicative

dvmflstm·2021년 2월 20일
0

Project - FP_PBT

목록 보기
5/5

Applicative

Monad를 구성하는 기본수단이 unit과 flatMap이었다면, Applicative는 unit과 map2를 기본수단으로 하는 특질이다.

interface Applicative<F> {
    fun <A> unit(a: () -> A): Kind<F, A>
    fun <A, B, C> map2(fa: Kind<F, A>, fb: Kind<F, B>, f: (A, B) -> C): Kind<F, C>

applicative 특질은 그 이름이 시사하는 것처럼 unit + map2 말고도 unit + apply 를 기본수단으로 가지도록 할 수도 있다.

interface Applicative<F> {
    fun <A> unit(a: () -> A): Kind<F, A>
    fun <A, B> apply(fab: Kind<F, (A) -> B>, fa: Kind<F, A>): Kind<F, B>

이 사실은 곧 map2는 unit과 apply를 이용해서 구현할 수 있고, apply 또한 unit과 map2를 이용해서 구현할 수 있다는 것을 뜻한다.

interface Applicative<F> {
    fun <A> unit(a: () -> A): Kind<F, A>
    fun <A, B, C> map2(fa: Kind<F, A>, fb: Kind<F, B>, f: (A, B) -> C): Kind<F, C>
    
    fun <A, B> apply(fab: Kind<F, (A) -> B>, fa: Kind<F, A>): Kind<F, B> = map2(fab, fa) { ab, a -> ab(a) }

    fun <A, B, C> map2UsingApply(fa: Kind<F, A>, fb: Kind<F, B>, f: (A, B) -> C): Kind<F, C> = apply(apply(unit { f.curry() }, fa), fb)
}

PBT로 Applicative 법칙 확인해보기

왼쪽, 오른쪽 항등법칙

map2(unit(()), fa)((_, a) => a) == fa
map2(fa, unit(()))((a, _) => a) == fa

kotlin syntax로 표현한 왼쪽, 오른쪽 항등법칙은 각각 아래와 같다.

fun <F, A> leftIdLaw(ap: Applicative<F>, fa: Kind<F, A>): Boolean =
    ap.run {
        map2(unit { }, fa) { _, a -> a } == fa
    }

fun <F, A> rightIdLaw(ap: Applicative<F>, fa: Kind<F, A>): Boolean =
    ap.run {
        map2(fa, unit { }) { a, _ -> a } == fa
    }

그리고 이를 검사하는 pbt 기반 테스트 코드는 다음과 같다.

"left identity law" {
    forAll(nelArb) { seq ->
        leftIdLaw(ListApplicative, ListK(seq))
    }
}

"right identity law" {
    forAll(nelArb) { seq ->
        rightIdLaw(ListApplicative, ListK(seq))
    }
}

nelArb는 비어있지 않은 List를 randomly generate 해주는 custom generator이다. 필자가 구현한 ListApplicative의 map2 구현이 빈 리스트에 대해서는 잘못 동작하기 때문에 ... generator를 따로 구현했다.

val nelArb = Arb.list(Arb.int(), 1..Int.MAX_VALUE)

결합법칙

applicative 특질의 결합법칙을 명료하게 표현하기 위해서는 아래와 같은 product 함수를 이용할 수 있다. 이 함수가 하는 일은 두 효과를 map2를 이용해서 하나의 쌍으로 묶어주는 것 뿐이다.

fun <A, B> product(fa: Kind<F, A>, fb: Kind<F, B>): Kind<F, Pair<A, B>> = map2(fa, fb) { a, b -> a to b }

이 Product를 이용한 applicative 특질의 결합법칙의 표현은 다음과 같은 형태가 될 것이다.

product(product(fa, fb), fc) == product(fa, product(fb, fc))

그런데 좌항과 우항은 의미론적으로는 동등하지만, 실제 리턴타입이 각각 F[((A,B),C)]F[(A,(B,C))]로 같지 않다. 그래서 (A,(B,C))((A,B),C)로 순서만 바꿔주는 함수가 하나 더 필요하다.

fun <A, B, C> assoc(p: Pair<A, Pair<B, C>>): Pair<Pair<A, B>, C> = (p.first to p.second.first) to p.second.second

그리고 위에서 적은 결합법칙의 우항에 이 assoc 함수를 사상하면 완성된 결합법칙의 표현이 나온다.

product(product(fa, fb), fc) == map(product(fa, product(fb, fc)))(assoc)

이 결합법칙을 kotlin syntax로 표현하면 다음과 같다.

fun <F, A, B, C> assocLaw(ap: Applicative<F>, fa: Kind<F, A>, fb: Kind<F, B>, fc: Kind<F, C>): Boolean =
    ap.run {
        product(product(fa, fb), fc) == product(fa, product(fb, fc)).map { assoc(it) }
    }
    
"associative law" {
    forAll(nelArb, nelArb, nelArb) { a, b, c ->
        assocLaw(ListApplicative, ListK(a), ListK(b), ListK(c))
    }
}

자연성 법칙

Applicative 효과들을 다룰 때에는 map2로 값을 결합하기 전에 변환을 적용할 수도 있고 결합한 후에 적용할 수도 있는 경우가 많다. 자연성 법칙은 둘 중 어떤 쪽을 선택하든 결과가 같음을 말해준다.

map2(fa,fb)(a, b => (f(a), g(b))) == product(map(fa)(f), map(fb)(g))

여기서 좌항의 map2에 들어가는 lambda function을 추출해 productF라는 이름을 지어줄 수도 있다. (product의 함수 버전)

fun <I, O, I2, O2> productF(f: (I) -> O, g: (I2) -> O2): (I, I2) -> Pair<O, O2> = { i, i2 -> f(i) to g(i2) }

이 productF를 사용하여 최종적으로 다음과 같이 자연성 법칙을 표현해볼 수 있다.

map2(fa,fb)(productF(f,g)) == product(map(fa)(f), map(fb)(g))

이 자연성 법칙을 kotlin syntax로 표현하고, 이전과 같이 pbt 기반의 테스트 코드를 작성했다.

fun <F, A, B, C, D> naturalityLaw(ap: Applicative<F>, fa: Kind<F, A>, fb: Kind<F, B>, f: (A) -> C, g: (B) -> D): Boolean =
    ap.run {
        map2(fa, fb) { a, b -> productF(f, g)(a, b) } == product(fa.map(f), fb.map(g))
    }
    

"naturality law" {
        forAll(nelArb, nelArb) { a, b ->
            val f: (Int) -> String = { it.toString() }
            val g: (Int) -> Int = { it * it }
            naturalityLaw(ListApplicative, ListK(a), ListK(b), f, g)
        }
    }

profile
서울대학교 컴퓨터공학부 github.com/BaekGeunYoung

0개의 댓글