Существуют ли для этого какие-либо теоретические причины (например, проверка типов или вывод типов стали бы неразрешимыми) или практические причины (слишком трудно осуществить должным образом)?
В настоящее время мы можем обернуть вещи newtypeкак
newtype Pair a = Pair (a, a)
а затем есть Pair :: * -> *
но мы не можем сделать что-то подобное λ(a:*). (a,a).
(Есть некоторые языки, в которых они есть, например, в Scala .)
haskell
abstraction
type-systems
lambda
Петр Пудлак
источник
источник
Ответы:
Вывод типа с лямбдами на уровне типа потребует объединения более высокого порядка, что неразрешимо. Это мотивация для их запрета. Но, как это случилось с другими неразрешимыми функциями (такими как вывод типов для GADT), может потребоваться подпись типов и разрешить это. Я не уверен, что это кто-то расследовал.
источник