Функции, которые работают только с одним конструктором типа

Question

Я пишу библиотеку для очередей сообщений. Очереди могут быть Direct или же Topic, Direct очереди имеют статический связующий ключ, а Topic очереди могут иметь динамические.

Я хочу написать функцию publish это работает только на Direct Очереди. Это работает:

{-# LANGUAGE DataKinds #-}

type Name = Text
type DirectKey = Text
type TopicKey = [Text]

data QueueType
  = Direct DirectKey
  | Topic TopicKey

data Queue (kind :: a -> QueueType)
  = Queue Name QueueType

Это требует двух отдельных конструкторов

directQueue :: Name -> DirectKey -> Queue 'Direct

topicQueue :: Name -> TopicKey -> Queue 'Topic

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

publish :: Queue 'Direct -> IO ()
publish (Queue name (Direct key)) =
   doSomething name key
publish _ =
   error "should be impossible to get here"

Есть ли лучший способ смоделировать эту проблему, чтобы мне не нужно это сопоставление с образцом? Direct очереди должны всегда иметь это Text метаданные и Topic очереди должны всегда иметь это [Text] метаданные. Есть ли лучший способ обеспечить это как на уровне типа, так и на уровне значений?

Answer 1

Как насчет сделать Queue простой полиморфный тип

data Queue a = Queue Name a

А затем определяя отдельные Queue DirectKey а также Queue TopicKey типы? Тогда вам не нужно было бы сопоставлять паттерны в publish :: Queue DirectKey -> IO (),

Если, кроме этого, вам нужны функции, которые должны работать в любом Queue, возможно, вы могли бы определить некоторые общие операции в классе типов которых DirectKey а также TopicKey будут экземпляры, а затем иметь подписи, такие как

commonFunction :: MyTypeclass a => Queue a -> IO ()

Может быть, вы могли бы поместить такие функции прямо в классе типов

class MyTypeclass a where
    commonFunction :: Queue a -> IO ()

Answer 2

Ваш код не компилируется как есть (требуется PolyKinds быть включенным также), поэтому я не знаю, является ли это просто несчастным случаем, но похоже, что вы пытались пойти на подход, где вы знаете из типа очереди, какие конструкторы могут быть задействованы, и поэтому могут статически гарантировать, что функция может быть вызвана только в определенной очереди.

Фактически, вы можете получить этот подход к работе, используя несколько конструкторов GADT (в отличие от использования нескольких совершенно разных типов, с классом типов для их объединения, когда это необходимо, в подходе, предложенном в ответе @danidiaz').

Но сначала почему ваш текущий код не работает. В вашей очереди введите:

data Queue (kind :: a -> QueueType)
  = Queue Name QueueType

вы параметризуете Queue тип переменной типа (называется kind), позволяя пометить Queue на уровне типа, каким QueueType Вы хотите быть в этом. Но только конструктор Queue Name QueueType не ссылается на kind совсем; это фантомный тип. Тот QueueType слот может быть заполнен любым допустимым типом очереди независимо от того, что kind находится в Queue kind тип очереди.

Это означает, что GHC был прав, когда хотел, чтобы вы добавили дело в publish это будет соответствовать ключу темы внутри Queue 'Direct; ваше определение типа данных говорит, что такие значения могут существовать.

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

Конкретно, мы можем сделать тип для ваших очередей таким, чтобы Queue 'Direct может содержать только прямой тип очереди и Queue 'Topic может содержать только тип очереди темы, и вы можете обработать любой, полиморфно принимая Queue a,

Проще всего сделать QueueType просто использовать для тега и иметь отдельный GADT для хранения данных. В вашем исходном коде вы могли повторно использовать конструкторы хранения данных, поднятые до уровня типа и не примененные, но это делает ваши добрые сигнатуры излишне сложными (что приводит к необходимости PolyKinds), и если вам понадобится добавить больше (и разное количество!) параметров в конструкторы данных, будет все труднее вводить их неприменимые типы в один и тот же тип при поднятии до уровня типа. Так:

data QueueType
  = Direct
  | Topic

data QueueData (a :: QueueType)
  where DirectData :: DirectKey -> QueueData 'Direct
        TopicData :: TopicKey -> QueueData 'Topic

Итак, у нас есть QueueType просто поднять с DataKinds (часто нет необходимости использовать такой тип на уровне значений). Тогда у нас есть тип QueueData параметризованный уровнем типа QueueType, Один конструктор занимает DirectKey и строит QueueData 'Direct, другой занимает TopicKey и строит QueueData 'Topic,

Тогда просто иметь Queue тип, который аналогично помечен с типом представляемой очереди:

data Queue (a :: QueueType)
  = Queue Name (QueueData a)

Теперь, если функция работает в любой очереди (скажем, потому что ей нужен только доступ к имени вне QueueData), это может занять Queue a:

getName :: Queue a -> Text
getName (Queue name _) = name

Вы также можете взять Queue a если вы можете явно обработать все случаи, и вы получите предупреждения, если пропустите случай:

getKeyText :: Queue a -> Text
getKeyText (Queue _ (DirectData key)) = key
getKeyText (Queue _ (TopicData keys)) = mconcat keys

И, наконец, при принятии Queue 'Direct как в вашем publish функция, GHC знает, что DirectData является единственным возможным конструктором для QueueData, Таким образом, вам не нужно добавлять регистр ошибок, как в OP, и он фактически будет обнаружен как ошибка типа, если вы попытаетесь обработать TopicData внутри

Полный пример:

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}

import Data.Text (Text)

type Name = Text
type DirectKey = Text
type TopicKey = [Text]

data QueueType
  = Direct
  | Topic

data QueueData (a :: QueueType)
  where DirectData :: DirectKey -> QueueData 'Direct
        TopicData :: TopicKey -> QueueData 'Topic

data Queue (a :: QueueType)
  = Queue Name (QueueData a)


getName :: Queue a -> Text
getName (Queue name _) = name

getKeyText :: Queue a -> Text
getKeyText (Queue _ (DirectData key)) = key
getKeyText (Queue _ (TopicData keys)) = mconcat keys

publish :: Queue 'Direct -> IO ()
publish (Queue name (DirectData key))
  = doSomething name key
  where doSomething = undefined