Tweag, Haskell에서 접착 연산을 명시적으로 만들어 층을 표현하다

Arnaud Spiwack은 Haskell에서 층을 표현하고 싶었지만, 교과서적 정의는 실질적인 문제를 안고 있었다. 체는 동일한 매칭 정보를 여러 중복된 방식으로 표현하며, 그 의존적 당김 구성은 Haskell에 너무 과한 의존적 타입이었다. 정의를 문자 그대로 옮기는 뻔한 접근은 불법 상태를 표현 가능하게 만들고 프로그램을 무관한 데이터로 파묻을 터였다.

그는 먼저 산술 표현식을 중심으로 구체적인 예를 만들었다. 준층은 표현식을 따라 값을 당길 수 있었지만, 원하는 조건부 연산은 불리언 덮개 위에서 두 갈래를 접착하는 층을 필요로 했다. 따라서 구현은 접착을 명시적인 타입 클래스 연산으로 만들고, 이를 타입이 지정된 Cover와 Gen 패밀리가 어떤 조각들을 조립할 수 있는지 기술하는 Site로 일반화했다.

타입이 지정된 site는 당김-체 부담을 제거한다. glue는 임의의 화살표에서 작동할 수 있고, 생성자는 실제 화살표로 표현될 필요가 없다. 곱, 지수, 요네다 매장, 쌍대곱, 재귀 리스트는 같은 방식으로 정의될 수 있다. Sheafify는 접착 연산을 조기에 평가하지 않고 저장함으로써 자유 층 구성을 수행하며, PFun은 지수에 필요한 분산을 담는다.

그 결과는 시연 저장소이자 추상적 아이디어의 Haskell다운 구현이며, 모든 수학적 세부가 사라진다는 주장은 아니다. Spiwack은 고정점을 명시적으로 미해결로 남겨두지만, 이 프로젝트는 언어에 비해 너무 느슨했던 정의를 타입이 지정된 작동적 구성 요소로 바꾸고 남은 미지의 부분을 정확하게 만든다.

덮개를 타입으로 표현하고, 접착을 명시적으로 수행한다

문자 그대로의 체는 중복된 매칭 패밀리 값을 인코딩하고 불가능해야 할 상태를 허용한다.

지수에 필요한 당김 체는 Haskell 구현이 편안하게 표현할 수 있는 범위를 넘는 의존적 타입을 요구한다.

타입이 지정된 덮개와 생성자는 유효한 접착 인터페이스를 작게 유지하면서 무관한 표현을 제거한다.

Sheafify는 접착 구문을 저장하여, 연산을 조기에 실행하지 않고도 쌍대곱과 재귀 리스트 같은 자유 구성을 가능하게 한다.

고정점을 명시적인 미해결 경계로 만듦으로써 구현이 아직 알지 못하는 것을 해결한 척하지 않게 한다.

형식적 정의가 불법 상태와 불가능한 의존적 타입을 만들어낼 때는, 유효한 덮개를 타입으로 인코딩하고 실행 가능한 접착 연산만 노출하라. 합성을 위해서는 자유 구성을 유지하라.

이 프로젝트는 구체적 및 추상적 Site/Sheaf 인스턴스를 갖춘 시연 저장소를 만들었고, 인코딩이 표현할 수 있는 것과 없는 것에 대한 더 명확한 경계를 제공했다. 고정점은 여전히 미해결이지만, 타입이 지정된 덮개 접근은 체 의존적 기계의 전체 무게를 들여오지 않고도 Haskell에서 층 연산을 사용 가능하게 만든다.