Aquí hay un rompecabezas de programación funcional que involucra estructuras de datos infinitos y de bucle. Hay un poco de fondo, así que agárrate fuerte.

El ajuste. Definamos un tipo de datos que represente tipos de datos recursivos:

type Var = String
data STerm = SMu Var STerm
           | SVar Var
           | SArrow STerm STerm
           | SBottom
           | STop
   deriving (Show)

es decirt ::= μα. t | α | t → t | ⊥ | ⊤. Tenga en cuenta que ⊥ denota el tipo sin habitantes, mientras que ⊤ denota el tipo con todos los habitantes. Tenga en cuenta que(μα. α) = ⊥, como μ es unmenos operador de punto fijo.

Podemos interpretar un tipo de datos recursivo como un árbol infinito, que surge del despliegue repetidoμα. t at[α ↦ μα. t]. (Para una descripción formal de este proceso, veahttp://lucacardelli.name/Papers/SRT.pdf) En Haskell, podemos definir un tipo de árboles perezosos, que no tienen ligantes ni variables:

data LTerm = LArrow LTerm LTerm
           | LBottom
           | LTop
   deriving (Show)

y, en Haskell ordinario, una función de conversión de uno a otro:

convL :: [(Var, LTerm)] -> STerm -> LTerm
convL _ STop    = LTop
convL _ SBottom = LBottom
convL ctx (SArrow t1 t2) = LArrow (convL ctx t1) (convL ctx t2)
convL ctx (SVar v)
    | Just l <- lookup v ctx = l
    | otherwise = error "unbound variable"
convL ctx (SMu v t) = fix (\r -> convL ((v, r) : ctx) t)

Sin embargo, hay un problema con esta función: no es productiva. Si tu corresconvL [] (SMu "x" (SVar "x")) Tendrás un bucle infinito. Preferiríamos obtenerLBottom en este caso. Un ejercicio interesante es arreglar directamente esta función para que sea productiva; Sin embargo, en esta pregunta quiero resolver el problema de manera diferente.

Productividad con la modalidad de retraso. Cuando construimos estructuras de datos cíclicos como se indicó anteriormente, debemos asegurarnos de no utilizar los resultados de nuestros cálculos antes de haberlos construido. La modalidad de retraso es una forma de garantizar que escribamos programas productivos (no de bucle infinito). La idea básica es simple: si el tipoInt significa que tengo un número entero hoy, defino un constructor de tiposD, así que esoD Int significa que tengo un valor de tipoInt mañana. D es un Functor y un Aplicativo (pero NO una mónada).

-- D is abstract; you are not allowed to pattern match on it
newtype D a = D a
   deriving (Show)

instance Functor D where
    fmap f (D a) = D (f a)

instance Applicative D where
    D f <*> D a = D (f a)
    pure x = D x

ConD, definimos un operador de punto fijo: dice que para construir un valor dea, puede tener acceso a laa estás construyendo, siempre y cuando solo lo usesmañana.

fixD :: (D a -> a) -> a
fixD f = f (D (fixD f))

Por ejemplo, un flujo consta de un valora Tengo hoy, y una corrienteStream a que tengo que producir mañana.

data Stream a = Cons a (D (Stream a))

UtilizandofixD, Puedo definir unmap funcionar en secuencias que esgarantizado ser productivo, ya que la llamada recursiva amap solo se usa para generar valores que se necesitan mañana.

instance Functor Stream where
    fmap f = fixD $ \go (Cons x xs) -> Cons (f x) (go <*> xs)

El problema. Aquí hay una variante deLTerm con una modalidad explícita de retraso.

data Term = Arrow (D Term) (D Term)
          | Bottom
          | Top
    deriving (Show)

UtilizandofixD (no se permiten referencias recursivas no estructurales), ¿cómo escribo una función?conv :: STerm -> Term (oconv :: STerm -> D Term)? Un caso de prueba particularmente interesante esSMu "x" (SArrow STop (SMu "y" (SVar "x"))); ¡No debería haber fondos en la estructura resultante!

Actualizar. Accidentalmente descarté la recursión estructural enSTerm, que no era la intención de la pregunta; He vuelto a redactar para eliminar esa restricción.