Aqui está um quebra-cabeça de programação funcional que envolve estruturas de dados de laço e infinitas. Há um pouco de fundo, então fique firme.

A configuração. Vamos definir um tipo de dados representando tipos de dados recursivos:

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

isto ét ::= μα. t | α | t → t | ⊥ | ⊤. Observe que ⊥ indica o tipo sem habitantes, enquanto ⊤ indica o tipo com todos os habitantes. Observe que(μα. α) = ⊥, como μ é ummenos operador de ponto fixo.

Podemos interpretar um tipo de dados recursivo como uma árvore infinita, resultante de desdobramentos repetidosμα. t parat[α ↦ μα. t]. (Para uma descrição formal desse processo, consultehttp://lucacardelli.name/Papers/SRT.pdf) Em Haskell, podemos definir um tipo de árvores preguiçosas, que não possuem μ-binders ou variáveis:

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

e, em Haskell comum, uma função de conversão de um para o outro:

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)

No entanto, há um problema com esta função: não é produtivo. Se você correrconvL [] (SMu "x" (SVar "x")) você terá loop infinito. Preferimos terLBottom nesse caso. Um exercício interessante é consertar diretamente essa função para que seja produtiva; no entanto, nesta pergunta, quero resolver o problema de maneira diferente.

Produtividade com a modalidade de atraso. Quando construímos estruturas de dados cíclicos como acima, precisamos garantir que não utilizemos os resultados de nossos cálculos antes de construí-los. A modalidade de atraso é uma maneira de garantir que escrevamos programas produtivos (loop não infinito). A ideia básica é simples: se o tipoInt significa que eu tenho um número inteiro hoje, eu defino um construtor de tipoD, de modo aD Int significa que eu tenho um valor do tipoInt amanhã. D é um Functor e um Candidato (mas NÃO uma 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

ComD, definimos um operador de ponto de fixação: ele diz que para construir um valor dea, você pode ter acesso aoa você está construindo, desde que você o use apenasamanhã.

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

Por exemplo, um fluxo consiste em um valora Eu tenho hoje, e um fluxoStream a que eu tenho que produzir amanhã.

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

UsandofixD, Eu posso definir ummap função em fluxos que égarantido produtivo, pois a chamada recursiva paramap é usado apenas para produzir valores necessários amanhã.

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

O problema. Aqui está uma variante deLTerm com uma modalidade de atraso explícita.

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

UsandofixD (nenhuma referência recursiva não estruturalmente permitida), como eu escrevo uma funçãoconv :: STerm -> Term (ouconv :: STerm -> D Term)? Um caso de teste particularmente interessante éSMu "x" (SArrow STop (SMu "y" (SVar "x"))); não deve haver fundos na estrutura resultante!

Atualizar. Eu descartei acidentalmente recursão estrutural emSTerm, que não era o objetivo da pergunta; Eu reformulei para remover essa restrição.