¿Cómo funciona `HFix` en el paquete multirres de Haskell?

Question

Entiendo el combinador de tipo de punto fijo regular y creo que entiendo los combinadores de tipo fijo-n de orden superior, pero HFix me elude. Podría dar un ejemplo de un conjunto de tipos de datos y sus puntos fijos (derivados manualmente) a los que puede aplicar HFix.

Answer 1

La referencia natural es el documento Generic programming with fixed points for mutually recursive datatypes donde se explica multirec package.

HFix es un combinador de tipo de punto fijo para tipos de datos mutuamente recursivos. Está bien explicado en la Sección 3.2 en el papel, pero la idea es generalizar este patrón:

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

a

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

Para restringir el número de tipos que lo hace un punto fijo sobre, se use constructores de tipo en lugar de *^n. Dan un ejemplo de un tipo de datos AST, mutuamente recursivo sobre tres tipos en el documento. Te ofrezco quizás el ejemplo más simple en su lugar. Deje nos FIXh este tipo de datos:

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

vamos a introducir el GADT familia específica para este tipo de datos como se hace en la sección 4,1

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

EO Even significará que estamos llevando alrededor de un número par. Necesitamos instancias de El para que esto funcione, que indica a qué constructor específico se refiere al escribir EO Even y EO Odd respectivamente.

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

Estos se utilizan como restricciones para el HFunctor instance para I.

Definamos ahora el funtor de patrones para el tipo de datos pares e impares. Usamos los combinadores de la biblioteca.Las etiquetas constructor :>: tipo un valor con su índice de tipos:

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

Ahora podemos usar HFix para atar el nudo alrededor de este patrón funtor:

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

Estos son ahora isomorfo a EO Incluso y EO impar, y podemos usar el hfrom and hto functions si lo hacemos una instancia de 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 simple pequeña prueba:

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

test' :: Even 
test' = hto E test 

*HFix> test' 
ESucc (OSucc Zero) 

Otra prueba tonto con un álgebra girando Even y Odd s Int a su valor:

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