5

通常の固定小数点型コンビネータと高階固定n型コンビネータは理解できたと思いますが、わかりHFixません。適用できるデータ型のセットとそれらの（手動で導出された）固定小数点の例を挙げてくださいHFix。

4

1 に答える 1

5

自然な参照は 、multirecパッケージが説明されている相互再帰データ型の固定小数点を使用した紙のジェネリックプログラミングです。

HFixは、相互に再帰的なデータ型の固定小数点型コンビネータです。論文のセクション3.2で十分に説明されていますが、アイデアはこのパターンを一般化することです。

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

に

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

固定小数点を実行する型の数を制限するために、*^nの代わりに型コンストラクターを使用します。それらは、論文の3つのタイプにわたって相互に再帰的な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これを機能させるには、Elインスタンスが必要です。これは、それぞれを作成するときに参照している特定のコンストラクターを示しEO Oddます。

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

これらは、Iの インスタンスの制約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偶数およびEO奇数と同型であり 、次 のインスタンスにすると、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し、Oddsを使用する別のばかげたテスト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
于 2012-03-15T20:56:48.593 に答える