Y Combinator em Haskell

Question

É possível escrever o Y Combinator em Haskell?

Parece que ele teria um infinitamente recursiva tipo.

 Y :: f -> b -> c
 where f :: (f -> b -> c)

ou algo assim.Até mesmo um simples ligeiramente fatorado factorial

factMaker _ 0 = 1
factMaker fn n = n * ((fn fn) (n -1)

{- to be called as
(factMaker factMaker) 5
-}

falha com "Ocorre de seleção:não é possível construir o infinito do tipo:t = t -> t2> t1"

(O Y combinator parece com isso

(define Y
    (lambda (X)
      ((lambda (procedure)
         (X (lambda (arg) ((procedure procedure) arg))))
       (lambda (procedure)
         (X (lambda (arg) ((procedure procedure) arg)))))))

no esquema) Ou, mais sucintamente, como

(λ (f) ((λ (x) (f (λ (a) ((x x) a))))
        (λ (x) (f (λ (a) ((x x) a))))))

Para o aplicativo, a fim E

(λ (f) ((λ (x) (f (x x)))
        (λ (x) (f (x x)))))

Que é apenas uma eta contração de distância para os mais preguiçosos versão.

Se você preferir curto nomes de variáveis.

Answer 1

Oh

esta página wiki e Esta Sobrecarga de Pilha resposta parecem responder a minha pergunta.
Vou escrever mais de uma explicação posterior.

Agora, eu descobri algo interessante sobre o que o Mu tipo.Considere S = Mu Bool.

data S = S (S -> Bool)

Se trata-se S como um conjunto e que o sinal de igual como isomorfismo, em seguida, a equação torna-se

S ⇋ S -> Bool ⇋ Powerset(S)

Então S é o conjunto dos conjuntos que são isomórficas às suas powerset!Mas sabemos que a partir do Cantor diagonal argumento de que a cardinalidade de a Powerset(S) é sempre estritamente maior que a cardinalidade de S, para que eles nunca são isomórficas.Eu acho que é por isso que agora você pode definir um ponto fixo do operador, mesmo que você não pode sem um.

Answer 2

Aqui está um não-recursiva definição do y combinator em haskell:

newtype Mu a = Mu (Mu a -> a)
y f = (\h -> h $ Mu h) (\x -> f . (\(Mu g) -> g) x $ x)

chapéu de ponta

Answer 3

A Y combinator não pode ser digitada usando Hindley-Milner tipos, polimórfico cálculo lambda no qual Haskell tipo de sistema é baseado.Você pode provar isso por apelar para as regras do tipo de sistema.

Eu não sei se é possível digitar o Y combinator, dando-lhe uma maior classificação do tipo.Ele seria surpresa para mim, mas eu não tenho uma prova de que não é possível.(A chave seria identificar adequadamente um tipo polimórfico para o lambda-vinculado x.)

Se você quer um ponto fixo do operador no Entanto, você pode definir um muito facilmente, porque em Haskell, deixe-associação possui ponto fixo semântica:

fix :: (a -> a) -> a
fix f = f (fix f)

Você pode usar isso em a maneira usual de se definir funções e até mesmo alguns finito ou infinito de estruturas de dados.

Também é possível usar funções recursivas tipos de implementar pontos fixos.

Se você estiver interessado em programação com pontos fixos, quer ler Bruce McAdam do relatório técnico O que Sobre termina-lo.

Answer 4

A definição canônica da Y combinator é como segue:

y = \f -> (\x -> f (x x)) (\x -> f (x x))

Mas não é o tipo de verificação no Haskell, devido a x x, pois exigiria um infinito tipo:

x :: a -> b -- x is a function
x :: a      -- x is applied to x
--------------------------------
a = a -> b  -- infinite type

Se o tipo de sistema para permitir que eram tais recursiva tipos, faria com que a verificação de tipo indecidíveis (sujeito a ciclos infinitos).

Mas o Y combinator irá funcionar se você forçá-lo para tipo verificação, por exemplo,usando unsafeCoerce :: a -> b:

import Unsafe.Coerce

y :: (a -> a) -> a
y = \f -> (\x -> f (unsafeCoerce x x)) (\x -> f (unsafeCoerce x x))

main = putStrLn $ y ("circular reasoning works because " ++)

Este é inseguro (obviamente). rampion resposta demonstra uma maneira mais segura para escrever um ponto fixo combinator em Haskell sem usar recursão.