Почему я могу передавать частично применяемые конструкторы типов только в позиции параметра типа?

#haskell #higher-kinded-types #unification #higher-order-types

Вопрос:

Это, вероятно, глупый вопрос, но я не могу понять основные правила для следующего поведения:

 foo :: t (f a) -> f a b -- accepted
foo = undefined

bar :: t [f a] -> f a b -- rejected
bar = undefined

Вполне логично, что f применение к a и a b , соответственно, в bar приводит к ошибке вида и, таким образом, отклоняется. Но почему это foo принято?

1. t может иметь вид (* -> *) -> * , поэтому выполните сопоставление с конкретным типом. Для списка это невозможно, так как список имеет вид * -> * , и это, таким образом, означает, что f a он должен быть «конкретного» типа.

2. Рассмотрим data T container = T (container Int) (container String) тип , который является параметрическим по сравнению с типами контейнеров и содержит контейнер с Int s внутри и контейнер с String s внутри, а type F = (,) также семейство контейнеров , по одному для каждого типа метаданных, которые помечают один содержащийся элемент некоторыми метаданными.

3. Вам нужно уметь это делать, чтобы использовать трансформаторы монад, если вы слышали о них. Если нет, то в основном они преобразуют произвольную монаду в новую монаду, обладающую дополнительной функциональностью (один достаточно распространенный шаблон для построения сложного кода в Haskell состоит в том, чтобы укладывать несколько трансформаторов монад друг на друга). Для этого им нужно принять саму монаду в качестве параметра типа, а не применяемый монадический тип (например, им нужно принять Maybe , IO , State s и т. Д.; не Maybe Int , IO String , или State s () ).

Ответ №1:

Это что-то в этом роде f .

Поскольку тип возвращаемого f a b значения — т. е. f применяется к двум параметрам, — это означает, что f :: Type -> Type -> Type .

Но затем f a используется в качестве элемента списка [f a] — и элементы списка должны быть Type , что означает это f a :: Type , что означает это f :: Type -> Type .

Несоответствие.

foo работает, потому что типы могут быть частично применены. То есть, если f :: Type -> Type -> Type , то f a :: Type -> Type . И затем, типу t разрешается иметь параметр вида Type -> Type , так что все совпадает.

Чтобы повторить вышесказанное:

foo работает, потому что тип t может иметь параметр вида Type -> Type .
bar не работает, потому что тип [] (он же «список») должен иметь параметр вида Type .

1. На уровне терминов вы не можете передать аргумент функции функции первого порядка. Тот же принцип применим и к уровню типов. Я ожидал, что это будет глупый вопрос. Все дело в видах: foo :: t f -> t (->) -> f a b с радостью принимается.