
 
 
 
 
 
 Os autores: (1) David Binder, Universidade de Tübingen, Alemanha; (2) Marco Tzschentke, Universidade de Tübingen, Alemanha; (3) Marius Muller, Universidade de Tübingen, Alemanha; (4) Klaus Ostermann, Universidade de Tübingen, Alemanha. Authors: (1) David Binder, Universidade de Tübingen, Alemanha; (2) Marco Tzschentke, Universidade de Tübingen, Alemanha; (3) Marius Muller, Universidade de Tübingen, Alemanha; (4) Klaus Ostermann, Universidade de Tübingen, Alemanha. Mesa da Esquerda 
 
 
 
 
 
 
 
 
 
 Introduction 
 
 
 
 
 
 
 
 Translating To Sequent Calculus 2.1 Arithmetic Expressions 2.2 Let Bindings 2.3 Top-level Definitions 2.4 Algebraic Data and Codata Types 2.5 First-Class Functions 2.6 Control Operators 
 
 
 
 Evaluation Within a Context 3.1 Evaluation Contexts for Fun 3.2 Focusing on Evaluation in Core 
 
 
 
 
 Typing Rules 4.1 Typing Rules for Fun 4.2 Typing Rules for Core 4.3 Type Soundness 
 
 
 
 
 
 
 
 
 Insights 5.1 Evaluation Contexts are First Class 5.2 Data is Dual to Codata 5.3 Let-Bindings are Dual to Control Operators 5.4 The Case-of-Case Transformation 5.5 Direct and Indirect Consumers 5.6 Call-By-Value, Call-By-Name and Eta-Laws 5.7 Linear Logic and the Duality of Exceptions 
 
 Related Work 
 
 Conclusion, Data Availability Statement, and Acknowledgments Introdução Tipo Regras Trabalho relacionado Conclusão, declaração de disponibilidade de dados e reconhecimentos A. A relação com o cálculo seqüencial B. Escrever regras para diversão C. Semântica operacional do rótulo/goto Referências 1 Introdução Suponha que você acabou de implementar sua própria linguagem funcional pequena. Para testá-lo, você escreve a seguinte função que multiplica todos os números contidos em uma lista: O que o incomoda sobre esta implementação é que você conhece uma óbvia otimização: a função deve retornar diretamente zero se encontrar um zero na lista. Há muitas maneiras de conseguir isso, mas você escolhe estender seu idioma com expressões rotuladas e uma instrução goto. Isso permite que você escreva a versão otimizada: def mult(l)  label α { mult’(l; α) } Porém, o que é mais importante é que você tenha que se preocupar com o que está acontecendo. Aqui está como você lê este trecho: Além do argumento de lista l, a definição def mult(l; α)  . . . toma um argumento α que indica como o cálculo deve continuar uma vez que o resultado da multiplicação é computado (nós novamente usamos; para separar esses dois tipos de argumentos). A função de auxílio mult’ toma um argumento de lista l e dois argumentos α e β; o argumento β indica onde a função deve retornar em uma chamada recursiva normal, enquanto α indica o ponto de retorno de uma computação de curto-circuito. No corpo de mult’ usamos o caso l. {Nil ⇒ . . . , Cons(x, xs) ⇒ . . .} talvez execute um caso de divisão na lista l. Se a lista é Nilo, então usamos O λμμ-calculus que você acabou de ver foi introduzido pela primeira vez por Curien e Herbelin [2000] como uma solução para uma pergunta aberta de longa data: Como deveria parecer uma linguagem de termo para o cálculo seqüencial? O cálculo seqüencial é um dos dois cálculos de prova influentes introduzidos por Gentzen [1935a,b] em um único artigo, o outro cálculo sendo dedução natural. O termo linguagem para dedução natural é o cálculo lambda comum, mas foi difícil encontrar uma boa linguagem de termo para o cálculo seqüencial. Depois de ter sido encontrado, o λμμ-calculus foi proposto como uma melhor base para linguagens intermediárias compiladoras, por exemplo por Downen et al. [2016]. Apesar disso, a maioria dos escritores de linguagem de design e comp Frequentemente discutimos ideias que envolvem o cálculo λμμ com estudantes e colegas e, portanto, temos que apresentá-las às suas idéias centrais. Mas geralmente não podemos motivar o cálculo λμμ como um sistema de atribuição de termos para o cálculo seqüencial, uma vez que a maioria deles não está familiarizada com ele. Em vez disso, explicamos o cálculo λμμ no tabuleiro compilando pequenos programas funcionais nele. Uma tal introdução é, infelizmente, ainda ausente na literatura publicada; a maioria das apresentações existentes pressupõe conhecimento do cálculo seqüencial ou, de outra forma, gasta muito espaço introduzindo-o primeiro. Acreditamos que se alguém pode entender o cálculo lambda sem primeiro aprender sobre provas de dedução natural, então também deve ser capaz de entender o cálculo λμμ sem conhecer o cál Por que estamos entusiasmados com o cálculo λμμ ̃, e por que pensamos que mais pessoas devem se familiarizar com suas idéias e conceitos centrais? A principal característica que distingue o cálculo λμμ ̃ do cálculo lambda é o seu tratamento de primeira classe de contextos de avaliação. Um contexto de avaliação é o restante do programa que corre após a subexpressão atual que estamos focados em avaliar os acabamentos. Isto torna-se mais claro com um exemplo: Quando queremos avaliar a expressão (2 + 3) ∗ 5, primeiro temos que nos concentrar na sub-expressão 2 + 3 e avaliá-la para o seu resultado 5. O resto do programa, que será executado depois de termos concluído a avaliação, pode ser representado com o contexto de avaliação □ ∗ 5. Não podemos vincular um contexto de avaliação como □ ∗ 5 a uma variável no tipo de cálculo lambda, mas no λμμ ̃-calculus podemos vincular tais contextos de avaliação a covariáveis. Além disso, o μ-operador dá acesso direto ao contexto de avaliação no qual a expressão é atualmente avaliada. Ter esse acesso direto ao contexto de avaliação não é sempre necessário para um programador que deseja escrever uma aplicação, mas é frequentemente importante para O restante do documento está estruturado da seguinte forma: • Na Seção 2 apresentamos a linguagem de superfície Fun e mostramos como podemos traduzir-la para o Core da linguagem baseada em cálculo sequencial. A linguagem de superfície é principalmente uma linguagem de programação funcional orientada para expressão, mas adicionamos algumas características como tipos de codata e operadores de controle cujas traduções fornecem insights importantes sobre como o λμμ ̃-calculus funciona. • Na Seção 3 discutimos foco estático e dinâmico, que são duas técnicas estreitamente relacionadas para elevar subexpressões que não são valores em uma posição onde eles podem ser avaliados. • A Seção 4 introduz as regras de digitação para Fun e Core e demonstra resultados padrão sobre digitação e avaliação. Mostramos por que estamos entusiasmados com o λμμ ̃-calculus na Seção 5.Apresentamos vários conceitos de linguagem de programação que se tornam muito mais claros quando os apresentamos no λμμ ̃-calculus: Mostramos que os let-bindings são exatamente duplos para controlar operadores, que os tipos de dados e codata são duas maneiras perfeitamente duplas de especificar tipos, e que a transformação caso-de-caso é nada mais do que uma μ-redução. • Finalmente, na Seção 6 discutimos o trabalho relacionado e fornecemos pistas para leitura mais aprofundada. Este artigo é acompanhado por uma implementação Haskell que também disponibilizamos como um site interativo (cf. Figura 1). 
 
 Este artigo está disponível em arquivo sob a licença CC BY 4.0. Este artigo está disponível em arquivo sob a licença CC BY 4.0. Disponível em Arquivo [1] Para o leitor interessado, mostramos no Apêndice A como o cálculo seqüencial e o cálculo λμμ ̃ estão conectados.

Part of HackerNoon's growing list of open-source research papers, promoting free access to academic material.

Read My Stories

Abstraction

Este áudio é produzido no idioma original da história!

E se as linguagens de programação pudessem pensar adiante?

About Author

COMENTARIOS

Rótulos

ESTE ARTIGO FOI APRESENTADO EM

Related Stories

Criando produtos criptográficos centrados no usuário: a importância do feedback do cliente

Guia do arquiteto para construir arquitetura de referência para um Datalake de IA/ML

Navegando pelas águas: desenvolvendo aplicações RAG de nível de produção com data lakes

Toque para ganhar: Telegram pode integrar os próximos 10 bilhões de usuários criptográficos antes de Solana

Criando produtos criptográficos centrados no usuário: a importância do feedback do cliente

Guia do arquiteto para construir arquitetura de referência para um Datalake de IA/ML

Navegando pelas águas: desenvolvendo aplicações RAG de nível de produção com data lakes

Toque para ganhar: Telegram pode integrar os próximos 10 bilhões de usuários criptográficos antes de Solana

Light-Mode

Classic

Newspaper

Minty

Dark-Mode

Neon Noir

Minty

HN StartUps