Início / coding / Perguntas / 79322925
Accepted
Wheat Wizard
Asked: 2025-01-02 14:20:53 +0800 CST

Codificação Böhm-Beraducci de Fix

  • 772

Tenho o functor de ponto fixo definido da seguinte forma:

newtype Fix f =
  Fix
    { unfix ::
      f (Fix f)
    }

Gostaria de definir uma função que recebe a Fix fe fornece sua codificação Böhm-Beraducci. Então, isso deve ter o tipo:

cata :: Fix f -> (forall a. (f a -> a) -> a)

Posso facilmente definir uma função como essa, mas com a restrição adicional que fé um Functor, mas estou com dificuldades sem essa restrição.

Intuitivamente, quero pegar o AST e substituir todas as instâncias do Fixconstrutor por uma função de entrada, no entanto, na prática, isso parece exigir uma Functorinstância para F. Mas, no meu entendimento, a codificação Böhm-Beraducci deve existir mesmo quando fnão é um Functor.

Sinto que estou esquecendo de algo simples aqui. Há alguma definição que estou esquecendo? Se Functorfor realmente necessário, por quê? Quando a codificação Böhm-Beraducci requer restrições adicionais como essa?

haskell

1 respostas

  1. Best Answer

    Dando uma olhada rápida no artigo original , parece que a codificação Böhm-Berarducci representa álgebras de termos usando tipos do Sistema F.

    Álgebras de termos envolvem essencialmente um implícito fque é sempre um functor.

    Haskell vai além disso e permite pontos fixos em nível de tipo em qualquer f, mesmo aqueles que não podem ser transformados em functores.

    Um exemplo famoso é o tipo recursivo negativo newtype R a = R { unR :: R a -> a }. O sistema de tipos Haskell permite essa definição de tipo. Usando isso R asozinho, e sem recursão de nível de termo, podemos derivar fix :: forall a . (a -> a) -> a(um exercício curto, mas não trivial, a propósito).

    O System F, por outro lado, não pode ser tão geral. Se tivéssemos R ano System F, também teríamos fix, portanto fix id :: forall a . apoderia ser usado para habitar qualquer tipo de System F. Mas sabemos que o System F é consistente, então isso não pode acontecer.

    • 2

relate perguntas