haskell - Hasfell的multirec软件包中的“HFix”如何工作？

我了解常规的定点类型组合器，并且我想了解高阶固定n类型组合器，但是HFix令我难以理解。您能否举一个可以应用HFix的数据类型及其固定点的例子。

最佳答案

自然参考是纸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 Even和EO Odd同构，我们可以使用
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转换为其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