Jak działa `HFix` w pakiecie multirec Haskell?

Question

Rozumiem regularny kombinator typu stałoprzecinkowego i myślę, że rozumiem kombinatory typu fixed-n wyższego rzędu, ale wymyka mi się HFix. Czy mógłbyś podać przykład zestawu typów danych i ich (ręcznie wyprowadzonych) stałych punktów, które możesz zastosować HFix do.

Answer 1

Naturalną referencją jest papier Generic programming with fixed points for mutually recursive datatypes , gdzie wyjaśniono, że multirec package.

HFix to kombinator typu fixpoint do wzajemnie rekurencyjnych typów danych. Jest dobrze wyjaśnione w rozdziale 3.2 na papierze, ale idea jest uogólniać tego wzoru:

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

do

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

Aby ograniczyć liczbę rodzajów robi punkt stały się one używaj konstruktorów typu zamiast *^n. Podają przykład typu danych AST, rekurencyjnie nawzajem w stosunku do trzy rodzaje papieru. Zamiast tego proponuję ci najprostszy przykład. Niech nas HFix Ten typ danych:

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

Pozwól nam przedstawić konkretny GADT rodzinne dla tego typu danych, jak odbywa się to w punkcie 4.1

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

EO Even będzie oznaczać, że jesteśmy roznosić parzystej liczbie. Potrzebujemy instancji El, aby to działało, co mówi, który konkretny konstruktor mamy na myśli, pisząc odpowiednio: EO Even i EO Odd.

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

Są one używane jako ograniczenia dla HFunctor instance do I.

Zdefiniujmy teraz wzór funktora dla parzystego i nieparzystego typu danych. Używamy kombinatorów z biblioteki.W :>: typu tagów konstruktora wartości z indeksem typu:

type PFEO = U  :>: Even -- ≈ Zero ::()  -> EO Even 
     :+: I Odd :>: Even -- ≈ ESucc :: EO Odd -> EO Even 
     :+: I Even :>: Odd -- ≈ OSucc :: EO Even -> EO Odd 

Teraz możemy użyć HFix zawiązać węzeł wokół tego wzorca funktora:

type Even' = HFix PFEO Even 
type Odd' = HFix PFEO Odd 

Są teraz izomorficzna EO Nawet i EO dziwne, i możemy użyć hfrom and hto functions jeśli robimy to wystąpienie 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 

Prosty mały test:

test :: Even' 
test = hfrom E (ESucc (OSucc Zero)) 

test' :: Even 
test' = hto E test 

*HFix> test' 
ESucc (OSucc Zero) 

Kolejny głupi test o Algebra obracając Even i Odd s do ich wartości 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