Haskell/GHC：如何在類型級自然編寫謂詞

Question

我可以發誓我最近看到一篇關於這方面的文章，但我找不到它。

我試圖做一個類型做國防部n數字的二進制編碼，但要做到這一點，我需要能夠寫在類型級別土黃謂詞：

{-# LANGUAGE MultiParamTypeClasses #-} 
{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE GADTs #-} 
{-# LANGUAGE TypeSynonymInstances #-} 
{-# LANGUAGE FunctionalDependencies #-} 
{-# LANGUAGE FlexibleInstances #-} 
{-# LANGUAGE FlexibleContexts #-} 
{-# LANGUAGE UndecidableInstances #-} 
module Modulo where 

-- (pseudo-)binary representation of 
-- numbers mod n 
-- 
-- e.g. Mod Seven contains 
-- Zero . Zero . Zero $ Stop 
-- Zero . Zero . One $ Stop 
-- Zero . One . Zero $ Stop 
-- Zero . One . One $ Stop 
-- One . Zero . Zero $ Stop 
-- One . Zero . One $ Stop 
-- One . One $ Stop 
data Mod n where 
    Stop :: Mod One 
    Zero :: Split n => Mod (Lo n) -> Mod n 
    One :: Split n => Mod (Hi n) -> Mod n 

-- type-level naturals 
data One 
data Succ n 
type Two = Succ One 

-- predicate to allow us to compare 
-- natural numbers 
class Compare n n' b | n n' -> b 

-- type-level ordering 
data LT 
data EQ 
data GT 

-- base cases 
instance Compare One One EQ 
instance Compare One (Succ n) LT 
instance Compare (Succ n) One GT 

-- recurse 
instance Compare n n' b => Compare (Succ n) (Succ n') b 

-- predicate to allow us to break down 
-- natural numbers by their bit structure 
-- 
-- if every number mod n can be represented in m bits, then 
class Split n where 
    type Lo n -- number of values mod n where the m'th bit is 0 
    type Hi n -- number of values mod n where the m'th bit is 1 

-- base case, n = 2 
-- for this, we only need m=1 bit 
instance Split Two where 
    type Lo Two = One -- 0 mod 2 
    type Hi Two = One -- 1 mod 2 

-- recurse 
-- if (Lo n) == (Hi n), then n = 2^m, so 
-- the values mod (n+1) will require one extra bit 
instance (Split n, Compare (Lo n) (Hi n) EQ) => Split (Succ n) where 
    type Lo (Succ n) = n -- all the numbers mod n will be prefixed by a 0 
    type Hi (Succ n) = One -- and one extra, which will be 10...0 

-- recurse 
-- if (Lo n) > (Hi n), then n < 2^m, so 
-- the values mod (n+1) still only require m bits 
instance (Split n, Compare (Lo n) (Hi n) GT) => Split (Succ n) where 
    type Lo (Succ n) = Lo (n)  -- we've got the same number of lower values 
    type Hi (Succ n) = Succ (Hi n) -- and one more higher value 

我現在實施吐出一堆編譯器錯誤的：

Nat.hs:60:8: 
    Conflicting family instance declarations: 
     type Lo Two -- Defined at Nat.hs:60:8-9 
     type Lo (Succ n) -- Defined at Nat.hs:74:8-9 

Nat.hs:61:8: 
    Conflicting family instance declarations: 
     type Hi Two -- Defined at Nat.hs:61:8-9 
     type Hi (Succ n) -- Defined at Nat.hs:75:8-9 

Nat.hs:66:10: 
    Duplicate instance declarations: 
     instance (Split n, Compare (Lo n) (Hi n) EQ) => Split (Succ n) 
     -- Defined at Nat.hs:66:10-62 
     instance (Split n, Compare (Lo n) (Hi n) GT) => Split (Succ n) 
     -- Defined at Nat.hs:73:10-62 

Nat.hs:67:8: 
    Conflicting family instance declarations: 
     type Lo (Succ n) -- Defined at Nat.hs:67:8-9 
     type Lo (Succ n) -- Defined at Nat.hs:74:8-9 

Nat.hs:68:8: 
    Conflicting family instance declarations: 
     type Hi (Succ n) -- Defined at Nat.hs:68:8-9 
     type Hi (Succ n) -- Defined at Nat.hs:75:8-9 

這讓我想我會寫關於我的謂詞錯誤，如果它認爲他們發生衝突。

我該怎麼做纔對？

Answer 1

衝突問題很簡單。 rules for overlapping type families很簡單：

在單個程序中使用的類型族的實例聲明只有在重疊實例的右側與重疊類型一致時纔會重疊。更正式地說，如果有一個替換使得實例的左側在語法上相同，則兩個實例聲明重疊。無論何時如此，實例的右側在相同的替換下也必須在語法上相等。

請注意，它指定句法上相等。考慮這兩個實例：

instance Split Two where 
    type Lo Two = One -- 0 mod 2 
    type Hi Two = One -- 1 mod 2 

instance Split (Succ n) where 
    type Lo (Succ n) = Lo (n) 
    type Hi (Succ n) = Succ (Hi n) 

Two被定義爲Succ One，和滑動型同義詞句法平等的目的擴大，所以這些都是在左手側相等;但右手不是，因此是錯誤。

您可能已經注意到我從上面的代碼中刪除了類上下文。更深層的問題，也許你爲什麼沒有想到會發生上述衝突，是因爲重複實例是衝突重複。對於實例選擇而言，類上下文一直被忽略，如果內存服務於我，這對於關聯類型系列來說是雙倍的，這對於非關聯類型系列來說在很大程度上是句法上的便利，並且可能不會受到類的約束期望。

現在，顯然這兩個實例應該是不同的，並且希望基於使用Compare的結果，它們之間進行選擇，因此該結果的類型必須爲類的參數，不僅僅是約束。你也在這裏混合具有函數依賴的類型族，這是不必要的尷尬。所以，從頂部開始，我們會保持基本類型：

-- type-level naturals 
data One 
data Succ n 
type Two = Succ One 

-- type-level ordering 
data LT 
data EQ 
data GT 

重寫Compare功能作爲一種家庭：

type family Compare n m :: * 
type instance Compare One One = EQ 
type instance Compare (Succ n) One = GT 
type instance Compare One (Succ n) = LT 
type instance Compare (Succ n) (Succ m) = Compare n m 

現在，辦理條件，我們將需要某種「流量控制」型家族。我將在這裏定義一些更一般的東西來引導和激勵;根據口味專門研究。

我們給它一個謂語，輸入和兩個分支選擇從：

type family Check pred a yes no :: * 

我們需要一個謂詞測試Compare的結果：

data CompareAs a 
type instance (CompareAs LT) LT yes no = yes 
type instance (CompareAs EQ) LT yes no = no 
type instance (CompareAs GT) LT yes no = no 
type instance (CompareAs LT) EQ yes no = no 
type instance (CompareAs EQ) EQ yes no = yes 
type instance (CompareAs GT) EQ yes no = no 
type instance (CompareAs LT) GT yes no = no 
type instance (CompareAs EQ) GT yes no = no 
type instance (CompareAs GT) GT yes no = yes 

這一套可怕的乏味的定義，批准，預測對於比較大型的類型值是相當嚴峻的。存在更多可擴展的方法（一種僞類型標籤和一種雙色注入，自然是一個明顯而有效的解決方案），但這有點超出了這個答案的範圍。我的意思是，我們只是在這裏進行類型級別的計算，我們不會得到荒謬的或任何東西。

在這種情況下，簡單的

是簡單地比較結果確定的情況下，分析功能：

type family CaseCompare cmp lt eq gt :: * 
type instance CaseCompare LT lt eq gt = lt 
type instance CaseCompare EQ lt eq gt = eq 
type instance CaseCompare GT lt eq gt = gt 

我將使用後者現在，但如果你想更復雜的條件句別處一種通用方法開始更有意義。

無論如何。我們可以分割......呃，Split類到非關聯型的家庭：

data Oops 

type family Lo n :: * 
type instance Lo Two = One 
type instance Lo (Succ (Succ n)) 
    = CaseCompare (Compare (Lo (Succ n)) (Hi (Succ n))) 
        Oops -- yay, type level inexhaustive patterns 
        (Succ n) 
        (Lo (Succ n)) 

type family Hi n :: * 
type instance Hi Two = One 
type instance Hi (Succ (Succ n)) 
    = CaseCompare (Compare (Lo (Succ n)) (Hi (Succ n))) 
        Oops -- yay, type level inexhaustive patterns 
        One 
        (Succ (Hi (Succ n))) 

這裏最顯著點是（貌似冗餘）使用的(Succ (Succ n)) --the原因是兩個Succ構造是必要的從Two區分參數，從而避免您看到的衝突錯誤。

請注意，爲了簡單起見，我已將所有內容都移至此處，因爲它完全是類型級別。如果您還希望根據上述計算處理不同的值（包括間接通過Mod類型），則可能需要返回適當的類定義，因爲這些是根據類型選擇項所需的，而不僅僅是選擇類型基於類型。