Come funziona `HFix` nel pacchetto multirec di Haskell?

Question

Capisco il normale combinatore di tipo a virgola fissa e penso di capire i combinatori di tipo fixed-n di ordine superiore, ma lo HFix mi sfugge. Puoi dare un esempio di un insieme di tipi di dati e dei loro punti fissi (derivati ​​manualmente) che puoi applicare a HFix.

Answer 1

Il riferimento naturale è il documento Generic programming with fixed points for mutually recursive datatypes in cui viene spiegato lo multirec package.

HFix è un combinatore di tipo fixpoint per tipi di dati reciprocamente ricorsivi. E 'ben spiegato nella sezione 3.2 nella carta, ma l'idea è generalizzare questo schema:

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

a

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

Per limitare il numero di tipi fa un punto fisso sopra, hanno utilizzare i costruttori di tipi anziché *^n. Forniscono un esempio di un tipo di dati AST, reciprocamente ricorsivo su tre tipi nella carta. Ti offro forse l'esempio più semplice invece. Facciamo noi HFix questo tipo di dati:

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

introduciamo la GADT specifica famiglia per questo tipo di dati, come avviene nella sezione 4,1

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

EO Even significherà che stiamo portando in giro un numero pari. Abbiamo bisogno che le istanze di El funzionino, il che indica quale costruttore specifico a cui ci riferiamo quando scriviamo rispettivamente EO Even e EO Odd.

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

sono utilizzati come vincoli per il HFunctor instance per I.

Definiamo ora il funtore di modello per il tipo di dati pari e dispari. Utilizziamo i combinatori dalla libreria.I :>: tipo costruttore tag un valore con il suo indice di tipo:

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

Ora possiamo usare HFix di legare il nodo attorno a questo modello funtore:

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

Queste sono ora isomorfi alle PO Anche e EO strano, e siamo in grado di utilizzare il hfrom and hto functions se facciamo un esempio di 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 

Un semplice piccolo test:

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

test' :: Even 
test' = hto E test 

*HFix> test' 
ESucc (OSucc Zero) 

Un altro test sciocco con un'algebra girando Even e Odd s per il loro valore 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