Понимание этого определения HList

Question

Я относительно новичок в Haskell и пытаюсь понять одно из определений HList.

data instance HList '[] = HNil
newtype instance HList (x ': xs) = HCons1 (x, HList xs)
pattern HCons x xs = HCons1 (x, xs)

У меня есть пара конкретных вопросов:

• Что '[] а также (x ': xs) синтаксис я вижу? Похоже, что это сопоставление с образцом для параметров типа variadic, но я никогда раньше не видел этот синтаксис, и я не знаком с параметрами типа variadic в Haskell. Я предполагаю, что это является частью семейства типов GHC, но я ничего не вижу об этом на связанной странице, и довольно сложно найти синтаксис в Google.

• Есть ли смысл использовать newtype объявление с кортежем (вместо data объявление с двумя полями) кроме того, чтобы избежать бокса HCons1?

Answer 1

Во-первых, вам не хватает части определения: data family сама декларация.

data family HList (l :: [*])
data instance HList '[] = HNil
newtype instance HList (x ': xs) = HCons1 (x, HList xs)

Это называется data family (доступно под TypeFamilies расширение).

pattern HCons x xs = HCons1 (x, xs)

Это двунаправленный шаблон (доступен под PatternSynonyms расширение).

Что '[] а также (x ': xs) синтаксис я вижу?

Когда ты видишь ' знаки перед конструкторами, это означает их продвинутые аналоги уровня типа. В качестве синтаксического удобства продвигаемым спискам и кортежам также просто нужна дополнительная галочка (и мы все еще можем писать '[] для пустого списка уровня типа и ': для типового уровня минусы. Все это доступно через DataKinds расширение.

Есть ли смысл использовать newtype объявление с кортежем (вместо объявления данных с двумя полями), кроме того, чтобы избежать бокса HCons1?

Да, чтобы убедиться, что HList имеет представительскую роль, что означает, что вы можете принуждать HList с ¹. Это слишком сложно, чтобы объяснить просто ответом, но вот пример того, как все идет не так, как мы хотим, когда у нас есть

 data instance HList (x ': xs) = HCons x (HList xs)

вместо newtype instance (и без рисунка). Рассмотрим следующее newtype s, которые в представительстве эквивалентны Int, Bool, а также () соответственно

newtype MyInt = MyInt Int
newtype MyBool = MyBool Bool
newtype MyUnit = MyUnit ()

Напомним, мы можем использовать coerce обернуть или развернуть эти типы автоматически. Ну, мы бы хотели сделать то же самое, но в целом HList:

ghci> l  = (HCons 3 (HCons True (HCons () HNil))) :: HList '[Int,   Bool,   ()]
ghci> l' = coerce l                               :: HList '[MyInt, MyBool, MyUnit]

Это работает с newtype instance вариант, но не тот data instance один из-за ролей. (Подробнее об этом здесь.)

---

¹ технически, для data family в целом: роли могут быть разными для каждого instance / newtype - здесь нам действительно нужно только HCons случай, чтобы быть представительным, так как это тот, который подвергается принуждению. Проверьте этот билет Trac.

Answer 2

'[] а также (x ': xs) являются синтаксисом для списков уровня типа в том смысле, что DataKinds расширение языка позволяет продвигать типы к видам и конструкторы к типам; т.е. если k какой-то '[k] тоже своего рода, и '[] это тип вида '[k], и если t :: k а также ts :: '[k], затем t ': ts :: '[k], Все сдвигается на один.

Так в HList (x ': xs), x а также xs соответствуют два типа: x соответствует "нормальному" типу вида * (например Int) а также xs соответствует другому списку типов '[*], Правая часть определяет (newtype) тип данных, который имеет конструктор HCons1 с параметром типа (x, HList xs),

В качестве примера мы можем иметь

HCons1 (1, HCons1 (True, HNil)) :: HList '[Int, Bool]

Или, используя синоним шаблона:

1 `HCons` True `HCons` HNil :: HList '[Int, Bool]

У меня нет хорошего ответа на ваш второй вопрос о том, почему он представлен как новый тип с кортежем.