Семейства данных против семейств инъекционных типов

Теперь, когда у нас есть инъективные типы семейств, существует ли другой вариант использования семейств данных над семействами типов?

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

Глядя на docs на семейства данных, я вижу, что причина не переписывать все виды использования семейств данных с помощью семейства инъективных типов.

Например, скажем, у меня есть семейство данных (я объединил некоторые примеры из документов, чтобы попытаться сжать все функции семейств данных)

data family G a b
data instance G Int Bool = G11 Int | G12 Bool deriving (Eq)
newtype instance G () a = G21 a
data instance G [a] b where
   G31 :: c -> G [Int] b
   G32 :: G [a] Bool

Я мог бы также переписать его как

type family G a b = g | g -> a b
type instance G Int Bool = G_Int_Bool
type instance G () a = G_Unit_a a
type instance G [a] b = G_lal_b a b

data G_Int_Bool = G11 Int | G12 Bool  deriving (Eq)
newtype G_Unit_a a = G21 a
data G_lal_b a b where
   G31 :: c -> G_lal_b [Int] b
   G32 :: G_lal_b [a] Bool

Само собой разумеется, что связанные экземпляры для семейств данных соответствуют соответствующим экземплярам с семействами типов одинаковым образом. Тогда единственная оставшаяся разница в том, что в пространстве имен типов меньше объектов?

В качестве продолжения, есть ли какая-либо польза от того, что в пространстве имен типов меньше вещей? Все, что я могу придумать, это то, что это станет отладочным адом для тех, кто играет с этим на ghci - типы конструкторов все, кажется, указывают на то, что все конструкторы находятся под одним GADT...

Ответы

Ответ 1

type family T a = r | r -> a
data family D a

Семейство инъективных типов T удовлетворяет аксиоме инъективности

если T a ~ T b, тогда a ~ b

Но семейство данных удовлетворяет гораздо более сильной аксиоме рождаемости

если D a ~ g b, затем D ~ g и a ~ b

(Если вам нравится: поскольку экземпляры D определяют новые типы, отличные от любых существующих типов.)

Фактически D сам по себе является законным типом в системе типов, в отличие от семейства типов, такого как T, который может появляться только в полностью насыщенном приложении, таком как T a. Это означает

D может быть аргументом для другого конструктора типов, например MaybeT D. (MaybeT T является незаконным.)
Вы можете определить экземпляры для D, например instance Functor D. (Вы не можете определить экземпляры для семейства типов Functor T, и это было бы непригодным для использования, поскольку выбор экземпляра, например, map :: Functor f => (a -> b) -> f a -> f b, основан на том, что из типа f a вы можете определить как f, так и a, так как для работы f не разрешается изменять типы семейств типов, даже инъективных.)

Ответ 2

Вам не хватает еще одной детали - семейства данных создают новые типы. Типы семей могут ссылаться только на другие типы. В частности, каждый экземпляр семейства данных объявляет новые конструкторы. И это красиво родовое. Вы можете создать экземпляр данных с помощью newtype instance, если хотите семантику newtype. Ваш экземпляр может быть записью. Он может иметь несколько конструкторов. Это может быть даже GADT, если вы хотите.

Именно различие между ключевыми словами type и data/newtype. Семейства инъекционных типов не дают вам новых типов, что делает их бесполезными в случае, когда вам это нужно.

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

Я хотел написать api для работы с изменяемыми ячейками в нескольких разных контекстах без использования классов. Я знал, что хочу сделать это со свободной монадой с переводчиками в IO, ST и, возможно, с некоторыми ужасными хаками с unsafeCoerce, даже до тех пор, пока он не запустит его в State. Конечно, это было не для какой-либо практической цели - я просто изучал дизайн API.

Итак, у меня было что-то вроде этого:

data MutableEnv (s :: k) a ...

newRef :: a -> MutableEnv s (Ref s a)
readRef :: Ref s a -> MutableEnv s a
writeRef :: Ref s a -> a -> MutableEnv s ()

Определение MutableEnv не было важно. Просто стандартный бесплатный/операционный материал монады с конструкторами, соответствующими трем функциям в api.

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

Тогда поздно ночью я вышел на прогулку, и это ударило меня - то, что я по существу хочу, это тип, конструкторы которого индексируются типом аргумента. Но это должно было быть открытым, в отличие от GADT - новые переводчики могли бы быть добавлены по своему усмотрению. И тут меня осенило. Именно это и есть семейство данных. Открытое, индексированное по типу семейство значений данных. Я мог бы завершить api следующим образом:

data family Ref (s :: k) :: * -> *

Тогда обращение к базовому представлению для Ref не имело большого значения. Просто создайте экземпляр данных (или экземпляр newtype, скорее), когда будет определен интерпретатор для MutableEnv.

Этот точный пример не очень полезен. Но это наглядно иллюстрирует то, что семейства данных могут делать, что семейства инъективных типов не могут.

Ответ 3

Ответ Рида Бартона объясняет различие между двумя моими примерами. Это напомнило мне что-то, что я прочитал в Ричарде Айзенберге thesis о добавлении зависимых типов к Haskell, и я подумал, что, поскольку суть этого вопроса это инъективность и генерируемость, стоит упомянуть, как DependentHaskell будет иметь дело с этим (когда он в конечном итоге будет реализован, и если предлагаемые в настоящее время кванторы являются последними).

Далее следуют страницы 56 и 57 (4.3.4 Совместимость) вышеупомянутого thesis:

Определение (Generativity) . Если f и g являются генеративными, то f a ~ g b подразумевает f ~ g

Определение (Инъективность) . Если f является инъективным, то f a ~ f b подразумевает a ~ b

Определение (соответствие) . Функция f сопоставима, если она является генеративной и инъективной

В Haskell, как мы это знаем сейчас (8.0.1), сопоставимые (тип-уровни) функции состоят именно из конструкторов типа newtype, data и data family. В будущем в DependentHaskell один из новых кванторов, который мы получим, будет '->, и это будет использоваться для обозначения совместимых функций. Другими словами, будет возможность сообщить компилятору, что функция уровня типа является генеративной (которая в настоящее время может быть выполнена только при условии, что функция является конструктором типа).