A eta-equivalência para funções é compatível com a operação seq de Haskell?

14

Lema: Assumindo a eta-equivalência, temos isso (\x -> ⊥) = ⊥ :: A -> B.

Prova: ⊥ = (\x -> ⊥ x)por eta-equivalência e (\x -> ⊥ x) = (\x -> ⊥)por redução no lambda.

O relatório Haskell 2010, seção 6.2 especifica a seqfunção por duas equações:

seq :: a -> b -> b
seq ⊥ b = ⊥
seq ab = b, se a ≠ ⊥

Ele então afirma "Como conseqüência, ⊥ não é o mesmo que \ x -> ⊥, pois seq pode ser usado para distingui-los."

Minha pergunta é: isso é realmente uma consequência da definição de seq?

O argumento implícito parece ser que seqseria incontestável se seq (\x -> ⊥) b = ⊥. No entanto, não consegui provar que isso seqseria incontestável. Parece-me que tal seqé monótono e contínuo, o que o coloca no domínio de ser computável.

Um algoritmo que implementa como seq pode funcionar tentando procurar por algum xlocal f x ≠ ⊥, enumerando o domínio def começar com ⊥. Embora essa implementação, mesmo que seja possível, fique bastante complicada quando queremos fazer seqpolimórficos.

Existe uma prova de que não há computável seqque identifica (\x -> ⊥)com ⊥ :: A -> B? Como alternativa, há alguma construção do seqque se identifica (\x -> ⊥)com ⊥ :: A -> B?

Russell O'Connor
fonte

Respostas:

6

Primeiro, vamos ser explícitos sobre como seqdistingue de λ x . :λx.

bottom :: a
bottom = bottom

eta :: a -> b
eta x = bottom

-- This terminates
fortytwo = seq eta 42

-- This does not terminate
infinity = seq bottom 42

Portanto, é um fato experimental que em Haskell e λ x . são operacionalmente distinguíveis. Também é um fato, e bastante óbvio, que é computável porque Haskell o computa. Muito sobre Haskell. Você está perguntando sobre o fraseado muito particular da documentação de Haskell. Eu li como dizendo que deveria satisfazer as duas equações dadas, mas essas duas equações não são suficientes para a definição de . Aqui está o porquê: Eu posso lhe dar dois modelos de ( -digitalamente digitado) λ- cálculo em que é computável e satisfaz as equações dadas, mas em um dos modelos e λ x . λx.seqseqseqλseqλx. concorda, enquanto no outro eles não.

Em um modelo teórico de domínio simples, em que as expressões são interpretadas no domínio de funções contínuas [ D E ] , temos = λ x . Obviously obviamente. Tome domínios Scott eficazes ou algo parecido para tornar tudo computável. É fácil definirλ[DE]=λx.seq nesse modelo.

Também podemos ter um modelo de cálculo no qual distingue e λ x . e, é claro, a regra η não pode ser mantida. Por exemplo, podemos fazer isso interpretando funções no domínio [ D E ] , ou seja, o domínio do espaço de funções com um fundo extra anexado. Agora é, bem, o fundo de [ D E ] , enquanto λ x . λseqλx.η[DE][DE]λx. é o elemento logo acima dele. Eles não podem ser distinguidos por aplicação, porque ambos avaliam , não importa em que você os aplique (eles sãoextensionalmente iguais). Mas temoscomo um mapa entre domínios e ele sempre distingue o fundo de todos os outros elementos.seq

Andrej Bauer
fonte
1
É um fato experimental que em GHC e / ou abraços ⊥ e λx.⊥. Felizmente, Haskell não é definido por uma implementação. Minha pergunta está sugerindo que Haskell está subespecificado no que diz respeito à seq.
Russell O'Connor
Você pode dar uma referência ao que você quer dizer com "domínios Scott efetivos" Presumivelmente, isso não implica que a ordem parcial seja decidível. Além disso, o STLC não é polimórfico, mas Haskell é. Geralmente, Haskell é interpretado no Sistema F ou em um de seus derivados. Como isso afeta seu argumento?
Russell O'Connor
Seção 1.1.4 do meu Ph.D. dissertation andrej.com/thesis/thesis.pdf tem uma definição curta de domínios Scott eficazes, e esse é realmente o primeiro hit do Google disponível gratuitamente.
Andrej Bauer
2
Se você escrever uma prova para mim, obterá uma implementação do Haskell 98, onde a regra-eta mantém permitindo que (foldr (\ ab -> fab) z xs) seja otimizada para (foldr fz xs) causando um aumento de desempenho assintótico de O (n ^ 2) a O (n) (consulte ghc.haskell.org/trac/ghc/ticket/7436 ). Mais atraente, permitirá que um NewTypeWrapper em (NewTypeWrapper. F) seja otimizado sem forçar a expansão de eta e evite algumas penalidades de desempenho assintóticas atualmente impostas por newTypes no GHC (no uso de foldr, por exemplo).
Russell O'Connor
1
Na verdade, você teria que garantir que seu compilador sempre implemente como . Ou seja, você pode ficar tentado a nem sempre contrair e, portanto, em princípio λ x . e seriam "algumas vezes distinguíveis", uma situação muito perigosa. Para garantir que esse não seja o caso, você precisa implementar de maneira inteligente, o que envolve gerar infinitos processos, cada um aplicando sua função a um elemento básico. Se algum dos processos terminar, poderá prosseguir. Seria interessante ver se podemos fazer isso sequencialmente. Hmm. λx.λx.seqseq
Andrej Bauer
2

Observe que a especificação para a seqqual você cita não é sua definição. Para citar o relatório Haskell "A função seq é definida pelas equações : [e depois pelas equações que você fornecer]".

O argumento sugerido parece ser que seq seria indiscutível se seq (\ x -> ⊥) b = ⊥.

Esse comportamento violaria a especificação de seq.

É importante ressaltar que, uma vez que seqé polimórfico, seqnão pode ser definido em termos de desconstrutores (projeções / correspondência de padrões etc.) em um dos dois parâmetros.

Existe uma prova de que não há seq computável que identifique (\ x -> ⊥) com ⊥ :: A -> B?

Se seq' (\x -> ⊥) b, poder-se-ia pensar que poderíamos aplicar o primeiro parâmetro (que é uma função) a algum valor e depois sair. Mas, seqnunca é possível identificar o primeiro parâmetro com um valor de função (mesmo que seja um para algum uso seq) devido ao seu tipo polimórfico paramétrico. Parametricidade significa que não sabemos nada sobre os parâmetros. Além disso, seqnunca pode tomar uma expressão e decidir "é este ⊥?" (cf. o problema da parada), seqpode apenas tentar avaliá-lo, e ele próprio diverge para ⊥.

O que seqfaz é avaliar o primeiro parâmetro (não totalmente, mas a "forma de cabeça fraca normal" [1], ou seja, ao mais alto construtor), em seguida, retornar o segundo parâmetro. Se o primeiro parâmetro for (ou seja, um cálculo não-terminativo), avaliá-lo faz seqcom que não termine e, portanto,seq ⊥ a = ⊥ ,.

[1] Teoremas livres na presença de seq - Johann, Voigtlander http://www.iai.uni-bonn.de/~jv/p76-voigtlaender.pdf

Dorchard
fonte
A especificação que forneço para seq é a definição de seq, porque é exatamente isso que o relatório Haskell 2010 diz na Seção 6.2. Sua definição de operação de seq não é suportada pelo relatório Haskell 2010: as palavras "formulário normal da cabeça" ocorrem apenas uma vez no relatório em um contexto totalmente diferente. Também é inconsistente com meu entendimento que o GHC frequentemente reduza o segundo argumento para seq antes do primeiro argumento, ou o primeiro argumento não será reduzido porque o analisador de rigidez provou que não é estaticamente inferior.
Russell O'Connor
A parametridade não diz diretamente que não podemos aplicar nenhum desconstrutor, nem diz que nunca podemos identificar o primeiro parâmetro com um valor de função. Tudo o que a parametridade diz para o cálculo lambda polimórfico com pontos de correção é que seq pode absorver funções estritas ou, geralmente, certas relações estritas mantidas para termos contêm seq. Admito que é plausível que a parametridade possa ser usada para provar (\ x -> ⊥) & ne; ⊥, mas gostaria de ver uma prova rigorosa.
Russell O'Connor
No caso de uma função f : forall a . a -> T(onde Testá outro tipo), fnão é possível aplicar nenhum desconstrutor ao seu primeiro argumento, pois ele não sabe quais desconstrutores aplicar. Não podemos fazer um "caso" em tipos. Eu tentei melhorar a resposta acima (inclusive citando informações sobre como seqavaliar a forma normal da cabeça).
dorchard
Posso tentar fazer a prova rigorosa mais tarde, se encontrar tempo (usar relações no estilo de Reynolds pode ser uma boa abordagem).
dorchard
@ RussellO'Connor: a descrição de seq não é "inconsistente" com esses comportamentos, é apenas uma especificação operacional (e comportamentos são otimizações que não alteram o resultado final).
Blaisorblade 24/03
2

λx.λx. , a avaliação termina. A observação "Como conseqüência ..." no relatório Haskell pressupõe que o leitor saiba disso.

Samson Abramsky considerou esta questão há muito tempo e escreveu um artigo chamado " The Lazy Lambda Calculus ". Portanto, se você deseja definições formais, é aqui que deve procurar.

Uday Reddy
fonte
1
Aparentemente, esses detalhes são definidos apenas pelo desugar no "kernel Haskell". Onde está definido? O relatório diz, na Sec. 1.2 : "Embora o kernel não seja formalmente especificado, é essencialmente uma variante levemente adocicada do cálculo lambda com uma semântica denotacional direta. A tradução de cada estrutura sintática no kernel é fornecida conforme a sintaxe é introduzida."
Blaisorblade 24/03
O relatório Haskell 2010 diz o mesmo , surpreendentemente.
Blaisorblade 24/03
Obrigado pela referência a Abramsky! I desnatado-lo para ver como ele responde à pergunta, e eu vim com a seguinte resposta: cstheory.stackexchange.com/a/21732/989
Blaisorblade
2

Provando que λ x. Ω ‌ ≠ Ω in é um dos objetivos que Abramsky estabelece para sua teoria do cálculo preguiçoso de lambda (página 2 de seu trabalho , já citado por Uday Reddy), porque ambos estão em forma normal de cabeça fraca. Na definição 2.7, ele discute explicitamente que eta-redução λ x. M x → M geralmente não é válido, mas é possível se M terminar em todos os ambientes. Isso não significa que M deve ser uma função total - apenas que a avaliação de M deve terminar (reduzindo para um lambda, por exemplo).

Sua pergunta parece ser motivada por preocupações práticas (desempenho). No entanto, embora o Relatório Haskell possa ser menos que completamente claro, duvido que seja igual a λ x. ‌Com ⊥ produziria uma implementação útil de Haskell; se implementa Haskell '98 ou não, é discutível, mas, dada a observação, fica claro que os autores pretendiam que fosse esse o caso.

Finalmente, como seq gerar elementos para um tipo de entrada arbitrário? (Eu sei que o QuickCheck define a classe arbitrária para isso, mas você não tem permissão para adicionar essas restrições aqui). Isso viola a parametridade.

Atualizado : não consegui codificar isso direito (porque não sou tão fluente em Haskel) e corrigir isso parece exigir runSTregiões aninhadas . Tentei usar uma única célula de referência (na mônada do ST) para salvar esses elementos arbitrários, lê-los mais tarde e disponibilizá-los universalmente. A parametridade prova que break_parametricityabaixo não pode ser definido (exceto retornando a parte inferior, por exemplo, um erro), enquanto pode recuperar os elementos que a seq proposta geraria.

import Control.Monad.ST
import Data.STRef
import Data.Maybe

produce_maybe_a :: Maybe a
produce_maybe_a = runST $ do { cell <- newSTRef Nothing; (\x -> writeSTRef cell (Just x) >> return x) `seq` (readSTRef cell) }

break_parametricity :: a
break_parametricity = fromJust produce_maybe_a

Devo admitir que estou um pouco confuso em formalizar a prova de parametridade necessária aqui, mas esse uso informal da parametridade é padrão em Haskell; mas aprendi com os escritos de Derek Dreyer que a teoria necessária está sendo rapidamente elaborada nos últimos anos.

Editar% s:

  • Eu nem tenho certeza se você precisa dessas extensões, que são estudadas para linguagens semelhantes a ML, imperativas e não tipadas, ou se as teorias clássicas da parametridade cobrem Haskell.
  • Além disso, mencionei Derek Dreyer simplesmente porque só depois me deparei com o trabalho de Uday Reddy - eu aprendi sobre isso recentemente em "A essência de Reynolds". (Só comecei a ler realmente literatura sobre parametridade no último mês).
Blaisorblade
fonte
A avaliação (\x -> writeSTRef cell (Just x) >> return x)de entradas aleatórias não executa uma gravação na célula. Somente os comandos ST que fazem parte do passado sequenciado runSTsão executados. Da mesma forma, a execução main = (putStrLn "Hello") `seq` (return ())não imprime nada no visor.
Russell O'Connor
@ RussellO'Connor, é claro que você está certo - o teste é difícil, já que o seq não tem o comportamento que discutimos. Mas ainda acho que a geração de elementos quebra a parametridade em si. Vou tentar corrigir a resposta para exemplificar isso.
Bluesorblade 07/04
Hum, a correção óbvia para a resposta requer o aninhamento de regiões runST e o uso da célula da região externa na interna, mas isso não é permitido.
Bluesorblade 07/04