online - haskell pdf

¿Por qué el operador en dólares($) es tan complejo en GHC 8.0.1?

Question

Prelude> :i ($)
($) ::
  forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r).
  (a -> b) -> a -> b
        -- Defined in ‘GHC.Base’
infixr 0 $

¿En qué se diferencia de (a -> b) -> a -> b ? ¿Hay alguna b que no se ajuste a la nueva firma de tipo?

Answer 1

Antes de la versión 8.0, había un caso especial en el buscador de tipos para hacer que funcionaran las aplicaciones de $ a tipos diferentes. Esto también significaba que no podía definir sus propias funciones que podrían funcionar con tipos elevados y sin elevar. Ahora que este llamado Levity Polymorphsim (''levidad'' se refiere a ''el grado en que algo se levanta'' - o ''lifting-ness'', debido a los tipos ''desatado'' y ''levantado'') está integrado en el comprobador de tipos, esto es posible:

import GHC.Exts (TYPE, RuntimeRep(..)) 
import Data.Kind (type (*))

ap :: forall (a :: *) (b :: *) . (a -> b) -> (a -> b) 
ap f x = f x 

ap_LP :: forall (a :: *) (b :: TYPE r) . (a -> b) -> (a -> b) 
ap_LP f x = f x

y, de hecho, la función $ ahora se define de forma idéntica a ap_LP , sin que se necesite un caso especial en el buscador de tipos para hacer que $ funcione con funciones que devuelven tipos desentendidos (todavía hay un caso especial en el buscador de errores para hacer una aplicación polimórfica, es decir, runST $ ... .trabajo, pero esto no está relacionado con el polimorfismo de la levedad). Esta es esencialmente la razón de la complejidad agregada: ahora hay menos ''hacks'' en el sistema de tipos, y los usuarios de GHC pueden aprovechar el polimorfismo de levidad simplemente al asignar a una función el tipo apropiado (tenga en cuenta que los tipos polimórficos de levidad nunca se deducen , Por lo que yo puedo decir). Antes del polimorfismo de la ligereza, si deseaba escribir una función polimórfica que pudiera funcionar en los tipos levantado y sin elevar, estaba obligado a escribir dos copias idénticas de la función con diferentes tipos de firmas.

El nuevo tipo difiere del anterior en que el nuevo tipo es estrictamente más general que el anterior:

-- ok 
ap'' :: forall (a :: *) (b :: *) . (a -> b) -> (a -> b) 
ap'' = ap_LP 

-- type error: 
--    * Couldn''t match a lifted type with an unlifted type
ap_LP'' :: forall (a :: *) (b :: TYPE r) . (a -> b) -> (a -> b) 
ap_LP'' = ap 

En otras palabras, cada b que "se ajuste" a la firma anterior debe (por definición) adaptarse a la nueva firma de tipo (¡y por lo tanto este cambio es perfectamente compatible con versiones anteriores!).

También tenga en cuenta que lo siguiente no es posible:

ap'''' :: forall (a :: TYPE r) (b :: *) . (a -> b) -> (a -> b)
ap'''' f x = f x 

El error producido es

A representation-polymorphic type is not allowed here:
  Type: a
  Kind: TYPE r
In the type of binder `x''

y SPJ explica la razón de la restricción here :

Es absolutamente correcto que el segundo argumento de ($) no debe tener un tipo sin caja. Debido a que el código para ($) debe mover ese argumento (pasar a la función), debe conocer su ancho, puntería, etc.

Pero en realidad estaría bien si el resultado de la llamada (f $ x) no estuviera en la caja, porque el código para ($) no se mete con el resultado; es sólo una llamada de cola f.

Esto quiere decir que no todos los tipos polimórficos de levidad tienen un habitante válido, y esto se relaciona con la distinción operacional entre los tipos sin caja y con caja, que solo pueden tratarse de manera uniforme en ciertos casos, y el tipógrafo se asegura de ello.