Почему этот код Haskell проверяет типы с помощью fundeps, но выдает неприкасаемую ошибку с семействами типов?

Учитывая некоторые определения типов:

data A
data B (f :: * -> *)
data X (k :: *)

… И этот класс типов:

class C k a | k -> a

… Эти (очень надуманные для целей минимального примера) определения функций typecheck:

f :: forall f. (forall k. (C k (B f)) => f k) -> A
f _ = undefined

g :: (forall k. (C k (B X)) => X k) -> A
g = f

Однако, если мы используем семейство типов вместо класса с функциональной зависимостью:

type family F (k :: *)

… Тогда эквивалентные определения функций не могут быть проверены по типу:

f :: forall f. (forall k. (F k ~ B f) => f k) -> A
f _ = undefined

g :: (forall k. (F k ~ B X) => X k) -> A
g = f


• Couldn't match type ‘f0’ with ‘X’
    ‘f0’ is untouchable
      inside the constraints: F k ~ B f0
      bound by a type expected by the context:
                 F k ~ B f0 => f0 k
  Expected type: f0 k
    Actual type: X k
• In the expression: f
  In an equation for ‘g’: g = f

I read Section 5.2 of the OutsideIn(X) paper, which describes touchable and untouchable type variables, and I sort of understand what’s going on here. If I add an extra argument to f that pushes the choice of f outside the inner forall, then the program typechecks:

f :: forall f a. f a -> (forall k. (F k ~ B f) => f k) -> A
f _ _ = undefined

g :: forall a. X a -> (forall k. (F k ~ B X) => X k) -> A
g = f

Однако в этом конкретном примере меня так смутило то, почему функциональная зависимость имеет другое поведение. Я слышал, как люди в разное время утверждали, что функциональные зависимости, подобные этой, эквивалентны семейству типов плюс равенство, но это демонстрирует, что на самом деле это не так.

Какую информацию предоставляет в этом случае функциональная зависимость, позволяющая создать экземпляр f способом, который не позволяет семейство типов?


functional-dependencies haskell type-families
person Alexis King    schedule 10.12.2017    source источник
comment
Обратите внимание, что g = f @ X также набирает проверки. Кажется, что алгоритм вывода не обязуется выбирать переменную типа f как X. Я не понимаю почему - обычно это потому, что может быть другое значение f, делающее тип (forall k. (F k ~ B f) => f k) -> A равным (forall k. (F k ~ B X) => X k) -> A. Здесь f ~ X кажется мне единственным решением (не так ли?). Интересный.   -  person chi    schedule 10.12.2017
comment
@chi Я тоже так думаю, но я недостаточно знаю об этом конкретном случае проверки типов, чтобы уверенно открыть ошибку. Возможно, мне все равно следует открыть заявку, и если это предполагаемое поведение, я, по крайней мере, возможно, узнаю, почему?   -  person Alexis King    schedule 10.12.2017
comment
Действительно интересно! Я теперь дважды повторял свое мнение о том, должна ли эта проверка типов выполняться с помощью ни fundeps и не семейств типов, или только с fundeps, или с обоими. Я просто недостаточно хорошо понимаю, как решаются ограничения. Но, по крайней мере, я не считаю неправдоподобным, что только версия fundep должна работать: решающее различие, похоже, состоит в том, что классы типов с их суперклассами можно «распутать» (f извлекается из B f), но из ограничения равенства это это невозможно.   -  person leftaroundabout    schedule 10.12.2017
comment
Не ответ, но по вашему вопросу я слышал, как люди утверждали, что функциональные зависимости, подобные этой, эквивалентны семейству типов плюс равенство - да, это немного упрощает. Когда вы думаете о Core, вы можете увидеть, откуда берутся семантические различия. Экземпляры семейства типов выражаются как приведение верхнего уровня, поэтому type instance F Int = Bool превращается в f_int :: F Int ~ Bool. Fundeps просто проявляется как ограничения во время объединения, они не влияют на принуждение. Вот почему трудно конвертировать между ними.   -  person Benjamin Hodgson♦    schedule 10.12.2017
comment
Извините, у меня тоже нет ответа, но будьте осторожны: вы не показали, что версия FunDep позволяет создать экземпляр f. Потому что вы не объявили никаких экземпляров для C (и получили f для работы с ними). Проверка семейства типов более активна, чем для FunDeps. Таким образом, у вас может быть, что на самом деле две формы эквивалентны в том смысле: форма семейства Type не компилируется; форма FunDep не имеет жилых экземпляров для f. Возможно поэтому вы можете определить только f _ = undefined. Итак, объявите экземпляр для C; попробуйте применить f к чему-нибудь. Аналогично попробуйте применить g.   -  person AntC    schedule 11.12.2017
comment
@AntC Это сокращение от более крупного фактического примера, где C фактически Reifies из Data.Reflection. Уверяю вас, он действительно выполняет проверку типов без каких-либо оснований где-либо и после применения g. Вы даже можете настроить этот пример для проверки типов без оснований, изменив C на Reifies и изменив определение f на f m = reify B (\(_ :: Proxy s) -> m @s seq` A) `(после того, как сделали A и B обитаемыми).   -  person Alexis King    schedule 11.12.2017
comment
чтобы ответить на первый комментарий @ chi: с g = f, да, это исправляет типы s.t. f ~ X. Если вы удалите определение для g, тогда f может быть любым типом конструктора, например Maybe.   -  person AntC    schedule 02.01.2018

Ответы (2)


arrow_upward
1
arrow_downward

Я не знаю, стоит ли публиковать это в качестве ответа, потому что это все еще довольно непросто, но я действительно думаю, что по сути происходит вот что:

Чтобы оценить значение (C k (B X)) => X k, вы должны выбрать конкретный тип для k и указать instance C k (B X), который удовлетворяет ограничениям. Для этого вы должны сформулировать, что аргумент a класса типов имеет форму B f, из которой компилятор может извлечь тип f (и выяснить, что это X в данном случае), что важно, он может сделать это до того, как глядя на экземпляр, который станет точкой, в которой f станет неприкасаемым.

Чтобы оценить (F k ~ B X) => X k, это немного другое. Здесь вам не нужно указывать на конкретный экземпляр, вам просто нужно гарантировать, что если компилятор найдет семейство типов для F k, тогда этот тип будет того же типа, что и B X. Но прежде чем фактически искать экземпляр, компилятор не может здесь сделать вывод, что F k имеет форму B f, и, следовательно, также не использовать это для унификации f с внешним аргументом квантификации из-за неприкасаемости.

Следовательно, поведение GHC, по крайней мере, не является полностью необоснованным. Я до сих пор не уверен, следует вести себя подобным образом.

person leftaroundabout    schedule 10.12.2017
comment
Хотя то, что вы говорите, имеет некоторый смысл, я немного скептически отношусь к этому ответу. Вот почему: если вы измените data B на type family B, версия с функциональной зависимостью все равно будет проверяться типом! Похоже, это противоречит вашему объяснению того, почему версия fundep работает именно так, поскольку B f ~ B X не подразумевает f ~ X, если B является семейством типов. - person Alexis King; 10.12.2017

arrow_upward
1
arrow_downward

Хорошо, у меня была возможность поиграть с этим. Есть несколько отвлекающих факторов:

В версии Type Family только определение для f дает ошибку 'f0' is untouchable. (Вы можете подавить это с помощью AllowAmbiguousTypes; это просто откладывает ошибку до появления g.) Давайте проигнорируем g здесь.

Тогда без AllowAmbiguousTypes сообщение об ошибке для f дает дополнительную информацию:

• Couldn't match type ‘f0’ with ‘f’
    ‘f0’ is untouchable
      inside the constraints: F k ~ B f0
      bound by the type signature for:
                 f :: F k ~ B f0 => f0 k
  ‘f’ is a rigid type variable bound by
    the type signature for:
      f :: forall (f :: * -> *). (forall k. F k ~ B f => f k) -> A
  Expected type: f0 k
    Actual type: f k

Ага! rigid type variable проблема. Я предполагаю, потому что f фиксируется ограничением равенства из k, которое также является жестким, потому что ...

Переходя к версии FunDep без g, какие типы мы можем вызывать f? Пытаться

f (undefined undefined :: X a)           -- OK
f (undefined "string"  :: X String)      -- rejected
f  Nothing                               -- OK
f (Just 'c')                             -- rejected

Сообщение об отказе (для примера X String)

• Couldn't match type ‘k’ with ‘String’
  ‘k’ is a rigid type variable bound by
    a type expected by the context:
      forall k. C k (B X) => X k
  Expected type: X k
    Actual type: X String
• In the first argument of ‘f’, namely
    ‘(undefined "string" :: X String)’

Обратите внимание, что сообщение касается k, не f, что определяется FunDep - или могло бы быть, если бы мы могли найти подходящий k.

Объяснение

Сигнатура для функции f говорит, что k экзистенциально определена количественно / имеет более высокий рейтинг. Тогда мы не можем позволить какой-либо информации о типе k ускользнуть в окружающий контекст. Мы не можем предоставить какое-либо (не нижнее) значение для k, потому что его тип будет вторгаться в forall.

Вот более простой пример:

f2 :: forall f. (forall k. f k) -> A
f2 _ = undefined

f2 Nothing                                 -- OK
f2 (Just 'c')                              -- rejected rigid type var

Так что исходная FunDep версия компилируется только для отвлечения внимания: в ней нельзя жить. (И это общий симптом с FunDeps, как я ранее подозревал.)

person AntC    schedule 01.01.2018
comment
Кстати, с этой подписью f :: forall f. (forall k. f ~ X => f k) -> A вы получите аналогичное f0 is untouchable отклонение. В поле зрения нет Type Family или FunDep. - person AntC; 02.01.2018