Prism: uma linguagem funcional impura com efeitos tipados

• Prism é um compilador experimental que não esconde efeitos como variáveis mutáveis, exceções e streams, expondo-os nos tipos, mas ainda mantém mudanças locais não observáveis externamente como tipos puros, como Int -> Int
• A ideia central combina handlers de efeitos algébricos e polimorfismo de linhas (row polymorphism): os efeitos são mesclados à linha do tipo de função, e os handlers tratam apenas os rótulos necessários antes de encaminhar o restante
• O mesmo sistema de efeitos expressa exceções, geradores/streams, lentes, estado com var e fluxos fail/guard; alguns caminhos são baixados sem listas intermediárias nem composição em runtime
• Do lado de desempenho, combina evidence passing com contagem de referências Perceus para evitar alocação por chamada de efeito e otimiza atualizações funcionais de valores com posse única como mutações in-place
• Prism oferece LLVM IR, MLIR, runtime em C, interpretador em Rust, modelo em Lean 4 e playground em WASM, permitindo inspecionar diretamente a inferência de tipos e os resultados de lowering

---

Mudanças invisíveis externamente e efeitos tipados

• O ponto de partida do Prism é que uma função fib que usa var e atribuição internamente também pode parecer uma função pura para um observador externo
  • O exemplo fib atualiza duas variáveis in-place, mas não expõe estado para fora da função
  • O tipo é Int -> Int, e o efeito não aparece no tipo
• Prism é um compilador funcional de prova de conceito desenvolvido ao longo dos últimos 3 anos, modelando efeitos com base em ideias modernas de tipos das famílias OCaml 5, Haskell e Koka
• A direção central não é evitar efeitos, mas colocá-los no sistema de tipos e otimizar para que o compilador elimine seus custos

Efeitos funcionam como interfaces

• Os efeitos do Prism seguem a abordagem de handlers de efeitos algébricos, em que operações são declaradas e handlers atribuem significado a essas operações
  • effect Gen { ctl yield(Int) : Unit } declara a operação yield
  • Em fn produce(n) : !{Gen} Unit, !{Gen} indica no tipo que a função executa yield
• Mesmo para o mesmo produtor, o significado muda conforme a continuation k é tratada
  • total soma os valores de yield
  • count conta o número de chamadas a yield
  • Descartar k vira uma exceção; chamá-la uma vez vira estado ou gerador; chamá-la várias vezes vira comportamento de busca
• O exemplo do efeito Amb expressa a busca por triplas pitagóricas com choose e reject
  • choose(n) fornece valores no intervalo 0..n-1
  • O handler retoma a mesma continuation para cada candidato, criando uma árvore de busca
• Diferentemente do OCaml 5, Prism inclui efeitos nos tipos e não exige empilhar camadas manualmente como em stacks de monad transformers do Haskell
  • As linhas de efeitos são mescladas estruturalmente ao longo das chamadas
  • Elas se comportam como um conjunto de rótulos, não como uma pilha

Recursos expressos por um único mecanismo

• Exceções

  • Em Prism, exceções são handlers que descartam a continuation
  • Uma cláusula final ctl descarta k e usa o valor do corpo como resultado do handler
  • Não é uma abordagem de propagar Result nem de espalhar ? pela pilha de chamadas
  • Como exceções são rótulos na linha de efeitos, elas se compõem como exceções extensíveis
  • Cada falha é uma operação separada, e a linha no tipo da função indica quais exceções podem escapar
  • No exemplo com Abort e Timeout, fetch tem !{Abort, Timeout}
  • with_default trata apenas Timeout para retornar o fallback "cached"; após o tratamento, só resta !{Abort} no tipo
  • Diferentemente das checked exceptions do Java, elas não ficam presas a uma hierarquia de classes e funcionam como um conjunto estrutural aberto

• Geradores e streams

  • Um stream é composto por um produtor que executa emit, transformadores que capturam e reemitem, e um consumidor que faz fold
  • O pipeline tem a forma de handlers aninhados em torno de um produtor, então listas intermediárias não surgem estruturalmente
  • Exemplo: srange(1, n).smap(square).skeep(even).stake(5).ssum()
  • Interrupção antecipada, como stake(5), é um handler que descarta a continuation depois de obter os valores necessários
  • A biblioteca de streams foi influenciada por pipes e conduit, do Haskell

• Lentes

  • As lentes do Prism não são uma biblioteca separada, mas uma combinação de caminhos de atualização de registros com o modelo de memória
  • Em registros aninhados, uma única expressão de caminho pode atualizar vários campos profundos
  • Exemplo: { g | player.pos.x = 30, player.hp = 95, score = 110 }
  • A spine do registro aninhado é reconstruída, mas, quando o valor tem posse única, as células desmontadas são reutilizadas
  • Graças a essa estrutura, uma atualização funcional pode ser compilada para escritas de ponteiro
  • Nenhum tipo optic é alocado ou composto em runtime
  • deriving (Lens) gera acessores comuns como funções, como score_of e with_score

• Estado mutável

  • var é dessugarizado para operações get/set de um efeito privado
  • Um handler instalado no fim do bloco trata esse efeito
  • A análise de escape de closures rejeita casos em que o estado escapa para fora
  • A função envolvente pode manter uma linha de efeitos vazia

• Falha

  • Falhas são expressas por um efeito anônimo Fail, e o sistema de tipos lida com “esta expressão pode não produzir um valor”
  • fail() executa uma falha, e guard(cond) falha quando a condição é falsa
  • ?? usa um fallback quando o lado esquerdo falha
  • ?. percorre uma cadeia opcional e interrompe cedo
  • Um guard em comprehension poda elementos que falharam, em vez de causar crash
  • Como var também é açúcar sintático para handlers, um bloco transact pode tirar snapshots de variáveis live e fazer rollback em caso de falha

Recursos de tipos modernos

• Prism usa inferência de tipos bidirecional higher-rank da família Dunfield-Krishnaswami para que a maioria do código não precise de assinaturas de tipo explícitas
• Em fronteiras que exigem polimorfismo de ordem superior, os binders são explicitados com forall
  • pick(g : forall a. (a) -> a) pode aplicar g tanto a Bool quanto a Int
  • Em um núcleo Damas-Milner, a seria unificado com Bool na primeira chamada, e a segunda chamada seria rejeitada
• Polimorfismo ad hoc é expresso com type classes no estilo Lean
  • Instâncias são valores nomeados
  • given Ord(a) exige um dicionário
  • Quando há várias instâncias, uma é marcada como canonical, e as outras são explicitadas com using
• deriving gera instâncias repetitivas e acessores de campos para Eq, Ord, Show, Lens e similares
• Pattern matching também se conecta a classes
  • pattern First(n) for Peek = view peek é um padrão que usa um método de classe como view
  • head_or pode usar o mesmo padrão para vários tipos que tenham uma instância de Peek
• show funciona de modo orientado por tipo, sem uma classe separada
  • O compilador sintetiza um printer estrutural a partir do tipo estático
  • Ele não lê tags de tipo em runtime para decidir como imprimir
• Linhas de efeitos também são polimórficas
  • fn twice(f : (Unit) -> Int ! {| e}) soma os resultados independentemente de qual seja a linha de efeitos e da função recebida
  • Em um thunk puro, e é unificado com a linha vazia {}
  • Em um thunk que executa efeitos como Tick ou Say, a linha correspondente é encaminhada intacta

Estratégia de compilação para reduzir o custo dos efeitos

• Implementações didáticas de efeitos algébricos podem reconstruir a computação como uma árvore em forma de free monad e alocar pequenas células a cada operação
• O caminho rápido do Prism é o evidence passing da família Koka
  • Em vez de reconstruir a computação para encontrar handlers, as cláusulas de handlers ativas são passadas para cada ponto de operação como parâmetros comuns
  • do op é baixado para uma chamada direta
  • Como apenas uma closure é alocada ao instalar um handler, o custo é O(handlers) e não proporcional ao número de operações
• A codificação por free monad permanece como fallback
  • Computações que escapam para uma estrutura de dados
  • Resumption verdadeiramente multishot
  • Padrões como masked handler
• Pipelines de streams calculam, por análise de fluxo interprocedural, a evidence de efeito necessária além das fronteiras de funções
  • A evidence é encadeada por produtores e transformadores
  • A cadeia inteira é baixada para um único loop
  • Não há listas intermediárias nem alocação de célula por operação
• Essa abordagem obtém, em um compilador de efeitos, resultados semelhantes à stream fusion do Haskell ou à unificação de adapters de iterators do Rust

Modelo de memória e runtime

• Prism usa contagem de referências Perceus
  • Células de heap são liberadas deterministicamente em pontos conhecidos estaticamente
  • Não há pausas nem tracing
• A reutilização limitada ao frame passa células recém-desmontadas por pattern match de volta ao lado do construtor
  • Um map sobre uma lista com posse única parece uma função pura que retorna uma nova lista, mas na prática pode ser feito in-place
  • A compilação de atualizações por lentes para escritas de ponteiro usa o mesmo mecanismo
• A estrutura de runtime é semelhante à disciplina de memória do Lean 4, mas Prism emite LLVM IR
  • O LLVM IR é gerado via inkwell
  • Para o mesmo programa, também é gerado um módulo MLIR textual
  • O resultado é ligado com clang ao runtime em C escrito manualmente, prism_rt.c
• prism_rt.c é um runtime pequeno, com cerca de 2 mil linhas
  • Células de heap têm uma estrutura de 4 ou mais words no formato { refcount, tag, arity, fields... }
  • Inclui allocator, rc_inc/rc_dec, allocator de reutilização in-place e primitivos de bignum e strings
  • Não há collector thread, card table nem safepoint
• O allocator padrão é o malloc da libc, com uma configuração opt-in de mimalloc para benchmarking
• O live-cell oracle verifica a propriedade garbage-free da suíte de testes fazendo assert, ao final da execução, de que o balanço do heap é 0

Modelo em Lean e validação de backends

• O interpretador do Prism é da família de máquinas CEK, e essa máquina é refletida no modelo Lean 4 models/Prism.lean
• O modelo Lean 4 tem um teorema verificado mecanicamente de que a relação small-step é determinística
  • Um programa avança para exatamente um próximo estado
• O interpretador em Rust também é usado como oracle diferencial
  • Todos os programas do corpus passam pelo interpretador e pelos backends LLVM, MLIR e binário linkado com C
  • O build só passa se as saídas dos quatro forem byte-identical
• Determinismo é a base para execução durável reproduzível
  • A ideia é que, fixando entradas e registrando a execução, seja possível reproduzi-la bit-for-bit
  • Em versões futuras, imagina-se um Prism que verifique como propriedade de tipo a segurança de replay após crash

Playground WASM e código-fonte

• O mesmo interpretador é compilado para WASM e permite executar código Prism sem instalação no playground
• O playground executa programas em um worker
• Botões permitem despejar assinaturas de tipos inferidas, effect rows e o core IR baixado
  • É possível ver para qual forma loops com var ou pipelines de streams realmente são baixados
• Os exemplos do texto estão incluídos em um dropdown
• O código-fonte completo, o modelo Lean e o runtime em C estão no repositório do Prism no GitHub

Linhagem de implementação e natureza do projeto

• O core IR do Prism pertence à família call-by-push-value, baseada em Call-by-Push-Value: A Functional/Imperative Synthesis, de Levy
• O caminho rápido de efeitos é próximo de Generalized Evidence Passing for Effect Handlers e Effect Handlers, Evidently, de Xie e Leijen
• O modelo de memória se baseia em Perceus: Garbage Free Reference Counting with Reuse, Reference Counting with Frame-Limited Reuse e FP^2: Fully in-Place Functional Programming
• As linhas de efeitos seguem row polymorphism e scoped labels, e os handlers adotam, via Eff e Koka, a forma de Handlers of Algebraic Effects, de Plotkin e Pretnar
• O pattern matching é baseado em decision tree e usefulness matrix, e a forma pattern combina view patterns com Pattern Synonyms, do GHC
• A camada de falhas reaproveita The Verse Calculus como handlers final ctl
• A direção do Prism está mais próxima de tornar efeitos visíveis, tipá-los e rastreá-los de forma componível do que de “programação funcional pura”
• O projeto em si está mais próximo de um brinquedo e de uma obra artística do que de uma ferramenta prática, e é descrito como um compilador criado pela beleza intelectual das ideias de programação funcional

[GN⁺]

Comentários no Lobste.rs

• Não entendo o que lentes têm a ver com efeitos. Toda vez que o texto menciona lentes, elas parecem não ter relação entre si, exceto por estarem agrupadas sob “um truque de cinco maneiras”
  E também não faço ideia do que tick_use() está tentando fazer. Esperam que o leitor entenda um exemplo tão enrolado sem explicação? Anotações de tipo teriam ajudado

  • Há mais explicações sobre lentes aqui: https://sdiehl.github.io/prism/spec.html#86-optic-paths
    Mesmo assim, fora o nível metafórico, ainda não vejo bem o que lentes têm a ver com efeitos. O autor escreve:

    This is the language’s “effects instead of monads” stance applied to optics, paths instead of optic combinators.
    Ou seja, entendo a metáfora assim: mônadas são valores, mas efeitos não são valores; são uma espécie de estrutura de controle. Da mesma forma, lentes são valores, mas os optic paths do Prism não são valores; estão mais para estruturas de controle com sintaxe hardcoded

• Vou precisar dedicar mais tempo para entender, mas parece realmente bonito

• Realmente impressionante. Justamente por isso fico curioso por que Diehl chama o compilador de brinquedo no fim do texto. Parece uma prova de conceito bem-sucedida que mostra um novo nível de elegância

• Gostaria de ver em mais detalhes como a representação intermediária call-by-push-value realmente é. Tenho curiosidade especialmente sobre como ela lida com pontos de junção (join points)
  Já houve artigos tratando da teoria de acrescentar efeitos ao CBPV. Dizer que computações têm tipos de efeito e valores não têm parece bem natural, mas eu não tinha visto isso concretizado o bastante para ser aplicado diretamente à passagem de evidências do Koka, então é interessante
  No geral, queria entender onde isso se posiciona em comparação ao Koka. Olhando para FBIP, Perceus e passagem de evidências, é claro que há forte inspiração no trabalho do Koka e, ao mesmo tempo, o uso de CBPV como representação intermediária também o torna claramente diferente. Só não fica muito visível o quanto é diferente

• Parece muito com algo que eu venho tentando arrumar tempo para construir. Gostei!

• Fugindo um pouco do tema, sempre achei meio triste que o projeto “write you a haskell” do Stephen tenha parado alguns anos atrás. Para o Prism, seria ótimo ter uma explicação de implementação em nível de tutorial

• Fico curioso sobre o que é “impuro” nesta linguagem. Essa palavra aparece só no título e não volta no corpo do texto
  Como todos os efeitos parecem ser rastreados, funções sem efeitos continuam sendo funções matemáticas. Estou deixando algo passar?

  • Parece ter a ver com o uso de variáveis locais mutáveis dentro da definição de funções, como na definição de fib mostrada. var x é uma variável mutável impura, enquanto let x é uma variável imutável pura

• É muito legal que coisas que normalmente eram tratadas como recursos da linguagem, como o yield da linguagem X ou o throw da linguagem Y, tenham sido implementadas como mais uma interface
  Poder construir vários fluxos de controle, como efeitos colaterais, exceções e continuações, sobre uma única abstração é uma forma interessante de enxergar de outro jeito todo o conjunto de perguntas de design, e espero que isso ajude ou estimule mais exploração e inovação. Acho que vou voltar a isso por muitos anos para buscar inspiração