Что такое грамматика System FC2 для видов?

Я пытаюсь понять этот пост в блоге о расширении ConstraintKinds.

В разделе комментариев был пост, который я совершенно не понял. Вот:

Адам М говорит: 14 сентября 2011 г., 19:53 UTC

Вау, это звучит здорово. Планируется ли он стать частью официального GHC 7.4? Кроме того, означает ли это, что вы ввели третью постановку в системную грамматику FC2 для видов? В настоящее время у него есть * и k~>k как единственные альтернативы, где k1~>k2 (в основном) разновидность (forall a::k1 . (t::k2)). Похоже, это добавит k1==>k2, что-то вроде (a::k1 => (t::k2)). Или эти два вида на самом деле одинаковы?

Может кто-нибудь, пожалуйста, проанализируйте это шаг за шагом или, по крайней мере, предоставьте несколько ссылок, которые помогли бы мне самому обдумать это. Некоторые ключевые моменты, которые я должен выделить:

  1. Что такое грамматика System FC2 для видов? (Возможно, основной и самый общий, ответ которого включает два других.)
  2. Я пытался объяснить, почему k1~>k2 (в основном) похоже на (forall a::k1 . (t::k2))? Насколько я понимаю, ~> - это какое-то специальное обозначение для -> в видах, поскольку * и k1 -> k2 единственные обитатели стандартной системы видов Haskell (соответствует их описанию: в настоящее время у него есть * и k~>k как единственные альтернативы). Таким образом, формула (forall a::k1 . (t::k2)) означает, что если мы возьмем обитаемый тип k1, он может быть отображен на другой k2 тогда и только тогда, когда он обитаемый (из-за Curry-Howard работает для типов так же, как и для типов). Это правильно? (P.S.: я вижу, как эта интуиция дает сбои, если я не понимаю понятия среды обитания для видов; соответствуют ли виды Истинным доказуемым формулам (см. комментарии), когда они имеют обитаемый тип как обитатель или произвольный тип? Во втором случае интуиция подводит.)
  3. Что означает => в формуле для k1==>k2, а именно (a::k1 => (t::k2))?

Ответ, который получил этот комментарий:

Макс говорит: 14 сентября 2011 г., 21:11 UTC

Адам: это не так сложно! Он просто добавляет базовый вид Constraint к грамматике видов. Это своего рода типы, населенные значениями, как и существующие типы * и #.

Итак, автор утверждает, что Адам М слишком усложнил расширение. Их ответ довольно легко понять. В любом случае, даже если комментарий Адама М не соответствует действительности, я думаю, что он полностью заслуживает внимания, поскольку он познакомил меня с некоторыми незнакомыми понятиями.


constraints functional-programming haskell type-kinds type-theory
person Zhiltsoff Igor    schedule 18.04.2021    source источник
comment
Лично я думаю, что Адам М просто запутался. Я бы проигнорировал комментарий на вашем месте; даже если не принимать во внимание, было ли это сложнее, чем правда, или нет, это не имеет особого смысла, и биты, которые я могу расшифровать, кажутся неправильными.   -  person Daniel Wagner    schedule 19.04.2021
comment
@DanielWagner, так что грамматика для видов не идет дальше S to *, #, Constraint, ... | S to (S -> S)? Кстати, во втором вопросе я предложил собственное утверждение. Можете ли вы прокомментировать это, пожалуйста? Кроме того, не могли бы вы прокомментировать понятие среды обитания для видов (которое я также обсуждал во втором пункте).   -  person Zhiltsoff Igor    schedule 19.04.2021
comment
Фрагмент, который вы процитировали в вопросе 2, - это именно тот фрагмент, который я был наиболее уверен в расшифровке и названии неверным. Я по-прежнему не рекомендую пытаться расширить его собственными мыслями. Насчет Карри-Ховарда... вообще верно не понятие. Есть доказуемое и недоказуемое; и хотя я не знаю наверняка, я подозреваю, что то, как большинство людей использует обитаемый, должно быть синонимом доказуемого.   -  person Daniel Wagner    schedule 19.04.2021
comment
@DanielWagner, верно, извините, я ошибся. Итак, а именно: закон Пирса (((P → Q) → P) → P) ~в целом верен~ в классической логике, но недоказуем, поскольку является законом. Таким образом, нет ни функции типа ∀ a b. ((a -> b) -> a) -> a, ни оператора типа ∀ p q. ((p -> q) -> p) -> q, поскольку они соответствовали бы несуществующему доказательству закона Пирса. Я, наконец, понял это правильно?   -  person Zhiltsoff Igor    schedule 19.04.2021
comment
Мне все это кажется правильным.   -  person Daniel Wagner    schedule 19.04.2021
comment
@DanielWagner забыл упомянуть. Мне понравился трюк с законом Пирса в этой статье о переполнении стека.   -  person Zhiltsoff Igor    schedule 19.04.2021

Ответы (1)


arrow_upward
2
arrow_downward

System FC2 – это термин, введенный Вейрихом et al в их статье 2010 года Абстракция генеративных типов и вычисления на уровне типов (ссылка). Это относится к добавлению ролей в System FC и послужило основой для реализации в GHC, описанной в статье 2016 года Безопасные приведения с нулевой стоимостью для Haskell. System FC, в свою очередь, представляет собой систему, изначально описанную в эта статья (или на самом деле более ранняя статья, которая является расширенной версией после публикации), которая расширила обычное полиморфное лямбда-исчисление System F с помощью равенств типов .

Однако я думаю, что Адам М., вероятно, использовал термин System FC2 менее формально для обозначения любой системы типов, которую GHC реализовывал на момент написания комментария. Итак, смысл фразы:

представил третью продукцию в грамматике System FC2 для видов

действительно:

добавлено третье правило производства в грамматику видов, так как виды в настоящее время реализованы в GHC

Он утверждал, что грамматика для видов в настоящее время имеет два правила производства:

  1. * это вид
  2. Если k1 и k2 — виды, то k1 ~> k2 — вид.

и он спрашивал, дает ли это расширение третье правило производства:

  1. Если k1 и k2 — виды, то k1 ==> k2 — вид.

Как вы уже догадались, он ввел оператор ~>, чтобы отличать стрелку уровня типа от стрелки уровня типа. (В GHC стрелочные операторы уровня вида и уровня типа записываются одинаково ->.) Он дал определение ~> следующим образом:

где k1~>k2 (в основном) вид (forall a::k1 . (t::k2)).

что интерпретируется, но очень неточно. Он пытался использовать forall здесь как своего рода лямбду уровня типа. Это не так, но вы можете себе представить, что если бы у вас был тип forall a. t, вы могли бы создать его экземпляр для определенного типа a, и если для всех a :: k1 вы получите t :: k2, то этот полиморфный тип как бы представляет неявную функцию типа вида k1 ~> k2. Но полиморфизм/универсальная квантификация здесь неуместны. Важно то, как a появляется в выражении t, и в какой степени вы можете выразить выражение уровня типа t как, скажем, функцию уровня типа:

type Whatever a = t

или, если бы в Haskell были лямбда-выражения на уровне типов, лямбда-выражения на уровне типов с a в качестве аргумента и t в качестве тела:

Lambda a. t

Вы ничего не добьетесь, если будете серьезно рассматривать forall a. t как обладателя вида k1 -> k2.

Основываясь на этой расплывчатой ​​интерпретации ~>, он попытался спросить, существует ли новый оператор уровня типа ==>, такой, что отношение между оператором уровня типа ~> и выражением уровня типа forall a. b было таким же, как отношение между новым оператором уровня типа forall a. b. гипотетический оператор уровня вида ==> и выражение уровня типа a => b. Я думаю, что единственный разумный способ интерпретировать этот вопрос — представить, что он хотел рассматривать выражение типа a => b как параметризованное a, точно так же, как он представлял forall a. b параметризованным a, поэтому он хотел рассмотреть уровень типа функция формы:

type Something a = a => b

и рассмотрим вид Something. Здесь вид Something есть Constraint ~> *. Итак, я полагаю, что ответ на его последний вопрос заключается в том, что эти два типа на самом деле одинаковы, и никакой другой оператор уровня вида, кроме ~>, не требуется.

Ответ Макса объяснил, что расширение не добавило никакого нового оператора уровня типа, а просто добавило новый примитивный вид, Constraint на том же грамматическом уровне, что и виды * и #. Оператор уровня вида ~> имеет такое же отношение к приложению уровня типа f a, независимо от того, являются ли задействованные примитивные виды *, # или Constratin. Так, например, дано:

{-# LANGUAGE ConstraintKinds, RankNTypes #-}
type Whatever a = Maybe [a]
type Something a = a => Int

виды Whatever и Something оба выражаются в терминах оператора вида ~> (в GHC записывается просто ->):

λ> :kind Whatever
Whatever :: * -> *
λ> :kind Something
Something :: Constraint -> *
person K. A. Buhr    schedule 19.04.2021