Ao explicar o combinador Y no contexto de Haskell, geralmente é observado que a implementação direta não verifica o tipo no Haskell devido ao seu tipo recursivo.
Por exemplo, do Rosettacode :
The obvious definition of the Y combinator in Haskell canot be used
because it contains an infinite recursive type (a = a -> b). Defining
a data type (Mu) allows this recursion to be broken.
newtype Mu a = Roll { unroll :: Mu a -> a }
fix :: (a -> a) -> a
fix = \f -> (\x -> f (unroll x x)) $ Roll (\x -> f (unroll x x))
E, de fato, a definição "óbvia" não digita check:
λ> let fix f g = (\x -> \a -> f (x x) a) (\x -> \a -> f (x x) a) g
<interactive>:10:33:
Occurs check: cannot construct the infinite type:
t2 = t2 -> t0 -> t1
Expected type: t2 -> t0 -> t1
Actual type: (t2 -> t0 -> t1) -> t0 -> t1
In the first argument of `x', namely `x'
In the first argument of `f', namely `(x x)'
In the expression: f (x x) a
<interactive>:10:57:
Occurs check: cannot construct the infinite type:
t2 = t2 -> t0 -> t1
In the first argument of `x', namely `x'
In the first argument of `f', namely `(x x)'
In the expression: f (x x) a
(0.01 secs, 1033328 bytes)
A mesma limitação existe em Ocaml:
utop # let fix f g = (fun x a -> f (x x) a) (fun x a -> f (x x) a) g;;
Error: This expression has type 'a -> 'b but an expression was expected of type 'a
The type variable 'a occurs inside 'a -> 'b
No entanto, no Ocaml, é possível permitir tipos recursivos passando no -rectypes
comutador:
-rectypes
Allow arbitrary recursive types during type-checking. By default, only recursive
types where the recursion goes through an object type are supported.
Ao usar -rectypes
, tudo funciona:
utop # let fix f g = (fun x a -> f (x x) a) (fun x a -> f (x x) a) g;;
val fix : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>
utop # let fact_improver partial n = if n = 0 then 1 else n*partial (n-1);;
val fact_improver : (int -> int) -> int -> int = <fun>
utop # (fix fact_improver) 5;;
- : int = 120
Sendo curioso sobre sistemas de tipos e inferência de tipos, isso levanta algumas questões que ainda não sou capaz de responder.
- Primeiro, como o verificador de tipos cria o tipo
t2 = t2 -> t0 -> t1
? Tendo inventado esse tipo, acho que o problema é que o type (t2
) se refere a si mesmo no lado direito? - Segundo, e talvez o mais interessante, qual o motivo dos sistemas do tipo Haskell / Ocaml não permitirem isso? Eu acho que não é uma boa razão desde Ocaml também não vai permitir isso por padrão, mesmo se ele pode lidar com tipos recursiva se dado a
-rectypes
chave.
Se esses são realmente grandes tópicos, eu gostaria de sugestões para literatura relevante.
No OCaml, você precisa passar
-rectypes
como parâmetro para o compilador (ou inserir#rectypes;;
no nível superior). Grosso modo, isso desativará "ocorre verificação" durante a unificação. A situaçãoThe type variable 'a occurs inside 'a -> 'b
não será mais um problema. O sistema de tipos ainda estará "correto" (som etc.), as infinitas árvores que surgem como tipos são às vezes chamadas de "árvores racionais". O sistema de tipos fica mais fraco, ou seja, torna-se impossível detectar alguns erros do programador.Veja minha palestra sobre lambda-calculus (começando no slide 27) para obter mais informações sobre operadores de fixpoint com exemplos no OCaml.
fonte