Это немного эзотерическое, но безумное. В ответе на еще один вопрос я отметил, что в этой полностью действующей программе
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 без дополнительной квантификации.
Что там происходит?