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

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?

Primeiro, vamos ser explícitos sobre como seqdistingue de λ x . ⊥ :$\bot$$\lambda x . \bot$

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 . $\bot$$\lambda x . \bot$seqseqseq$\lambda$seq$\bot$$\lambda x . \bot$ 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$\lambda$$[D \to E]$$\bot = \lambda x . \bot$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 . $\lambda$seq$\bot$$\lambda x . \bot$$\eta$$[D \to E]_\bot$$\bot$$[D \to E]_\bot$$\lambda x . \bot$ é 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.$\bot$seq

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

$\lambda x.\, \bot$$\lambda x.\, \bot$ , 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.

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).