Y Combinator, tipos infinitos y recursión anónima en Haskell

Question

Estaba tratando de resolver el Problema de suma máxima de la subsecuencia y se le ocurrieron una solución de Neato

msss :: (Ord a, Num a) => [a] -> a
msss = f 0 0

f gmax _ [] = gmax
f gmax lmax (x:xs) = 
  let g = max (lmax + x)
  in  f (g gmax) (g 0) xs

Llamas a la función de envoltura msss, que entonces llama f, que a su vez realmente hace el trabajo. La solución es buena y Afaik funciona correctamente. Si por alguna razón tuviera que resolver el problema de suma de posterior máxima en el código de producción, así es como lo haría.

Sin embargo, esa función de envoltura realmente me molesta. Me encanta cómo en Haskell, si eres lo suficientemente persistente, puedes escribir todo tu programa en una sola línea, para conducir realmente a casa el punto de que un programa es solo una gran expresión. Así que pensé que intentaría eliminar la función de envoltura para el desafío adicional.

Ahora me encuentro con el problema clásico: ¿cómo hacer una recursión anónima? ¿Cómo se recurre cuando no puede dar nombres a las funciones? Afortunadamente, los Padres de la Computación resolvieron este problema hace años descubriendo Combinadores de punto fijo, con el más popular siendo el Y Combinador.

He hecho varios intentos para configurar un combinador Y, pero no pueden superar el compilador.

msss' :: [Int] -> Int
msss' = (\y f x -> f (y y f) x) 
        (\y f x -> f (y y f) x) 
        (\g' gmax lmax list -> if list == [] 
                               then gmax 
                               else g' (max gmax lmax + head list) 
                                       (max 0    lmax + head list) 
                                       tail list)

Solo cede

Prelude> :l C:\maxsubseq.hs
[1 of 1] Compiling Main             ( C:\maxsubseq.hs, interpreted )

C:\maxsubseq.hs:10:29:
    Occurs check: cannot construct the infinite type:
      t0 = t0 -> (([Int] -> Int) -> [Int] -> Int) -> [Int] -> Int
    In the first argument of `y', namely `y'
    In the first argument of `f', namely `(y y f)'
    In the expression: f (y y f) x

C:\maxsubseq.hs:11:29:
    Occurs check: cannot construct the infinite type:
      t0 = t0 -> (([Int] -> Int) -> [Int] -> Int) -> [Int] -> Int
    In the first argument of `y', namely `y'
    In the first argument of `f', namely `(y y f)'
    In the expression: f (y y f) x

C:\maxsubseq.hs:12:14:
    The lambda expression `\ g' gmax lmax list -> ...'
    has four arguments,
    but its type `([Int] -> Int) -> [Int] -> Int' has only two
    In the second argument of `\ y f x -> f (y y f) x', namely
      `(\ g' gmax lmax list
          -> if list == [] then
                 gmax
             else
                 g' (max gmax lmax + head list) (max 0 lmax + head list) tail list)'
    In the expression:
      (\ y f x -> f (y y f) x)
        (\ y f x -> f (y y f) x)
        (\ g' gmax lmax list
           -> if list == [] then
                  gmax
              else
                  g' (max gmax lmax + head list) (max 0 lmax + head list) tail list)
    In an equation for `msss'':
        msss'
          = (\ y f x -> f (y y f) x)
              (\ y f x -> f (y y f) x)
              (\ g' gmax lmax list
                 -> if list == [] then
                        gmax
                    else
                        g' (max gmax lmax + head list) (max 0 lmax + head list) tail list)
Failed, modules loaded: none.

Cambiar de f (y y f) a f (y f) Solo cede

C:\maxsubseq.hs:11:29:
    Couldn't match expected type `[Int] -> Int'
                with actual type `[Int]'
    Expected type: (([Int] -> Int) -> t1 -> t0) -> t2 -> t0
      Actual type: ([Int] -> Int) -> t1 -> t0
    In the first argument of `y', namely `f'
    In the first argument of `f', namely `(y f)'
Failed, modules loaded: none.

He intentado adoptar un enfoque diferente simplemente definiendo el combinador externamente, sin embargo, esto todavía no funciona y realmente no enfrenta mi desafío para hacerlo en una expresión.

y f = f (y f)

msss' :: [Int] -> Int
msss' = y (\g' gmax lmax list -> if list == [] 
                                 then gmax 
                                 else g' (max gmax lmax + head list) 
                                         (max 0    lmax + head list) 
                                         tail list)

¿Puedes detectar qué pasa con lo que estoy haciendo? Estoy perdido. La queja de construir tipos infinitos realmente me marca porque, aunque Haskell se trataba de ese tipo de cosas. Tiene estructuras de datos infinitas, entonces, ¿por qué el problema con los tipos infinitos? Sospecho que tiene algo que ver con esa paradoja que mostró que el cálculo de lambda sin tipo es inconsistente. Aunque no estoy seguro. Sería bueno si alguien pudiera aclarar.

Además, tengo la impresión de que la recursión siempre se puede representar con las funciones de pliegue. ¿Alguien puede mostrarme cómo podría hacerlo simplemente usando un redil? Sin embargo, el requisito de que el código sea una sola expresión sigue en pie.

Answer 1

No puedes definir al combinador y así en Haskell. Como notó, eso da como resultado un tipo infinito. Afortunadamente, ya está disponible en Data.Function como fix, donde se define usando un let Unión:

fix f = let x = f x in x

Answer 2

Debido a que el combinador y necesita tipos infinitos, necesitará soluciones como éste.

Pero escribiría tu msss Funciona como una línea de una sola como esta:

msss = fst . foldr (\x (gmax, lmax) -> let g = max (lmax + x) in (g gmax, g 0)) (0, 0)

Answer 3

Bueno, pensemos en ello por un minuto. ¿Qué tipo tiene esta expresión lambda?

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

Bien f es una función (a -> b) -> a -> b, y x es algún valor b. ¿Qué hace eso? y? Bueno, dado lo que acabamos de decir sobre f,

(y y f) :: (a -> b)

Además, dado que estamos aplicando esta expresión a sí misma, sabemos que y tiene el mismo tipo que toda la expresión. Esta es la parte en la que me quedo un poco perplejo.

Asi que y es una función mágica de orden superior. Y se necesitan dos funciones como entrada. Entonces es algo así como y :: f1 -> f2 -> f3. f2 tiene la forma de f, y f3 tiene el tipo de resultado mencionado anteriormente.

y :: f1 -> ((a -> b) -> a -> b) -> (a -> b)

La pregunta es ... ¿Qué es f1? Bueno, tiene que ser lo mismo que el tipo de y. ¿Ves cómo esto está más allá del poder del sistema de tipo de Haskell? El tipo se define en términos de sí mismo.

f1 = f1 -> ((a -> b) -> a -> b) -> (a -> b)

Si quieres una "línea" autónoma, tome la sugerencia de Hammar en su lugar:

msss' = (\f -> let x = f x in x) 
        (\g' gmax lmax list -> case list of
            [] -> gmax
            (x:xs) -> g' (max gmax lmax + x) (max 0 lmax + x) xs
        ) 0 0

Aunque en mi humilde opinión max es permitido, entonces fix De Data. La función también debe estar permitida. A menos que esté en un concurso solo de preludio.