Почему `[1," a "] :: [forall a. Показать a => a] `не разрешено?

Question

В моих (Мощи некорректных) пониманиях, следующие два списка должен быть эквивалентен:

[1, "a"] :: [forall a. Show a => a] 

data V = forall a. Show a => V a 
[V 1, V "a"] :: [V] 

Однако первый один не принят, но второй один работает отлично (с ExistentialQuantification).

Если первого списка не существует, каков будет тип в пробе map V :: ??? -> [V]? Какой тип механизма обеспечивает наличие оболочки?

Answer 1

Ваше понимание неверно. Большая часть проблемы заключается в том, что традиционный синтаксис экзистенциального квантификации, который вы использовали, довольно запутан для всех, кто не знаком с ним. Поэтому я настоятельно рекомендую использовать вместо этого синтаксис GADT, который также имеет преимущество быть более сильным. Легкая вещь - просто включить {-# LANGUAGE GADTs #-}. Пока мы на нем, давайте включим {-# LANGUAGE ScopedTypeVariables #-}, потому что мне неинтересно задавать вопрос, что означает forall в любом месте. Ваше V определение означает то же самое, как

data V where 
    V :: forall a . Show a => a -> V 

Мы можем на самом деле падение явный forall, если нам нравится:

data V where 
    V :: Show a => a -> V 

Так конструктор данных V это функция, которая принимает что-то любой showable типа и производит что-то типа V. Тип map довольно ограничительно:

map :: (a -> b) -> [a] -> [b] 

Все элементы списка, передаваемые map должны иметь одинаковый тип. Таким образом, тип map V просто

map V :: Show a => [a] -> [V] 

Давайте вернемся к вашему первому выражению в настоящее время:

[1, "a"] :: [forall a. Show a => a] 

Теперь то, что это на самом деле говорит, что [1, "a"] список, каждый из элементов которого имеет тип forall a . Show a => a. То есть, если я предоставляю любой a, который является экземпляром Show, каждый элемент списка должен иметь этот тип. Это просто неправда. "a" не, например, есть тип Bool. Здесь есть еще одна проблема; тип [forall a . Show a => a] является «нецелесообразным». Я не понимаю детали того, что это значит, но, как вы говорите, вы запустили forall в аргументе конструктора типа, отличного от ->, и это недопустимо. GHC может предложить вам включить расширение ImpredicativeTypes, но это действительно не работает правильно, поэтому вам не следует. Если вам нужен список существительно сугубо квантифицированных вещей, вам необходимо сначала их обернуть в экзистенциальные типы данных или использовать специализированный тип экзистенциального списка. Если вам нужен список предметов с квантованием по всему миру, сначала их нужно обернуть (возможно, в newtypes).