Почему доллар ($) является настолько сложным в GHC 8.0.1?

Ответ 1

До 8.0 в программе typechecker был особый случай, чтобы приложения $ работали в неработающих видах. Это также означало, что вы не могли определить свои собственные функции, которые могли бы работать как с поднятыми, так и с непринужденными видами. Теперь, когда этот так называемый Levity Polymorphsim ( "легкость" относится к "степени, в которой что-то поднимается" - или "поднятой", из-за "небрежного" и "поднятые" типы) встроен в typechecker, это возможно:

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

и действительно, функция $ теперь определена тождественно с ap_LP, без специального случая, необходимого в методе typechecker, чтобы сделать $ работать с функциями, возвращающими неперекрываемые типы (есть еще особый случай в typechecker для сделать полиморфное приложение, т.е. runST $ ... работать, но это не связано с полиморфизмом легкомыслия). Это по существу является причиной дополнительной сложности - в системе типов теперь меньше "хаков", и пользователи GHC могут использовать полиморфизм левитирования, просто предоставляя функции соответствующему типу (обратите внимание: никогда не выходят из строя полиморфизм типа levity, насколько я могу судить). До полиморфизма легкомыслия, если вы хотите написать полиморфную функцию, которая могла бы работать как с поднятыми, так и с неактивными видами, вы были обязаны написать две идентичные копии функции с сигнатурами различного типа.

Новый тип отличается от старого тем, что новый тип является строго более общим, чем старый:

-- 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 

Другими словами, каждый b, который "подгоняет" старую подпись, должен (по определению) соответствовать новой сигнатуре типа (и, таким образом, это изменение отлично обратное!).

Также обратите внимание, что следующее невозможно:

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

Произошла ошибка

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

и SPJ объясняет причину ограничения здесь:

Совершенно верно, что второй аргумент ($) не должен иметь распакованный. Поскольку код для ($) должен перемещать этот аргумент вокруг (перейдите к функции), поэтому он должен знать его ширину, ect указателя.

Но на самом деле было бы нормально, чтобы результат вызова (f $x) был unboxed, потому что код для ($) не испортит результат; Это только хвостовые вызовы f.

Это означает, что не каждый левити-полиморфный тип имеет действительного жителя - и это относится к оперативному различию между типами unboxed и boxed, которые могут обрабатываться единообразно только в определенных случаях, и проверка typechecker гарантирует это.