Что происходит с отсутствующими переменными типа в ядре церковного стиля?

Это немного эзотерическое, но безумное. В ответе на еще один вопрос я отметил, что в этой полностью действующей программе

poo :: String -> a -> a
poo _ = id

qoo :: (a -> a) -> String
qoo _ = ""

roo :: String -> String
roo = qoo . poo

переменная типа a не решается и не обобщается в процессе проверки roo. Мне интересно, что происходит в переводе на основной язык GHC, вариант в стиле церкви System F. Позвольте мне прочесть вещи из рук в руки, с явным типом lambdas /\ и типами приложений @.

poo :: forall a. [Char] -> a -> a
poo = /\ a -> \ s x -> id @ a

qoo :: forall a. (a -> a) -> [Char]
qoo = /\ a -> \ f -> [] @ Char

roo :: [Char] -> [Char]
roo = (.) @ [Char] @ (? -> ?) @ [Char] (qoo @ ?) (poo @ ?)

Что происходит в местах ?? Как roo становится допустимым ключевым термином? Или мы действительно получаем загадочный пустой квантификатор, несмотря на то, что говорит подпись типа?

roo :: forall a. [Char] -> [Char]
roo = /\ a -> ...

Я только что проверил, что

roo :: forall . String -> String
roo = qoo . poo

проходит через ok, что может или не означает, что вещь typechecks без дополнительной квантификации.

Что там происходит?

Ответы

Ответ 1

Здесь ядро ​​сгенерировано GHC (после добавления некоторых NOINLINE прагм).

qoo_rbu :: forall a_abz. (a_abz -> a_abz) -> GHC.Base.String
[GblId, Arity=1, Caf=NoCafRefs]
qoo_rbu = \ (@ a_abN) _ -> GHC.Types.[] @ GHC.Types.Char

poo_rbs :: forall a_abA. GHC.Base.String -> a_abA -> a_abA
[GblId, Arity=1]
poo_rbs = \ (@ a_abP) _ -> GHC.Base.id @ a_abP

roo_rbw :: GHC.Base.String -> GHC.Base.String
[GblId]
roo_rbw =
  GHC.Base..
    @ (GHC.Prim.Any -> GHC.Prim.Any)
    @ GHC.Base.String
    @ GHC.Base.String
    (qoo_rbu @ GHC.Prim.Any)
    (poo_rbs @ GHC.Prim.Any)

Кажется, что GHC.Prim.Any используется для полиморфного типа.

Из документы (внимание мое):

Конструктор типа Any - это тип, к которому вы можете поднятый тип и назад.

  • Поднимается и, следовательно, отображается указателем
  • Он не претендует на быть типом данных, и это важно для генератора кода, потому что код gen может ввести значение данных, но никогда не вводит значение функции.

Он также используется для создания экземпляров без ограничений типа после типа проверка.

Имеет смысл иметь такой тип для вставки вместо не-ограниченных типов, поскольку в противном случае тривиальные выражения, такие как length [], вызывают неоднозначную ошибку типа.

Ответ 2

Это не проблема. В сигнатуре roo переменная типа a просто не отображается, как она есть. Более простым примером могло бы быть выражение

const 1 id

где

id :: forall a.a->a