Ответ 1
Это вопрос программирования языка программирования. Это можно сделать так, как вы предлагаете, но я утверждаю, что это плохая идея.
Не очевидно ли из сигнатуры типа, что я хочу передать полиморфную функцию первого класса в ListScott?
Я не думаю, что мы можем, очевидно, многое сказать об этом определении.
Универсальный или экзистенциальный? Конфликт с обозначением GADT
Здесь мы можем написать с расширением GADTs:
data ListScott a where
ListScott :: { unconsScott :: (a -> ListScott a -> r) -> r -> r } -> ListScott a
Здесь r экзистенциально количественно определяется в поле unconsScott, поэтому конструктор имеет первый тип ниже:
ListScott :: forall a r. ((a -> ListScott a -> r) -> r -> r) -> ListScott a
-- as opposed to
ListScott :: forall a. (forall r. (a -> ListScott a -> r) -> r -> r) -> ListScott a
Вывод отключает обнаружение ошибок
Что делать, если r вместо этого означает параметр ListScott, но мы просто забыли его добавить? Я считаю, что это достаточно вероятная ошибка, потому что и гипотетические ListScott r a, и ListScott a могут служить в качестве представлений списков в некотором роде. Тогда вывод связующих будет приводить к принятию ошибочного определения типа, а ошибки сообщаются в другом месте, как только тип будет использоваться (надеюсь, не слишком далеко, но это все равно будет хуже, чем ошибка в самом определении).
Explicitness также предотвращает опечатки, когда конструктор типа получает туманность как переменную типа:
newtype T = T { unT :: maybe int }
-- unlikely to intentionally mean "forall maybe int. maybe int"
Недостаточно контекста в объявлении типа, чтобы уверенно догадываться о значении переменных, поэтому мы должны принудительно привязывать переменные должным образом.
читаемость
Рассмотрим запись функций:
data R a = R
{ f :: (r -> r) -> r -> r
, g :: r -> r
}
data R r a = R
{ f :: (r -> r) -> r -> r
, g :: r -> r
}
Мы должны посмотреть слева от =, чтобы определить, существует ли там r, а если нет, мы должны мысленно вставлять связующие в каждом поле. Я считаю, что первая версия трудно читать, потому что переменная r в двух полях фактически не будет находиться под одним и тем же переплетчиком, но она, безусловно, выглядит иначе.
Сравнение с аналогичными конструкциями
Обратите внимание, что что-то похожее на то, что вы предложили, происходит с типами классов, которое можно рассматривать как своего рода запись:
class Functor f where
fmap :: (a -> b) -> f a -> f b
Большинство аргументов выше применимы также, и поэтому я бы предпочел написать этот класс как:
class Functor f where
fmap :: forall a b. (a -> b) -> f a -> f b
Аналогичное утверждение можно было бы сказать о локальных аннотациях типа. Однако подписи верхнего уровня различны:
id :: a -> a
Это однозначно означает id :: forall a. a -> a, потому что нет другого уровня, где a может быть привязан.