Tester si une valeur correspond à un constructeur

Question

Disons que j'ai un type de données comme ceci :

data NumCol = Empty |
              Single Int |
              Pair Int Int |
              Lots [Int]

Maintenant, je souhaite filtrer les éléments qui correspondent à un constructeur donné à partir d'un fichier de type [NumCol] . Je peux l'écrire pour, disons, Pair :

get_pairs :: [NumCol] -> [NumCol]
get_pairs = filter is_pair
    where is_pair (Pair _ _) = True
          is_pair _ = False

Cela fonctionne, mais ce n'est pas générique. Je dois écrire une fonction séparée pour is_single , is_lots etc.

J'aimerais plutôt pouvoir écrire :

get_pairs = filter (== Pair)

Mais cela ne fonctionne que pour les constructeurs de type qui ne prennent pas d'arguments (c.-à-d. Empty ).

La question est donc la suivante : comment puis-je écrire une fonction qui prend une valeur et un constructeur, et qui renvoie si la valeur correspond au constructeur ?

Answer 1

Au moins get_pairs lui-même peut être défini relativement simplement en utilisant une compréhension de liste pour filtrer à la place :

get_pairs xs = [x | x@Pair {} <- xs]

Pour une solution plus générale de mise en correspondance des constructeurs, vous pouvez utiliser les prismes de l'outil d'évaluation de la qualité de l'eau. lens paquet :

{-# LANGUAGE TemplateHaskell #-}

import Control.Lens
import Control.Lens.Extras (is)

data NumCol = Empty |
              Single Int |
              Pair Int Int |
              Lots [Int]

-- Uses Template Haskell to create the Prisms _Empty, _Single, _Pair and _Lots
-- corresponding to your constructors
makePrisms ''NumCol

get_pairs :: [NumCol] -> [NumCol]
get_pairs = filter (is _Pair)

Answer 2

Les étiquettes des syndicats étiquetés devraient être des valeurs de premier ordre, et avec un peu d'effort, elles le sont.

Alerte à la pyromanie :

{-# LANGUAGE GADTs, DataKinds, KindSignatures,
    TypeFamilies, PolyKinds, FlexibleInstances,
    PatternSynonyms
#-}

Première étape : définir des versions des balises au niveau du type.

data TagType = EmptyTag | SingleTag | PairTag | LotsTag

Deuxième étape : définir des témoins de niveau valeur pour la représentabilité des balises de niveau type. La bibliothèque Singletons de Richard Eisenberg le fera pour vous. Je veux dire quelque chose comme ça :

data Tag :: TagType -> * where
  EmptyT   :: Tag EmptyTag
  SingleT  :: Tag SingleTag
  PairT    :: Tag PairTag
  LotsT    :: Tag LotsTag

Et maintenant, nous pouvons dire quelles sont les choses que nous nous attendons à trouver associées à un tag donné.

type family Stuff (t :: TagType) :: * where
  Stuff EmptyTag   = ()
  Stuff SingleTag  = Int
  Stuff PairTag    = (Int, Int)
  Stuff LotsTag    = [Int]

Nous pouvons donc refactoriser le type auquel vous avez d'abord pensé

data NumCol :: * where
  (:&) :: Tag t -> Stuff t -> NumCol

et utiliser PatternSynonyms pour retrouver le comportement que vous aviez en tête :

pattern Empty        = EmptyT   :&  ()
pattern Single  i    = SingleT  :&  i
pattern Pair    i j  = PairT    :&  (i, j)
pattern Lots    is   = LotsT    :&  is

Donc ce qui s'est passé c'est que chaque constructeur pour NumCol s'est transformée en une balise indexée par le type de balise à laquelle elle correspond. En d'autres termes, les balises de constructeur sont maintenant séparées du reste des données, synchronisées par un index commun qui garantit que les éléments associés à une balise correspondent à la balise elle-même.

Mais nous pouvons parler uniquement des étiquettes.

data Ex :: (k -> *) -> * where  -- wish I could say newtype here
  Witness :: p x -> Ex p

Maintenant, Ex Tag est le type de "balises d'exécution avec une contrepartie au niveau du type". Elle possède un Eq instance

instance Eq (Ex Tag) where
  Witness EmptyT   ==  Witness EmptyT   = True
  Witness SingleT  ==  Witness SingleT  = True
  Witness PairT    ==  Witness PairT    = True
  Witness LotsT    ==  Witness LotsT    = True
  _                ==  _                = False

De plus, nous pouvons facilement extraire la balise d'une NumCol .

numColTag :: NumCol -> Ex Tag
numColTag (n :& _) = Witness n

Et cela nous permet de répondre à votre cahier des charges.

filter ((Witness PairT ==) . numColTag) :: [NumCol] -> [NumCol]

Ce qui soulève la question de savoir si votre spécification correspond réellement à ce dont vous avez besoin. Le fait est que la détection d'une balise vous donne le droit de vous attendre à ce que cette balise soit utilisée. Le type de sortie [NumCol] ne rend pas justice au fait que vous savez que vous avez les bonnes paires.

Comment pouvez-vous resserrer le type de votre fonction et continuer à la fournir ?

Answer 3

Une approche consiste à utiliser DataTypeable y el Data.Data module. Cette approche s'appuie sur deux instances de classe de type générées automatiquement qui transportent les métadonnées sur le type pour vous : Typeable y Data . Vous pouvez les dériver avec {-# LANGUAGE DeriveDataTypeable #-} :

data NumCol = Empty |
          Single Int |
          Pair Int Int |
          Lots [Int] deriving (Typeable, Data)

Maintenant, nous avons un toConstr qui, étant donné une valeur, nous donne une représentation de son constructeur :

toConstr :: Data a => a -> Constr

Ainsi, il est facile de comparer deux termes juste par leurs constructeurs. Le seul problème restant est que nous avons besoin d'une valeur à laquelle comparer lorsque nous définissons notre prédicat ! Nous pouvons toujours créer une valeur fictive à l'aide de la commande undefined mais c'est un peu moche :

is_pair x = toConstr x == toConstr (Pair undefined undefined)

La dernière chose que nous allons faire est de définir une petite classe pratique qui automatise cela. L'idée de base est d'appeler toConstr sur des valeurs qui ne sont pas des fonctions et de récursion sur les fonctions en passant d'abord en undefined .

class Constrable a where
  constr :: a -> Constr

instance Data a => Constrable a where
  constr = toConstr

instance Constrable a => Constrable (b -> a) where
  constr f = constr (f undefined)

Cela repose sur FlexibleInstance , OverlappingInstances y UndecidableInstances Il est donc possible que ce soit un peu diabolique, mais, en utilisant le (in)célèbre théorème du globe oculaire, cela devrait aller. Sauf si vous ajoutez d'autres instances ou si vous essayez de l'utiliser avec quelque chose qui n'est pas un constructeur. Dans ce cas, ça pourrait exploser. Violemment. Pas de promesses.

Enfin, le mal étant bien contenu, nous pouvons écrire un opérateur "égal par constructeur" :

(=|=) :: (Data a, Constrable b) => a -> b -> Bool
e =|= c = toConstr e == constr c

(Le =|= est un peu un moyen mnémotechnique, parce que les constructeurs sont syntaxiquement définis avec une balise | .)

Maintenant, vous pouvez écrire presque exactement ce que vous vouliez !

filter (=|= Pair)

De plus, vous voudrez peut-être désactiver la restriction du monomorphisme. En fait, voici la liste des extensions que j'ai activées et que vous pouvez simplement utiliser :

{-# LANGUAGE DeriveDataTypeable, FlexibleInstances, NoMonomorphismRestriction, OverlappingInstances, UndecidableInstances #-}

Oui, c'est beaucoup. Mais c'est ce que je suis prêt à sacrifier pour la cause. De ne pas écrire de supplément undefined s.

Honnêtement, si ça ne te dérange pas de compter sur lens (mais bon sang, cette dépendance est un problème), vous devriez simplement adopter l'approche du prisme. La seule chose qui recommande la mienne est que vous pouvez utiliser l'amusant nommé Data.Data.Data classe.