rayas - ¿Existe una relación entre el signo de dólar($) y la función de identificación en Haskell?

signo peso con dos rayas

Question

Uno de estos días estaba leyendo comentarios sobre el Monad Challenge (que recomiendo encarecidamente a cualquier principiante en Haskell, como yo), y terminé en este hilo donde leí que ($) = id .

No sé cómo asustar a la gente, pero muchos lenguajes de programación tienen conceptos que se demuestran mejor con pequeños ejemplos que hacen que la gente diga "whoa".

Por ejemplo, es sorprendente que append () en Prolog pueda ejecutarse "hacia atrás" desde el resultado concatenado para producir todas las listas que pueden concatenarse para producirlo. O que el operador de enlace monádico en Haskell (>> =) se puede definir en términos de unión y fmap, o que ($) = id.

($) = id !?

<lo intenta en Raskell / Ghci>

Ahora veo por qué es verdad, pero aún así ... ¡Whoah! ¡Gracias por eso! (...)

Luego verifiqué el código base-4.10.0.0 , buscando las definiciones de ($) e id , pero justo arriba, leí esto:

NOTA BENE: Do NOT use ($) anywhere in this module! The type of ($) is slightly magical (it can return unlifted types), and it is wired in. But, it is also *defined* in this module, with a non-magical type. GHC gets terribly confused (and *hangs*) if you try to use ($) in this module, because it has different types in different scenarios. This is not a problem in general, because the type ($), being wired in, is not written out to the interface file, so importing files don''t get confused. The problem is only if ($) is used here. So don''t!

Y sus implementaciones son:

-- | Identity function.
id                      :: a -> a
id x                    =  x

-- | Application operator.
{-# INLINE ($) #-}
($)                     :: (a -> b) -> a -> b
f $ x                   =  f x

Intenté intercambiar uno por otro en GHCi y todo lo que obtuve fueron errores tipográficos (como esperaba). Ahora, tengo más preguntas de las que empecé:

1. ¿Qué quieren decir con decir que ($) = id ?
2. ¿En qué casos es cierta esa afirmación? ¿Eso significa que puedo usar uno en lugar de otro?
3. En la base , ¿qué se entiende por decir que ($) es "levemente mágico (puede devolver tipos sin elevar)" y "estar conectado"?
4. ¿Y qué hay de "diferentes tipos en diferentes escenarios"? Pensé que, dado que Haskell es un lenguaje fuertemente tipificado, una vez que define una firma de tipo, esa firma se conserva hasta el final del Tiempo. ¿No es eso cierto? ¿Hay casos en que uno puede cambiar el tipo de una función?

Answer 1

1. ¿Qué quieren decir con decir que ($) = id ?

La función ($) podría definirse como

($) f x = f x

Es decir, tomar una función y un argumento y devolver el resultado de la aplicación. De manera equivalente, gracias al curry, podemos interpretar que tomar solo f y devolver una función de x .

($) f = /x -> f x

Aquí, podemos observar que la función /x -> fx asigna cualquier entrada x a fx - ¡eso es también lo que hace f ! Entonces, podemos simplificar la definición a

($) f = f

Ahora, este es el mismo que el id y = y definición de la función de identidad id y = y , por lo que podríamos escribir

($) = id

2. ¿En qué casos es cierta esa afirmación? ¿Eso significa que puedo usar uno en lugar de otro?

La ecuación se mantiene siempre, pero hay dos advertencias.

La primera es que ($) tiene un tipo más restringido que el de id , ya que ($) f = f mantiene solo para una función f , no para ningún valor f . Esto significa que puede reemplazar ($) con id , pero no al revés. Cuando se escribe

($) = id

se podría hacer explícito el argumento de tipo implícito y escribir que, para cualquier tipo a y b

($) @ a @ b = id @ (a->b)

La otra advertencia es que, en presencia de una función de mayor rango, ($) recibe un manejo especial durante la verificación de tipo, mientras que la id no. Este es el punto 3 de golpe.

3. En la base, ¿qué se entiende por decir que ($) es "levemente mágico (puede devolver tipos sin elevar)" y "estar conectado"?

Normalmente, en funciones polimórficas tales como

id :: forall a . a -> a

La variable de tipo a puede ser instanciada a otros tipos, pero solo bajo algunas restricciones. Por ejemplo, a puede ser instanciado a Int , pero no puede ser instanciado a otro tipo polimórfico para todos forall b . ... forall b . ... Esto mantiene el sistema de tipos predicativo , lo que ayuda mucho durante la inferencia de tipos.

Por lo general, esto no es un problema en la programación diaria. Sin embargo, algunas funciones utilizan tipos de rango 2, por ejemplo, runST

runST :: (forall s. ST s x) -> x

Si escribimos

runST (some polymorphic value here)

el tipo de sistema puede escribir comprobar que. Pero si usamos el lenguaje común

runST $ some polymorphic value here

entonces el motor de inferencia de tipos debe tomar el tipo de ($)

($) :: forall a b . (a -> b) -> a -> b

y elige a ~ forall s. ST sx a ~ forall s. ST sx que es polimorfo, por lo tanto prohibido.

Dado que este idioma es demasiado común, los desarrolladores de GHC decidieron agregar un caso especial a la escritura de ($) para permitir esto. Dado que esto es un poco ad-hoc, si define su propio ($) (posiblemente con otro nombre), e intente escribir check runST $ ... esto fallará ya que no usa el caso especial.

Además, no se puede crear una instancia de tipos sin caja como Int# , o tuplas sin caja (# Int#, Int# #) . Estas son extensiones de GHC que permiten funciones de escritura que pasan un entero "sin procesar", sin la envoltura de procesador habitual. Esto puede cambiar la semántica, por ejemplo, hacer que las funciones sean más estrictas de lo que son. A menos que desee exprimir más el rendimiento de algún código numérico, puede ignorarlo.

(Estoy dejando esta parte aquí, pero lisyarus ya la cubrió con mayor precisión).

f $ x = f x
-- i.e.
($) f x = f x
-- i.e.
($) f x = id f x
-- eta contraction
($) f = id f
-- eta contraction
($) = id

Básicamente, ($) es id , pero con un tipo más restrictivo. id se puede usar en argumentos de cualquier tipo, ($) lugar toma un argumento de función.

($) :: (a -> b) -> a -> b
-- is better read as
($) :: (a -> b) -> (a -> b)
-- which is of the form (c -> c) with c = (a -> b)

Tenga en cuenta que id :: c -> c , por lo que el tipo de ($) es de hecho un caso especial.

¿Y qué hay de "diferentes tipos en diferentes escenarios"? Pensé que, dado que Haskell es un lenguaje fuertemente tipificado, una vez que define una firma de tipo, esa firma se conserva hasta el final del Tiempo. ¿No es eso cierto? ¿Hay casos en que uno puede cambiar el tipo de una función?

En el código de las bibliotecas que definen ($) , GHC tiene que jugar algunos trucos para que las reglas de escritura especiales funcionen para las otras bibliotecas y programas. Para eso, aparentemente se requiere no usar ($) en dicha biblioteca. A menos que esté desarrollando GHC o el módulo base que pasa a definir ($) , puede ignorarlo. Es un detalle de implementación interno del compilador, no es algo que el usuario del compilador y las bibliotecas deben saber.

Answer 2

Haskell de hecho está fuertemente tipado; el problema está relacionado con algunos hackers específicos para el operador ($) . Desafortunadamente, no tengo idea de qué se trata: con suerte alguien contestará su pregunta 3 (y la pregunta 4 automáticamente).

Con respecto a la pregunta 1, mira los tipos:

id :: a -> a
($) :: (a -> b) -> (a -> b)

Renombra c = a -> b y obtienes ($) :: c -> c , lo que significa que el tipo de ($) es una especificación del tipo de id , de modo que al menos los tipos nos permiten usar id para implementar ($) .

Ahora, mira la definición de ($) :

f $ x = f x

Vamos a reescribirlo un poco:

($) f = /x -> f x

Y aplicar eta-reducción:

($) f = f

Ahora se ve claramente que ($) es solo id con un tipo un poco más específico (de modo que f es siempre una función).

Tenga en cuenta que no funciona de otra manera, ya que el tipo de ($) es más restrictivo. Por ejemplo, puede llamar a id 5 y obtener 5 como resultado, pero ($) 5 no verificará: 5 no tiene el tipo de formulario a -> b .

El punto de ($) es que tiene una prioridad muy baja y permite evitar llaves alrededor de los argumentos de f , y se puede usar como

someFunction $ whatever complex computation you dont need braces around