Haskellのmultirecパッケージで `HFix`はどのように動作しますか？

Question

私は固定小数点型のコンビネータを理解していますが、高次の固定n型のコンビネータは分かりますが、HFixはわかりません。 HFixを適用できる一連のデータ型とその（手作業で派生した）固定小数点の例を挙げてください。

Answer 1

ここで、multirec packageについて説明します。

HFixは、相互に再帰的なデータ型用の固定小数点型の組み合わせです。 これはよく紙に3.2節で説明したが、アイデアは、このパターン一般化する です：彼らは、それが固定点を超えるんどのように多くの種類を制限するには

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

に

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

を*^nのかわりに を使用してください。それらは、 以上の相互に再帰的なASTデータ型の例を示しています。私はおそらく最も単純な例を提供します。

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

たちは偶数を持ち歩いていることを意味します

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

EO Evenセクション4.1

に行われているように、私たちは、このデータ型のため、家族の特定のGADTをご紹介しましょう：私たち にHFIXこのデータ型をしてみましょう。 EO Evenと EO Oddをそれぞれ書くときに、具体的なコンストラクタ を参照するElインスタンスが必要です。

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

これらはIためHFunctor instance の制約として使用されています。

ここで、偶数データ型と奇数データ型のパターンファンクタを定義します。 ライブラリからコンビネータを使用します。:>:型コンストラクタタグ その型のインデックスを持つ値：

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と同型です奇数、私たちはそれFamのインスタンス作れば、私たちは hfrom and hto functions を使用することができます。

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) 

代数が自分Int値にEvenとOdd Sを回すと別の愚かなテスト：

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