SnocList recursive view 형 드라이버를 개발해 보세요 in Idris2

안녕하세요.23일째 보도입니다.이번에는 며칠 전이에요.κ실제 제작 een씨가 쓴 Idris Advent Calendar 2020에 소개된 SnocList view를 통해 형구동 개발의 실례를 조금 상세하게 설명하고 싶습니다(보도에 오류가 있으면 알려주세요).

원래 뷰는...

뷰란 데이터 구조자의 분해 이외의 방법에 따라 데이터형을 분해하고 해석하는 것을 말한다. 즉, (View)를 보기 위한 데이터형이다.Irdris에서 View는 의존형 데이터형을 사용하는 것으로 정의되었고 그 유형 구조자는 목표 데이터의 의도를 분해하는 형식을 유지하고 있다.구체적인 예를 살펴보자.

SnocList view

List는 Idris의 Produde에 의해 정의됩니다.
익숙하신 것 같습니다.현재, 예를 들어, 만약에 어리석게reverse 함수를 정의하여 첫 번째 매개 변수의 목록을 패턴적으로 일치시키면, 보통 아래의 데이터 구축자에 따라 분해됩니다.

data List (a : Type) -> Type where
   Nil  : List a
   (::) : (x : a) -> (xs : List a) -> List a

현재 이naive의 실현을 개선하기 위해 위의 매개 변수의 lst를 끝에서 분해하고 싶습니다.그렇게 생각하는 순간일 거예요.
하지만 번역할 수 없습니다.매개 변수의 패턴 일치는 데이터 건설기를 따라 진행되기 때문이다.이걸 해결하는 게 뷰야.

reverse : (lst : List a) -> List a
reverse []        = []
reverse (x :: xs) = reverse xs ++ [x]

SnocList는 (xs:Lista)에 글자가 붙었다.2개의 데이터 구조자가 있는데,
Enpty는 빈 목록의 SnocList를 표시하고, Snoc는 x:a와 xs:Lista, 그리고 snoc:SnocList xs는 (xs++[x]) 형식으로 목록을 봅니다.지금도

-- これは通らない
reverse : (lst : List a) -> List a
reverse []          = []
reverse (xs ++ [x]) = x :: reverse xs

함수를 통해 임의의 xs:Lista를 SnocList xs로 변환할 수 있다면 SnocList의 데이터 구조자에 따라 패턴을 매칭하여 xs의 끝 요소를 끊임없이 추출할 수 있다.SnocList를 사용한 Reverse의 정의는 다음과 같습니다.

data SnocList : (xs : List a) -> Type where 
  Empty : SnocList []
  Snoc : (x : a) -> (xs : List a) -> (snoc : SnocList xs) -> SnocList (xs ++ [x])

여기서 Idris의 with 문법을 사용하면 helper 함수를 쓰지 않을 수 있습니다.

snocList : (xs : List a) -> SnocList xs

그리고 뷰를 간단하게 설명했기 때문에 지금부터 형 드라이브 개발을 통해 임의의 (xs:Lista)를 SnocList xs의 전역 함수인 snocList로 바꾸어 보려고 합니다.

형 구동 개발

TDD with Idris서에 따르면 형 구동 개발의 기본 단계는 다음과 같은 3가지다.

Type: 함수 유형을 최고 레벨에서 선언

Define: 형식 선언에 따라 컴파일러가 골격 코드를 생성하고 매개 변수를 패턴으로 일치시키거나 자명한hole를 실제 장치로 바꿉니다.Refine: 남은 홀의 유형을 조사하면서 맨 윗부분 선언을 변경하고 유형을 개작하여 홀을 채워 실복을 완성합니다.네.먼저 snocList형 선언을 하겠습니다.

reverse : (lst : List a) -> List a
reverse lst = helper (snocList lst)
  where
    helper : SnocList xs -> List a
    helper Empty = []
    helper (Snoc x xs snoc) = x :: helper snoc

편집기 플러그인을 직접 사용하여 컴파일러가 대략적인 코드를 생성하도록 한다.

reverse : (lst : List a) -> List a
reverse lst with (snocList lst)
reverse [] | Empty = []
reverse (xs ++ [x]) | (Snoc x xs snoc) = x :: reverse xs | snoc

편집기 플러그인을 사용하여 데이터 건설기를 따라 xs를 분할할 수 있습니다.

snocList : (xs : List a) -> SnocList xs

이때의 시도 63?snocList_rhs_두 가지 유형은 이렇게 형성된 것이다.

snocList : (xs : List a) -> SnocList xs
snocList xs = ?snocList_rhs

허선에서 현재 사용할 수 있는 변수와 그 유형, 다음에 만들어야 할 값이 가지고 있는 유형.스노크라이스트(x:xs)를 점선 위에 있는 것만 만드는 건 좀 어려울 것 같아.
SnocList 자체는 데이터 구조자를 호출하는 형식이기 때문에 accumultator의 helper 함수를 정의하는 것이 좋습니다.

snocList : (xs : List a) -> SnocList xs
snocList [] = Empty          
snocList (x :: xs) = let rec = snocList xs in ?snocList_rhs_2

여기서 helper가 xs=input++rest라는 것을 주의하면 이것은 리스트를 스캔하는 함수입니다. 이것은 accumulator와 함께 사용됩니다.input은 SnocList화가 완성된 부분List이며, rest는 향후 SnocList화가 남은 부분List를 표시한다.
다음에 컴파일러로 하여금 helper의 프레임워크를 생성하게 합니다.(rest:Lista)를 SnocList로 변환하고 싶으므로 데이터 구조자에 따라 rest를 분해하십시오.

 0 a : Type
   x : a
   xs : List a
   rec : SnocList xs
------------------------------
snocList_rhs_2 : SnocList (x :: xs)

?helper_rhs_1형은 이렇다.

snocList : (xs : List a) -> SnocList xs
snocList xs = helper Empty xs 
  where 
    helper : (acc : SnocList input) ->
             (rest : List a) -> SnocList (input ++ rest)

acc에서 SnocList(input++[])를 얻을 수 있을 것 같지만 Idris는 당연히
input++[]=input을 모릅니다.그래서 그렇다는 것을 증명해야 한다.
Data.List

snocList : (xs : List a) -> SnocList xs
snocList xs = helper Empty xs where
  helper : (acc : SnocList input) ->
           (rest : List a) -> SnocList (input ++ rest) 
  helper acc [] = ?helper_rhs_1   
  helper acc (x :: ys) = ?helper_rhs_2 

이 함수가 증명했으니 이번에도 공부를 위해 그걸 하자.우선, 다음과 같이 보충한다.

 0 a : Type
   xs : List a
   acc : SnocList input
------------------------------
helper_rhs_1 : SnocList (input ++ [])

Idris2에서는 정의에 사용된 implicit arguments가 명확하게 발표해야 하기 때문에 input을 발표하는 동시에 appeendNilRightNeutral의 유형 정의를 쓴다.이번에는 컴파일러가 appendNilRightNeutral의 골격을 생성하도록 합시다.그리고 유일한 매개 변수인 input을 분해합니다.

appendNilRightNeutral : (l : List a) -> l ++ [] = l

?appendNilRightNeutral_rhs_한 사이즈는 이렇습니다.
질의응답 없이 Refl입니다.다른 한편?appendNilRightNeutral_rhs_2예,

appendNilRightNeutral : (input : List a) -> input ++ [] = input

snocList : (xs : List a) -> SnocList xs
snocList xs = helper Empty xs where                                           
  helper : {input : List a} -> 
           (acc : SnocList input) -> 
	   (rest : List a) -> SnocList (input ++ rest)
  helper {input} acc [] = ?helper_rhs_1
  helper acc (x :: ys) = ?helper_rhs_2

.좀 복잡해 보이는데 xs 적용 귀납법에 관해서는 됩니다.
대부분의 증명은 구조에 관한 귀납법이다.
이번에는 어때?xs에 귀속적으로 적용하면 모델이 바뀐다.

appendNilRightNeutral : (input : List a) -> input ++ [] = input
appendNilRightNeutral [] = ?appendNilRightNeutral_rhs_1
appendNilRightNeutral (x :: xs) = ?appendNilRightNeutral_rhs_2

snocList : (xs : List a) -> SnocList xs
snocList xs = helper Empty xs where                                           
  helper : {input : List a} -> 
           (acc : SnocList input) -> 
	   (rest : List a) -> SnocList (input ++ rest)
  helper {input} acc [] = appendNilRightNeutral input 
  helper acc (x :: ys) = ?helper_rhs_2

현재,rec의 유형 rhs만약 2의 왼쪽을 다시 쓸 수 있다면 x:xs=x:xs, 기쁘고 축하할 만한 Refl.다시 쓰는 문법이 있고, rewrite Ain B를 쓰면 A의 형식으로 B를 다시 쓸 수 있다.

 0 a : Type
------------------------------
appendNilRightNeutral_rhs_1 : [] = []

그리고

 0 a : Type
   x : a
   xs : List a
------------------------------
appendNilRightNeutral_rhs_2 : x :: (xs ++ []) = x :: xs

저는 이웃입니다. 기쁘고 축하합니다.이제 증명 끝났어.

appendNilRightNeutral : (input : List a) -> input ++ [] = input
appendNilRightNeutral [] = Refl
appendNilRightNeutral (x :: xs)
  = let rec = appendNilRightNeutral xs in ?rhs_2

?helper_rhs_1 의 유형은

 0 a : Type
   x : a
   xs : List a
   rec : xs ++ [] = xs
------------------------------
rhs_2 : x :: (xs ++ []) = x :: xs

이니까 리트리트로 다시 쓰면 이 홀이 끝이야.

appendNilRightNeutral : (input : List a) -> input ++ [] = input
appendNilRightNeutral [] = Refl
appendNilRightNeutral (x :: xs)
   = let rec = appendNilRightNeutral xs in rewrite rec in ?rhs

나머지는 helperrhs_먼저 모델을 봅시다.

 0 a : Type
   x : a
   xs : List a
   rec : xs ++ [] = xs
------------------------------
rhs : x :: xs = x :: xs

쳐다보면 보이는데, SnocList(input++(y:ys) 이런 유형은
SnocList(input++[y])++ys)형과 같고 Helper(Snocy input acc)ys를 호출할 때의 결과형과 같습니다.
따라서 지금 input++(y:ys)를 (input++[y])++ys로 바꿀 수 있다면 이hole도 채울 수 있습니다.(y:ys)=[y]++ys를 이용하여
(input++(y:ys)=(input++([y]++ys)=(input+++[y])++ys)만 증명하면 됩니다.
이것은 단지 appeend의 결합율, Data를 나타낸다.리스트에서는 그게 맞아요.
appendAssociative : (l, c, r : List a) -> l++ (c++ r) = (l++ c)++ r
이런 함수가 있다.이것도 아까와 마찬가지로 다음과 같다.

appendNilRightNeutral : (input : List a) -> input ++ [] = input
appendNilRightNeutral [] = Refl
appendNilRightNeutral (x :: xs) = rewrite appendNilRightNeutral xs in Refl

snocList : (xs : List a) -> SnocList xs
snocList xs = helper Empty xs where
  helper : {input : List a} -> 
           (acc : SnocList input) ->
           (rest : List a) -> SnocList (input ++ rest)
  helper {input} acc [] = ?helper_rhs_1
  helper acc (x :: ys) = ?helper_rhs_2

이때,

 0 a : Type
   xs : List a
   input : List a
   acc : SnocList input
------------------------------
helper_rhs_1 : SnocList (input ++ [])

,

appendNilRightNeutral : (input : List a) -> input ++ [] = input
appendNilRightNeutral [] = Refl
appendNilRightNeutral (x :: xs) = rewrite appendNilRightNeutral xs in Refl

snocList : (xs : List a) -> SnocList xs
snocList xs = helper Empty xs where
  helper : {input : List a} -> 
           (acc : SnocList input) -> 
           (rest : List a) -> SnocList (input ++ rest) 
  helper {input} acc [] = rewrite appendNilRightNeutral input in acc
  helper acc (y :: ys) = ?helper_rhs_2  

, rewrite를 사용하여 덮어쓰기

 0 a : Type
   xs : List a
   y : a
   ys : List a
   acc : SnocList input
------------------------------
helper_rhs_2 : SnocList (input ++ (y :: ys))

.이번 시도?helper_rhs_2 의 유형은

appendAssociative : (l, c, r : List a) -> l ++ (c ++ r) = (l ++ c) ++ r
appendAssociative [] c r = Refl                               
appendAssociative (x :: xs) c r = rewrite appendAssociative xs c r in Refl

, helper(Snocy input acc)ys:SnocList((input++[y])++ys)인 경우 최종

snocList : (xs : List a) -> SnocList xs
snocList xs = helper Empty xs where 
  helper : {input : List a} -> 
           (acc : SnocList input) -> 
           (rest : List a) -> SnocList (input ++ rest)
  helper {input} acc [] = rewrite appendNilRightNeutral input in acc
  helper {input} acc (y :: ys) = 
    let thm = appendAssociative input [y] ys in ?helper_rhs_2

.지금까지 snocList의 정의였습니다.