`HFix`如何在Haskell的multirec包中工作？

Question

我瞭解常規定點類型combinator，我想我理解高階固定n型combinators，但HFix避開了我。你能給出一個數據類型的例子和他們的（手工派生的）固定點，你可以應用HFix。

Answer 1

自然參考文獻Generic programming with fixed points for mutually recursive datatypes 其中multirec package的解釋。

HFix是用於相互遞歸數據類型的固定點類型組合器。 它在3.2節中的文件很好的解釋，但這個想法是 來概括這種模式：

Fix :: (∗ -> ∗) -> ∗ 
Fix2 :: (∗ -> ∗ -> ∗) -> (∗ -> ∗ -> ∗) -> ∗ 

到

Fixn :: ((∗ ->)^n * ->)^n ∗ 
≈ 
Fixn :: (*^n -> *)^n -> * 

要限制它有多少種做一個固定點上，他們使用類型構造函數 而不是*^n。他們給出了一個AST數據類型的例子，這個數據類型通過 三種類型相互遞歸。相反，我給你提供的可能是最簡單的例子。讓 我們的hFIX這個數據類型：

data Even = Zero | ESucc Odd deriving (Show,Eq) 
data Odd = OSucc Even  deriving (Show,Eq) 

讓我們來介紹一下家庭的具體GADT該數據類型作爲在第4.1節

data EO :: * -> * where 
    E :: EO Even 
    O :: EO Odd 

EO Even做將意味着我們圍繞偶數攜帶。 我們需要使用El實例才能正常工作，這說明在分別編寫EO Even和EO Odd時我們指的是哪個特定的構造函數 。

instance El EO Even where proof = E 
instance El EO Odd where proof = O 

這些被用作用於HFunctor instance 爲I約束。

讓我們現在定義偶數和奇數數據類型的模式仿函數。 我們使用庫中的組合器。該:>:類型構造標籤 其類型的索引值：

type PFEO = U  :>: Even -- ≈ Zero ::()  -> EO Even 
     :+: I Odd :>: Even -- ≈ ESucc :: EO Odd -> EO Even 
     :+: I Even :>: Odd -- ≈ OSucc :: EO Even -> EO Odd 

現在我們可以使用HFix綁圍繞這種模式函子結：

type Even' = HFix PFEO Even 
type Odd' = HFix PFEO Odd 

現在這些同構於偶數和EO EO奇怪，我們可以使用 hfrom and hto functions 如果我們把它Fam一個實例：

type instance PF EO = PFEO 

instance Fam EO where 
    from E Zero  = L (Tag U) 
    from E (ESucc o) = R (L (Tag (I (I0 o)))) 
    from O (OSucc e) = R (R (Tag (I (I0 e)))) 
    to E (L (Tag U))   = Zero 
    to E (R (L (Tag (I (I0 o))))) = ESucc o 
    to O (R (R (Tag (I (I0 e))))) = OSucc e 

一個簡單的小測試：

test :: Even' 
test = hfrom E (ESucc (OSucc Zero)) 

test' :: Even 
test' = hto E test 

*HFix> test' 
ESucc (OSucc Zero) 

與代數轉向Even和Odd s到他們的Int值的另一種愚蠢的測試：

newtype Const a b = Const { unConst :: a } 

valueAlg :: Algebra EO (Const Int) 
valueAlg _ = tag (\U    -> Const 0) 
      & tag (\(I (Const x)) -> Const (succ x)) 
      & tag (\(I (Const x)) -> Const (succ x)) 

value :: Even -> Int 
value = unConst . fold valueAlg E