Tweag 以顯式膠合操作在 Haskell 中表示層

Arnaud Spiwack 想在 Haskell 中表示層，但教科書定義帶來一個實際問題：篩包含許多同一匹配資訊的冗餘表示，而其依賴的拉回構造對 Haskell 而言依賴型別負擔過重。顯而易見的做法——逐字翻譯定義——會使非法狀態可被表示，並讓程式淹沒在無關資料中。

他首先圍繞算術表達式建立一個具體範例。預層可沿表達式拉回值，但所需的條件運算需要一個層，在布林覆蓋上膠合兩個分支。因此實作將膠合做成顯式的型別類別操作，再推廣為 Site，其具型別的 Cover 與 Gen 族描述哪些片段可以組裝。

具型別的 site 移除了拉回篩的負擔：膠合可作用於任意箭頭，而生成元不必表示為實際箭頭。積、指數、Yoneda 嵌入、餘積與遞迴列表便可依同樣風格定義。Sheafify 作為自由層構造，儲存膠合操作而非過早求值，而 PFun 攜帶指數所需的變異性。

結果是一個示範儲存庫，以及抽象概念的 Haskell 風格實作，而非聲稱每個數學細節都消失。Spiwack 明確將不動點留為未解，但該專案把一個對語言而言過於寬鬆的定義轉化為具型別、可操作的建構積木，並使其餘未知變得精確。

將覆蓋表示為型別，然後顯式膠合

字面篩編碼冗餘的匹配族值，並允許本應不可能的狀態。

指數所需的拉回篩要求依賴型別，超出 Haskell 實作能舒適表達的範圍。

具型別的覆蓋與生成元使有效膠合介面保持精簡，同時移除無關表示。

Sheafify 儲存膠合語法，允許餘積與遞迴列表等自由構造，而不提前執行操作。

將不動點明確設為未解邊界，可防止實作假裝解決它尚不知道的事。

當形式定義產生非法狀態與不可能的依賴型別時，將有效覆蓋編碼進型別，並只暴露可執行的膠合操作。為組合保留自由構造。

該專案產出一個示範儲存庫，包含具體與抽象的 Site/Sheaf 實例，並更清楚劃定此編碼能與不能表達的邊界。不動點仍未解，但具型別覆蓋的方法使層操作可在 Haskell 中使用，而無需引入篩依賴機制的全部重量。