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

Question

我理解常规的定点型组合器,我想我理解高阶固定n型组合器,但HFix我不知道.您能举例说明一组数据类型及其可以应用的(手动派生的)固定点HFix.

Answer 1

自然参考是纸质通用编程,具有相互递归数据类型的固定点, 其中解释了multirec包.

HFix是一种用于相互递归数据类型的fixpoint类型组合器.本文第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将意味着我们携带一个偶数.我们需要为这个工作,它说这特定的构造函数,我们写闯民宅时,埃尔实例EO Even和EO Odd分别.

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

这些被用作限制HFunctor实例 为我.

现在让我们为偶数和奇数数据类型定义模式函子.我们使用图书馆的组合器.该:>:类型构造标记及其类型索引值:

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和hto函数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