Fix e Mu isomórfico

No recursion-schemespacote, os seguintes tipos são definidos:

newtype Fix f = Fix (f (Fix f))

newtype Mu f = Mu (forall a. (f a -> a) -> a)

Eles são isomórficos? Se sim, como você prova isso?

Eles são isomórficos?

Sim, eles são isomórficos em Haskell. Consulte Qual é a diferença entre Fix, Mu e Nu no pacote do esquema de recursão de Ed Kmett para algumas observações adicionais.

Se sim, como você prova isso?

Vamos começar definindo funções para realizar as conversões:

muToFix :: Mu f -> Fix f
muToFix (Mu s) = s Fix

fixToMu :: Functor f => Fix f -> Mu f
fixToMu t = Mu (\alg -> cata alg t)

Para mostrar que essas funções testemunham um isomorfismo, devemos mostrar que:

muToFix . fixToMu = id
fixToMu . muToFix = id

De Fixe para trás

Uma das direções do isomorfismo sai um pouco mais direta do que a outra:

muToFix (fixToMu t) = t
muToFix (fixToMu t)  -- LHS
muToFix (Mu (\f -> cata f t))
(\f -> cata f t) Fix
cata Fix t  -- See below.
t  -- LHS = RHS

A passagem final acima,, cata Fix t = tpode ser verificada através da definição de cata:

cata :: Functor f => (f a -> a) -> Fix f -> a
cata alg = alg . fmap (cata alg) . unfix

cata Fix t, então é Fix (fmap (cata Fix) (unfix t)). Podemos usar a indução para mostrar que deve ser t, pelo menos para um finito t(fica mais sutil com estruturas infinitas - veja o adendo no final desta resposta). Há duas possibilidades a considerar:

• unfix t :: f (Fix f)está vazio, sem posições recursivas para cavar. Nesse caso, deve ser igual a fmap absurd zpara alguns z :: f Void, e assim:

  cata Fix t
  Fix (fmap (cata Fix) (unfix t))
  Fix (fmap (cata Fix) (fmap absurd z))
  Fix (fmap (cata Fix . absurd) z)
  -- fmap doesn't do anything on an empty structure.
  Fix (fmap absurd z)
  Fix (unfix t)
  t

• unfix tnão está vazio. Nesse caso, pelo menos sabemos que fmap (cata Fix)não podemos fazer nada além de aplicar cata Fixnas posições recursivas. A hipótese de indução aqui é que isso deixará essas posições inalteradas. Temos então:

  cata Fix t
  Fix (fmap (cata Fix) (unfix t))
  Fix (unfix t)  -- Induction hypothesis.
  t

(Por fim, cata Fix = id é um corolário de Fix :: f (Fix f) -> Fix xser uma álgebra inicial F. Recorrer diretamente a esse fato no contexto dessa prova provavelmente seria um atalho demais.)

De Mue para trás

Dado muToFix . fixToMu = id, para provar que fixToMu . muToFix = idbasta provar:

• aquele muToFix é injetivo, ou

• isso fixToMué subjetivo.

Vamos pegar a segunda opção e revisar as definições relevantes:

newtype Mu f = Mu (forall a. (f a -> a) -> a)

fixToMu :: Functor f => Fix f -> Mu f
fixToMu t = Mu (\alg -> cata alg t)

fixToMuser adjetivo significa, então, que, dado qualquer específico Functor f, todas as funções do tipo forall a. (f a -> a) -> apodem ser definidas como \alg -> cata alg t, para alguns específicos t :: Fix f. A tarefa, então, torna-se catalogar oforall a. (f a -> a) -> a funções e verificar se todas elas podem ser expressas nessa forma.

Como podemos definir uma forall a. (f a -> a) -> afunção sem nos apoiarmos fixToMu? Seja como for, deve envolver o uso da f a -> aálgebra fornecida como argumento para obter um aresultado. A rota direta seria aplicá-la a algum f avalor. Uma ressalva importante é que, como aé polimórfico, devemos ser capazes de conjurar o referido f avalor para qualquer escolha a. Essa é uma estratégia viável desde que fexistam valores. Nesse caso, podemos fazer:

fromEmpty :: Functor f => f Void -> forall a. (f a -> a) -> a
fromEmpty z = \alg -> alg (fmap absurd z)

Para tornar a notação mais clara, vamos definir um tipo para itens que podemos usar para definir forall a. (f a -> a) -> afunções:

data Moo f = Empty (f Void)

fromMoo :: Functor f => Moo f -> forall a. (f a -> a) -> a
fromMoo (Empty z) = \alg -> alg (fmap absurd z)

Além da rota direta, há apenas uma outra possibilidade. Dado que fé a Functor, se de alguma forma tivermos um f (Moo f)valor, podemos aplicar a álgebra duas vezes, sendo a primeira aplicação sob a fcamada externa , via fmape fromMoo:

fromLayered :: Functor f => f (Moo f) -> forall a. (f a -> a) -> a
fromLayered u = \alg -> alg (fmap (\moo -> fromMoo moo alg) u)

Tendo em conta que nós também podemos fazer forall a. (f a -> a) -> afora de f (Moo f)valores, faz sentido adicioná-los como um caso de Moo:

data Moo f = Empty (f Void) | Layered (f (Moo f))

Por conseguinte, fromLayeredpode ser incorporado a fromMoo:

fromMoo :: Functor f => Moo f -> forall a. (f a -> a) -> a
fromMoo = \case
    Empty z -> \alg -> alg (fmap absurd z)
    Layered u -> \alg -> alg (fmap (\moo -> fromMoo moo alg) u)

Observe que, ao fazer isso, passamos sorrateiramente da aplicação algsob uma fcamada para a aplicação recursiva algsob um número arbitrário de fcamadas.

Em seguida, podemos observar que um f Voidvalor pode ser injetado no Layeredconstrutor:

emptyLayered :: Functor f => f Void -> Moo f
emptyLayered z = Layered (fmap absurd z)

Isso significa que na verdade não precisamos do Emptyconstrutor:

newtype Moo f = Moo (f (Moo f))

unMoo :: Moo f -> f (Moo f)
unMoo (Moo u) = u

E o Emptycaso fromMoo? A única diferença entre os dois casos é que, no Emptycaso, temos em absurdvez de \moo -> fromMoo moo alg. Como todas as Void -> afunções são absurd, também não precisamos de um Emptycaso separado :

fromMoo :: Functor f => Moo f -> forall a. (f a -> a) -> a
fromMoo (Moo u) = \alg -> alg (fmap (\moo -> fromMoo moo alg) u)

Um possível ajuste cosmético é inverter os fromMooargumentos, para que não seja necessário escrever o argumento fmapcomo lambda:

foldMoo :: Functor f => (f a -> a) -> Moo f -> a
foldMoo alg (Moo u) = alg (fmap (foldMoo alg) u)

Ou, mais pointfree:

foldMoo :: Functor f => (f a -> a) -> Moo f -> a
foldMoo alg = alg . fmap (foldMoo alg) . unMoo

Neste ponto, uma segunda olhada em nossas definições sugere que alguma renomeação esteja em ordem:

newtype Fix f = Fix (f (Fix f))

unfix :: Fix f -> f (Fix f)
unfix (Fix u) = u

cata :: Functor f => (f a -> a) -> Fix f -> a
cata alg = alg . fmap (cata alg) . unfix

fromFix :: Functor f => Fix f -> forall a. (f a -> a) -> a
fromFix t = \alg -> cata alg t

E aí está: todas as forall a. (f a -> a) -> afunções têm a forma \alg -> cata alg tpara algumas t :: Fix f. Portanto, fixToMué surjetivo, e temos o isomorfismo desejado.

Termo aditivo

Nos comentários, uma questão pertinente foi levantada sobre a aplicabilidade do argumento de indução na cata Fix t = tderivação. No mínimo, as leis e a parametridade dos functores garantem que fmap (cata Fix)não criarão trabalho extra (por exemplo, não ampliarão a estrutura ou introduzirão posições recursivas adicionais para serem exploradas), o que justifica por que entrar nas posições recursivas é tudo o que assuntos na etapa indutiva da derivação. Sendo assim, se tfor uma estrutura finita, o caso base de um vazio f (Fix t)será finalmente alcançado e tudo ficará claro. Se permitirmos tser infinitos, no entanto, podemos continuar descendo sem parar, fmapdepois fmapdepois fmap, sem nunca chegar ao caso base.

A situação com estruturas infinitas, no entanto, não é tão terrível quanto possa parecer à primeira vista. A preguiça, que é o que viabiliza estruturas infinitas, em primeiro lugar, permite consumir estruturas infinitas preguiçosamente:

GHCi> :info ListF
data ListF a b = Nil | Cons a b
    -- etc.
GHCi> ones = Fix (Cons 1 ones)
GHCi> (\(Fix (Cons a _)) -> a) (cata Fix ones)
1
GHCi> (\(Fix (Cons _ (Fix (Cons a _)))) -> a) (cata Fix ones)
1

Enquanto a sucessão de posições recursivas se estende infinitamente, podemos parar a qualquer momento e obter resultados úteis nos ListFcontextos funcionais circundantes . Vale a pena repetir que esses contextos não são afetados fmape, portanto, qualquer segmento finito da estrutura que possamos consumir não será afetado porcata Fix .

Este adiamento preguiça reflete como, como mencionado em outro lugar nesta discussão, preguiça desaba a distinção entre os pontos fixos Mu, Fixe Nu. Sem preguiça, Fixnão basta codificar a corecursão produtiva e, portanto, precisamos mudar para Nuo maior ponto fixo. Aqui está uma pequena demonstração da diferença:

GHCi> :set -XBangPatterns
GHCi> -- Like ListF, but strict in the recursive position.
GHCi> data SListF a b = SNil | SCons a !b deriving Functor
GHCi> ones = Nu (\() -> SCons 1 ()) ()
GHCi> (\(Nu c a) -> (\(SCons a _) -> a) (c a)) ones
1
GHCi> ones' = Fix (SCons 1 ones')
GHCi> (\(Fix (SCons a _)) -> a) ones'
^CInterrupted.