Синтаксис продвижения данных

Question

Недавно я обнаружил, что Data.Promotion половина из одиночки.Он имеет множество семейств типов, которые допускают по существу произвольные вычисления на уровне типа.У меня есть пара вопросов об использовании:

1. В чем разница между ($), (%$), ($$), и связаны ли они с :++$, :.$, и т.д.?Действительно ли это инфиксные операторы?Я был под впечатлением все конструкторы инфиксного типа должны были начинаться с :.

2. Я пытаюсь сопоставить конструктор со списком:

   {-# LANGUAGE DataKinds, TypeOperators, PolyKinds #-}
   import Data.Promotion.Prelude
   
   data Foo a b
   type MyList = '[Int, Double, Float]
   
    -- expects one more argument to `Foo`
   type FooList1 b = Map ((Flip Foo) $ b) MyList
   
   -- parse error on the second `b`
   type FooList2 b = Map (($ b) :. Foo) MyList 
   

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

3. Я смог заменить все функции типа, которые я написал, эквивалентными функциями из Data.Promotion кроме этого одного:

   type family ListToConstraint (xs :: [Constraint]) :: Constraint
   type instance ListToConstraint '[] = ()
   type instance ListToConstraint (x ': xs) = (x, ListToConstraint xs)
   

   Есть ли какая-то магия, происходящая с Constraint вид, который предотвратил бы манипулирование им как вложенными парами?

Answer 1

1. Как было объяснено в комментариях, синтаксическое требование к инфиксным функциям на уровне типа, чтобы они начинались с двоеточия, больше не существует.Так что да, все это инфиксные операторы.Никакие два инфиксных оператора автоматически не связаны друг с другом, но библиотека singletons использует некоторые соглашения об именовании внутри, чтобы связать символы, используемые для прекращение функционирования (см. ниже) к их обычным аналогам.

2. Существует целый ряд проблем, возникающих из-за того факта, что семейства типов не могут быть частично применены, но типы данных могут.Вот почему библиотека singletons использует метод, называемый прекращение функционирования:для каждой частично применяемой функции типа она определяет тип данных.Затем существует (очень большое и открытое) семейство типов, называемое Apply это принимает все эти типы данных, которые представляют частично применяемые функции и подходящие аргументы, и выполняет фактическое приложение.

   Разновидностью таких нефункционализированных представлений функций типа является

   TyFun k1 k2 -> *
   

   по разным причинам (кстати, хорошее введение во все это есть в блоге Ричарда Айзенберга "Прекращение функционирования ради победы"), тогда как вид соответствующей функции "нормального" типа был бы

   k1 -> k2
   

   Теперь все функции типа более высокого порядка в синглетонах ожидают нефункционализированных аргументов.Например, вид Map является

   Map :: (TyFun k k1 -> *) -> [k] -> [k1]
   

   и не

   Map :: (k -> k1) -> [k] -> [k1]
   

   Теперь давайте посмотрим на функции, с которыми вы работаете:

   Flip :: (TyFun k (TyFun k1 k2 -> *) -> *) -> k1 -> k -> k2
   

   Первый аргумент - это нефункционализированная функция curried вида k -> k1 -> k2, и это превращает это в обычную функцию типа kind k1 -> k -> k2.

   Также:

   ($) :: (TyFun k1 k -> *) -> k1 -> k
   

   Это всего лишь синоним для Apply Я упоминал выше.

   Теперь давайте посмотрим на ваш пример:

   type FooList1 b = Map ((Flip Foo) $ b) MyList  -- fails
   

   Здесь есть две проблемы:Первый, Foo является типом данных, а не нефункционализированным символом, как Flip ожидает.Второй, Flip является семейством типов и ожидает три аргумента, но предоставляется только один.Мы можем устранить первую проблему, применив TyCon2, который принимает обычный тип данных и превращает его в нефункционализированный символ:

   TyCon2 :: (k -> k1 -> k2) -> TyFun k (TyFun k1 k2 -> *) -> *
   

   Для решения второй задачи нам нужно одно из частичных приложений Flip это синглтоны уже определяют для нас:

   FlipSym0 :: TyFun (TyFun k1 (TyFun k2 k -> *) -> *)
                     (TyFun k2 (TyFun k1 k -> *) -> *)
               -> *
   FlipSym1 ::    (TyFun k1 (TyFun k2 k -> *) -> *)
               -> TyFun k2 (TyFun k1 k -> *) -> *
   
   FlipSym2 ::    (TyFun k1 (TyFun k2 k -> *) -> *)
               -> k2 -> TyFun k1 k -> *
   
   Flip     ::    (TyFun k (TyFun k1 k2 -> *) -> *)
               -> k1 -> k -> k2
   

   Если вы присмотритесь повнимательнее, то FlipSymN требуется ли представительство, если Flip частично применяется к N аргументы, и Flip соответствует воображаемому FlipSym3.В приведенном примере, Flip применяется к одному аргументу, поэтому исправленный пример становится

   type FooList1 b = Map ((FlipSym1 (TyCon2 Foo)) $ b) MyList
   

   И это работает:

   GHCi> :kind! FooList1 Char
   FooList1 Char :: [*]
   = '[Foo Int Char, Foo Double Char, Foo Float Char]
   

   Второй пример аналогичен:

   type FooList2 b = Map (($ b) :. Foo) MyList
   

   Здесь мы сталкиваемся со следующими проблемами:снова, Foo должен быть превращен в нефункционализированный символ с помощью TyCon2;разделы оператора, такие как $ b недоступны на уровне типа, отсюда и ошибка синтаксического анализа.Нам придется использовать Flip снова, но на этот раз FlipSym2, потому что мы применяем его к оператору $ и b.О, но тогда $ частично применяется, поэтому нам нужен символ, соответствующий $ с 0 аргументами.Это доступно в виде $$ в синглетонах (к символьным операторам добавлены нефункционализированные символы $ы).И , наконец ,, :. также частично применяется:он ожидает трех операторов, но получил только двух.Итак, мы идем от :. Для :.$$$ (три доллара, потому что один доллар соответствует 0, а три доллара соответствуют 2).В целом:

   type FooList2 b = Map ((FlipSym2 ($$) b) :.$$$ TyCon2 Foo) MyList
   

   И опять же, это работает:

   GHCi> :kind! FooList2 Char
   FooList2 Char :: [*]
   = '[Foo Int Char, Foo Double Char, Foo Float Char]
   

3. Может быть, я слеп, но я не думаю, что это содержится в синглетонах, которые не так уж сильно касаются Constraints.Тем не менее, это полезная функция.Это в библиотека, над которой я сейчас работаю.Однако она все еще незакончена и в основном недокументирована, вот почему я ее еще не выпустил.