Fonctions qui ne fonctionnent qu'avec un constructeur d'un type

Question

J'écris une lib pour les files d'attente de messages. Les files d'attente peuvent être Direct ou Topic. Les files d'attente Direct ont une clé de liaison statique, tandis que les files d'attente Topic peuvent avoir des files d'attente dynamiques. Je veux écrire une fonction publish qui ne fonctionne que sur les files d'attente Direct. Cela fonctionne:

{-# 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 

Cela nécessite deux constructeurs distincts

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

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

Mais quand je vais écrire publier, il y a un modèle supplémentaire que je dois correspondre à ce qui devrait être impossible

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

Existe-t-il une meilleure façon de modéliser ce problème afin que je n'aie pas besoin de ce modèle? Les files d'attente Direct doivent toujours avoir les métadonnées Text et les files d'attente Topic doivent toujours contenir les métadonnées [Text]. Existe-t-il une meilleure façon de faire respecter ce principe au niveau du type et de la valeur?

Answer 1

Que diriez-vous faire Queue un type polymorphes plaine

data Queue a = Queue Name a 

Et puis définir Queue DirectKey et Queue TopicKey distincts types? Ensuite, vous n'auriez pas besoin de faire correspondre le modèle dans publish :: Queue DirectKey -> IO().

Si, à part cela, vous avez besoin des fonctions qui devraient fonctionner dans tous les Queue, peut-être vous pouvez définir certaines opérations communes dans une classe de types dont DirectKey et TopicKey aurait des cas, et des signatures comme

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

peut-être que vous pourriez mettre ces fonctions directement dans la classe de types

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

Answer 2

Votre code ne compile pas-est (il faut PolyKinds être activée aussi bien), donc je ne kno w si c'est seulement un accident, mais on dirait que vous essayez d'aller vers l'approche où vous savez à partir du type d'une file d'attente où les constructeurs pourraient être impliqués, et donc statiquement garantir qu'une fonction ne peut être appelée que sur un certain type de la file d'attente.

Vous pouvez en fait obtenir cette approche à travailler, en utilisant plusieurs constructeurs d'un GADT (par opposition à l'utilisation de plusieurs types complètement séparés, avec une classe de type pour les rassembler si nécessaire, dans l'approche suggérée dans @danidiaz 'réponse).

Mais d'abord pourquoi votre code actuel ne fonctionne pas. Dans le type de file d'attente:

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

vous paramétrer le type Queue par une variable de type (appelé kind), ce qui vous permet de marquer un Queue au niveau du type de ce genre de QueueType vous voulez être dedans. Mais seul le constructeur Queue Name QueueType ne fait aucune référence à kind du tout; C'est un type fantôme. Cet emplacement QueueType peut être rempli par tout type de file d'attente valide, quel que soit le type kind dans le type Queue kind de la file d'attente.

Cela signifie que GHC a eu raison de vouloir que vous ajoutiez un cas à publish qui correspondrait à une clé de rubrique à l'intérieur d'un Queue 'Direct; votre définition de type de données indique que de telles valeurs peuvent exister.

Ce que GADT vous permet de faire est de déclarer explicitement le type complet de chaque constructeur séparément, incluant le type de retour. Vous pouvez donc établir une relation entre le type de la valeur que vous construisez et les constructeurs (ou leurs paramètres) qui pourraient éventuellement être utilisés pour faire une valeur de ce type.

En termes concrets, nous pouvons faire un type pour vos files d'attente telles que Queue 'Direct peut que contiennent un type de file d'attente directe et Queue 'Topic peut que contiennent un type de file d'attente de sujet, et vous pouvez gérer soit en acceptant polymorphically une Queue a.

Il est plus simple de faire QueueTypejuste être utilisé pour l'étiquette, et avoir un GADT séparé stocker les données. Dans votre code d'origine, vous étiez en mesure de réutiliser les constructeurs de données levés au niveau du type et non appliqués, mais cela rend vos signatures aimables inutilement compliquées (nécessitant PolyKinds), et si vous avez besoin d'ajouter plus (et différents numéros de!) paramètres aux constructeurs de données, il deviendra de plus en plus difficile d'adapter leurs types non appliqués pour qu'ils correspondent au même type lorsqu'ils sont levés au niveau du type. Alors:

data QueueType 
    = Direct 
    | Topic 

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

Nous avons donc QueueType juste pour soulever avec DataKinds (il n'y a souvent pas besoin de jamais réellement utiliser un tel type au niveau de la valeur). Ensuite, nous avons le type QueueData paramétré par un niveau de type QueueType. Un constructeur prend un DirectKey et construit un QueueData 'Direct, l'autre prend un TopicKey et construit un QueueData 'Topic.

Ensuite, il est simple d'avoir un type Queue qui est tout aussi marqué avec le type de file d'attente étant représenté:

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

Maintenant, si une fonction fonctionne sur une file d'attente (par exemple parce qu'il a besoin que l'accès au nom en dehors de la QueueData), il peut prendre un Queue a: si vous pouvez gérer explicitement tous les cas

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

vous pouvez également prendre un Queue a, et vous obtiendrez des avertissements quand y ous manquez un cas:

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

Et enfin, en prenant une Queue 'Direct comme dans votre fonction publish, GHC sait que DirectData est le seul constructeur possible pour le QueueData. Vous n'avez donc pas besoin d'ajouter un cas d'erreur comme dans l'OP, et il serait en fait détecté comme une erreur de type si vous essayez de gérer un TopicData à l'intérieur.

Exemple complet:

{-# 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