SOP를 사용하여 Case Analysis 함수 일반 설치

case analysis 함수에 관해서는 우선kkun61씨의 아래 글을 참조하십시오.
https://kakkun61.hatenablog.com/entry/2021/01/06/Case_Analysis_함수.
case analysis 함수는 데이터 유형에 따라 결정되는 함수입니다. 자세히 보면 간단한 규칙으로 통일적으로 실현할 수 있을 것 같습니다.
Haskell에서 같은 이름의 함수를 사용하여 여러 데이터 형식을 처리하기 위해서는 모듈을 분류하거나 유형 유형을 활용하는 데 공을 들여야 한다.
이 글에서 저는 매우 규범화된 프로그램 설계를 바탕으로 각종 데이터 유형에 대응하는case analysis 함수를 실시하고 싶습니다.
지금부터 실시gfold'(generic fold)의 함수는 다음과 같다.

> :t unFun . gfold' @Bool
unFun . gfold' @Bool :: Bool -> r -> r -> r

> :t unFun . gfold' @(Maybe Bool)
unFun . gfold' @(Maybe Bool) :: Maybe Bool -> r -> (Bool -> r) -> r

> :t unFun . gfold' @(Either Bool Int)
unFun . gfold' @(Either Bool Int)
  :: Either Bool Int -> (Bool -> r) -> (Int -> r) -> r

SOP

SOP는 sums of products의 줄임말로 데이터형을 직접적으로 축적된 합으로 분해한다.SOP의 논문에서 설명한 설치를 프로그램 라이브러리로 하는 것은generics-sop이다.
'직화','직적'등의 단어에 익숙하지 않은 사람은 먼저 아래의 문장을 참고하세요.
https://ryota-ka.hatenablog.com/entry/2018/07/09/110000
일반적으로 대수의 데이터형의 상하문에서 직화 또는 직적Either을 말하면 원조(,)를 사용하여 나타낸다실제 사용되는 데이터형 중 여러 유형에 따른 직접적 적·직화를 많이 고려하기 때문에 SOP에서는 n-ary sumsNS와 n-ary productsNP를 나타내는 유형(SOP는sum's'of product's'의 생략을 떠올리세요)을 사용한다.어느 것이든 유형 등급 목록에 따라 직접 또는 직접 합병된 유형을 관리한다.
실제 SOP를 사용하여 얻은 데이터 유형의 표현을 살펴봅시다.

> from (Just 'a')
SOP (S (Z (I 'a' :* Nil)))

GHC.Generics와는 달리 메타 정보가 포함되지 않기 때문에 단순히 직화와 직적의 구조를 처리하려고 할 때는 SOP를 사용하는 것이 간단하다.

> :t from (Just 'a')
from (Just 'a') :: SOP I '[ '[], '[Char]]

몰드에서 네스트된 클래스 목록을 볼 수 있습니다.외측의 유형 등급 목록과 내측의 유형 등급 목록은 직접 대응한다.이것은 메이브형의 표현'[]이 대응Nothing, '[Char]가 대응Just Char이다.구체적인 실행 방안을 살펴봅시다.

-- | ジェネリックなSOPの表現との相互変換を扱う型クラス
class ... => Generic (a :: Type) where
    type Code a :: [[Type]]
    from :: a -> Rep a
    to :: Rep a -> a

-- | 型aのジェネリックな表現
type Rep a = SOP I (Code a)

-- | 直積の直和を表す型
newtype SOP (f :: k -> Type) (xss :: [[k]]) = SOP (NS (NP f) xss)

-- | 恒等関手
newtype I a = I a

Generics의 유형류 제한에 대해서는 신경 쓸 필요가 없기 때문에 생략했습니다.라이브러리는 대부분의 표준 유형의 실례Generics를 정의했고 자신이 정의한 유형의 실례Generics를 자동으로 내보낼 수 있다.
N 유형을 나타내는 직선 및 NS는 다음과 같이 정의됩니다.

data NS :: (k -> Type) -> [k] -> Type where
  Z :: f x -> NS f (x ': xs)
  S :: NS f xs -> NS f (x ': xs)

이것은 Peano자연수와 유사한 실현이다.이것은 유형 등급 목록이 총계를 표시하기 때문에 수치는 목록에 포함된 임의의 유형의 값만 있기 때문에 몇 번째 유형의 값이 있는지 표시하기 위해 자연수의 실시 방식을 채택하였다.예를 들어 다음Char과 Int 및 String의 직화를 나타낼 수 있다.

> Z (I 'a') :: NS I '[Char, Int, String]
Z (I 'a')
> S $ Z (I 1) :: NS I '[Char, Int, String]
S (Z (I 1))
> S . S $ Z (I "abc") :: NS I '[Char, Int, String]
S (S (Z (I "abc")))

N개 유형을 나타내는 직접적NP의 설치를 살펴보자.

data NP :: (k -> Type) -> [k] -> Type where
  Nil  :: NP f '[]
  (:*) :: f x -> NP f xs -> NP f (x ': xs)

테러리스트와 같은 실시 방식은 말할 것도 없다.예를 들어 다음Char과 Int과String의 직접적을 나타낼 수 있다.

> I 'a' :* I 1 :* I "abc" :* Nil :: NP I '[Char, Int, String]
I 'a' :* I 1 :* I "abc" :* Nil

일반case와alysis 함수 유형

그럼 SOP를 사용하여 일반적인 케이스 alysis 함수gfold를 실현합시다.
우선 유형a과 관련된caseanalysis 함수의 유형을 고려해 보겠습니다.

gfold :: (直和の各成分を処理する関数の直積) -> a -> r

이렇게 써야 하지만 괄호 안의 함수수는 a의 형식에 따라 달라지기 때문에 이렇게 표현하기 어렵다.따라서 가설a의 표현Rep a은SOP I xss이고 우리는caseanalyysis 함수의 유형을 다시 고려한다.

gfold :: SOP I xss -> Fun xss r

의 첫 번째 매개 변수는 a의 표시이다.되돌아오는 값의 유형Fun이 지금부터 정의됩니다. 표시(直和の各成分を処理する関数の直積) -> r를 고려하십시오.Fun는 처리형족의 유형으로 방침으로 a를 반영한 SOP의 구조xss를 사용하여 형족에 따라 구한直和の各成分を処理する関数の直積의 유형을 고려했다.
예를 들어 유형의 직접적'[a, b, c]부터 r의 함수까지 가리화를 고려하면a -> b -> c -> r.형족으로 이걸 이루면 다음과 같은 내용을 쓸 수 있다.

type family FunP (xs :: [Type]) r where
    FunP '[] r = r
    FunP (x ': xs) r = x -> FunP xs r

진일보한 유형의 정화'[a, b, c]부터 r까지의 함수는 (a -> r, b -> r, c -> r)로 쓸 수 있다.case analysis 함수는 최종적으로 이 대응하는 역(a -> r, b -> r, c -> r) -> '[a, b, c] -> r이 필요하다. '[a, b, c]은 SOP에서 얻었기 때문에 획득(a -> r, b -> r, c -> r) -> r을 실현한 유형족이다.

type family FunS (xss :: [[Type]]) r where
    FunS '[] r = r
    FunS (xs ': xss) r = FunP xs r -> FunS xss r

안쪽의 목록이 직적임을 감안하여 실시에서도 사용FunP.
마지막으로 FunS 단사형족이 아니기 때문에 형으로 처리하기가 번거롭다.따라서 간단히FunS 랩으로 포장newtype할 예정이다.

newtype Fun xss r = Fun {unFun :: FunS xss r}

이렇게 Fun의 유형이 완성되었습니다.이제 설치를 진행하겠습니다.

일반case와alysis 함수의 실현

gfold 유형 등급 목록을 유형 변수로 하기 위해서는 유형 분류 귀납 정의를 사용하는 것이 좋다.

class GFold (xss :: [[Type]]) where
    gfold :: SOP I xss -> Fun xss r

우선 빈 명단gfold의 상황을 고려한다.금형으로 사용할 수치가 없는 셈xss이다.Void의caseanalysis 함수는 어떠한 값Void도 되돌려주지 않기 때문에 실시 방식으로는 다음과 같다.

instance GFold '[] where
    gfold _ = Fun undefined

다음은 빈 명단이 아니라 값인 상황을 고려해 보겠습니다.

instance GFold xss => GFold (xs ': xss) where
    gfold (SOP (S xs)) = ...
    gfold (SOP (Z x))  = ...

귀납적인 정의를 고려하기 때문에 undefined의 상당 부분은 xss의 실례이다.tail의 실현은 직화GFold가 어떤 후속gfold인지NS인지에 따라 구분된다.후속S이라면 귀납적으로 Z에 다시 S하면 된다.

    gfold (SOP (S xs)) = constFun (gfold (SOP xs))

여기xs는 유형 등급 목록 형식과 일치하는 함수입니다.

constFun :: Fun xss r -> Fun (xs ': xss) r
constFun (Fun f) = Fun $ const f

한 마디로 하면 gfold에 대응하는 함수를 무시하고 유형에 부합하도록 한다.caseanalysis는 직접적이고 대응하는 함수만 실행하는 행위를 실현해야 한다.
다음은 직접과 함수의 실현 상황constFun을 살펴보자.

    gfold (SOP (Z x))  = embed (Fun $ \f -> apply f x)

xs와 Z는 정의되지 않았으며 뒤에 서술할 것입니다.직화형에 대응하는 값embed이 존재하면 apply에 따라 대응하는 함수를 꺼낸다.x의 유형은 Fun $ \f ->의 유형f의 유형은 a -> b -> c -> r의 유형이기 때문에 함수 응용에 공을 들여야 한다.그래서 다음과 같은 유형의 반을 준비했다.

class Apply (xs :: [Type]) where
    apply :: FunP xs r -> NP I xs -> r

instance Apply '[] where
    apply r _ = r

instance Apply xs => Apply (x ': xs) where
    apply f ((I x) :* xs) = apply (f x) xs

이것을 x로 사용하면 NP I (xs :: [Type])를 통해 평가할 수 있다apply f x.f의 유형은 최종적으로x이지만 유형이 수요에 부합되기 위해Fun $ \f -> apply f x.거기에 필요한 것은 Fun '[xs] r입니다.Fun (xs ': xss) r도 유형 유형에 따라 다음과 같이 설치했다.

class Embed (xss :: [[Type]]) where
    embed :: Fun (xs ': '[]) r -> Fun (xs ': xss) r

instance Embed '[] where
    embed = id

instance Embed xss => Embed (xs ': xss) where
    embed = flipFun . constFun . embed

flipFun :: Fun (xs ': ys ': xss) r -> Fun (ys ': xs ': xss) r
flipFun f = Fun $ \ys xs -> unFun f xs ys

즉,case analyysis 함수에 대응하는 함수를 평가한 후 배열된 함수를 모두 무시embed한 것이다.
이상의 내용에 따라 최종 실시embed는 다음과 같다.

class GFold (xss :: [[Type]]) where
    gfold :: SOP I xss -> Fun xss r

instance GFold '[] where
    gfold _ = Fun undefined

instance (Apply xs, Embed xss, GFold xss) => GFold (xs ': xss) where
    gfold (SOP (S xs)) = constFun (gfold (SOP xs))
    gfold (SOP (Z x))  = embed (Fun $ \f -> apply f x)

constFun :: Fun xss r -> Fun (xs ': xss) r
constFun (Fun f) = Fun $ const f


class Apply (xs :: [Type]) where
    apply :: FunP xs r -> NP I xs -> r

instance Apply '[] where
    apply r _ = r

instance Apply xs => Apply (x ': xs) where
    apply f ((I x) :* xs) = apply (f x) xs


class Embed (xss :: [[Type]]) where
    embed :: Fun (xs ': '[]) r -> Fun (xs ': xss) r

instance Embed '[] where
    embed = id

instance Embed xss => Embed (xs ': xss) where
    embed = flipFun . constFun . embed

flipFun :: Fun (xs ': ys ': xss) r -> Fun (ys ': xs ': xss) r
flipFun f = Fun $ \ys xs -> unFun f xs ys

는 설치된 constFun를 사용하여 일반적인case와alysis 함수를 실현한다.

gfold' :: (GFold (Code a), Generic a) => a -> Fun (Code a) r
gfold' = gfold . from

정말 보고 싶었지만gfold 내용이 나오기 전gfold 결정되지 않았기 때문에 이 실시에서 번역을 통과할 수 없습니다.
우리 처음에 열거한 예를 다시 한 번 봅시다.

> :t unFun . gfold' @Bool
unFun . gfold' @Bool :: Bool -> r -> r -> r

> :t unFun . gfold' @(Maybe Bool)
unFun . gfold' @(Maybe Bool) :: Maybe Bool -> r -> (Bool -> r) -> r

> :t unFun . gfold' @(Either Bool Int)
unFun . gfold' @(Either Bool Int)
  :: Either Bool Int -> (Bool -> r) -> (Int -> r) -> r

물론 실제 집행도 가능하다.

> (unFun . gfold') True 1 2
2

> (unFun . gfold') (Just 1) "empty" show
"1"

> (unFun . gfold') (Right "Haskell") (++ "??") (++ "!!")
"Haskell!!"

여기서 실시한gfold' = unFun . gfold . from 실례만 적용되면 이전에 실시한 유형에도 적용될 수 있다.
그런데 리스트에 대해서 어때요?

> :t unFun . gfold' @[Int]
unFun . gfold' @[Int] :: [Int] -> r -> (Int -> [Int] -> r) -> r

목록의case와alysis 함수를 떠올릴 때

> :t GHC.OldList.foldr
GHC.OldList.foldr :: (a -> b -> b) -> b -> [a] -> b

처리하는 함수 옆에 목록 형식이 표시되지 않았음을 알 수 있습니다.
이를 위해서는 리커션 셰임즈의 카타모피즘 아이디어를 접할 필요가 있다.

cata :: (Base t a -> a) -> t -> a

목록Fun의 a에 대응하는 유형은

data ListF a b = Nil | Cons a b

의 유형, gfold'의caseanalysis 함수를 고려하면

(a -> b -> b) -> b -> ListF a b -> b

의 유형.이거랑 Generic랑 합치면

(a -> b -> b) -> b -> [a] -> b

는 목록의casealysis 함수와 일치합니다.
이걸 사실로 만들기 위해서.

distFun :: (a -> Fun xss r) -> Fun xss (a -> r)
mapFun :: (a -> b) -> Fun xss a -> Fun xss b

라는 함수를 실현한 후에

gcata = mapFun cata (distFun gfold)

이렇게 설치하면 됩니다.
다만 시행하기가 어려울 것 같아 이번에는 지침만 건드리고 끝냈다.
읽어주셔서 감사합니다!
이 기사가 재미있었으면 좋겠어요♡ 받을 수 있다면 기쁠 거예요☺️
100엔이라도 지지를 받으면 다음 글을 쓰기 위해 격려해 드리겠습니다.🙌