Типы, зависящие от пути в Haskell

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

Точнее, представьте, что у вас есть тип для представления таблицы в базе данных, связанной с каким-то типом:

type Table a = ...

и вы можете извлечь столбцы таблицы вместе с типом столбца:

type Column col = ...

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

extractCol :: Table Frog -> Column Weight

Вот вопрос: я хотел бы отличить начало столбцов, чтобы пользователи не могли выполнять операции между таблицами. Например:

bullfrogTable = undefined :: Table Frog
toadTable = undefined :: Table Frog
bullfrogWeights = extractCol bullfrogTable
toadWeights = extractCol toadTable
-- Or some other columns from the toad table
toadWeights' = extractCol toadTable
-- This should compile
addWeights toadWeights' toadWeights
-- This should trigger a type error
addWeights bullfrogWeights toadWeights

Я знаю, как достичь этого в Scala (используя типы, зависящие от пути, см. [1]), и я думал о 3 вариантах в Haskell:

не использует типы и просто выполняет проверку во время выполнения (текущее решение)
расширение TypeInType для добавления типа phantom в тип таблицы и передать этот дополнительный тип в столбцы. Я не заинтересован в этом, потому что построение такого типа будет очень сложным (таблицы генерируются с помощью сложных операций DAG) и, вероятно, медленнее компилировать в этом контексте.
обертывание операций с использованием конструкции forall, аналогичной ST-монаде, но в моем случае я бы хотел, чтобы дополнительный тип тегов фактически удалял конструкцию.

Я рад, что у меня очень ограниченная область видимости для построения тех же столбцов (т.е. столбцы из table и (id table) не смешиваются), и я в основном забочусь о смысле DSL API, а не безопасность.

[1] Что подразумевается под Scala зависимыми от пути типами?

Мое текущее решение

Вот что я сделал, используя RankNTypes.

Я все еще хочу дать пользователям возможность использовать столбцы, как они сочтут нужным, без каких-либо сильных проверок типов, и выбрать, хотят ли они каких-то более сильных гарантий типа: это DSL для ученых-данных, которые не будут знать о силе сторона Haskell

Таблицы по-прежнему помечены их содержимым:

type Table a = ...

и столбцы теперь помечены некоторыми дополнительными ссылочными типами, поверх типа данных, которые они содержат:

type Column ref col = ...

Проецирования из таблиц в столбцы либо помечены, либо не отмечены. На практике это скрывается за линзоподобным DSL.

extractCol :: Table Frog -> Column Frog Weight

data TaggedTable ref a = TaggedTable { _ttTable :: Table a }

extractColTagged :: Table ref Frog -> Column ref Weight

withTag :: Table a -> (forall ref. TaggedTable ref a -> b) -> b
withTag tb f = f (TaggedTable tb)

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

let doubleToadWeights = withTag toadTable $ \ttoadTable ->
  let toadWeights = extractColTagged ttoadTable in
    addWeights toadWeights toadWeights

и это не будет скомпилировано по желанию:

let doubleToadWeights =
  toadTable `withTag` \ttoads ->
     bullfrogTable `withTag` \tbullfrogs ->
       let toadWeights = extractColTagged ttoads
           bullfrogWeights = extractColTagged tbullfrogs
       in addWeights toadWeights bullfrogWeights -- Type error

С точки зрения DSL, я считаю, что это не так просто, как то, что можно было бы достичь с помощью Scala, но сообщение об ошибке типа понятно, что имеет первостепенное значение для меня.

Ответ 1