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

Question

我了解常规定点型组合器，我想我了解高阶定 n 型组合器，但是 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)

让我们像第 4.1 节中所做的那样，为该数据类型引入特定于系列的 GADT

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 s 到他们的 Int值(value):

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