Je crée de nombreux pipelines de traitement de données à l'aide de données de spectrométrie de masse, où les données de l'instrument sont nettoyées, transformées, mises à l'échelle, inspectées et enfin analysées. J'ai tendance à utiliser une définition de type récursive pour cela - voici un exemple fortement simplifié:

data Dataset = Initial { x::(Vector Double), y::(Vector Double) name::String}
             | Cleaned { x::(Vector Double), y::(Vector Double) name::String}
             | Transformed { x::(Vector Double), y::(Vector Double) name::String}

Ensuite, un pipeline typique sera simplement une chaîne de fonctions qui commence par un créateur Dataset, puis continue avec des fonctions qui consomment quelque chose de type Dataset, et produisent quelque chose de type Dataset:

createDataset :: Vector Double -> Vector Double -> String -> Dataset
createDataset x y name = Initial x y name

removeOutliers :: Dataset -> Dataset
removeOutliers (Initial x y n) = let
                         (new_x, new_y) = outlierRemovalFunction x y
                         in Cleaned new_x new_y (n ++"_outliersRemoved")
               (Cleaned x y n) = error "Already been cleaned"
               (Scaled x y n) = error "Scaled data should have already been cleaned"
               (Transformed x y n) = error "Transformed data should have already been cleaned"

logTransform :: Dataset -> Dataset
logTransform (Initial x y n) = error "Need to clean first"
             (Cleaned x y n) = let
                         (new_x, new_y) = logTransformFunction x y
                         in Transformed new_x new_y (n ++ "_logTransformed)


Cela garantit que les étapes de traitement du pipeline se déroulent dans le bon ordre et vous pouvez créer des pipelines entiers à l'aide de la composition

(logTransform . removeOutliers . createDataset) init_y init_y "ourData"

Mais cette approche semble extrêmement limitée pour plusieurs raisons. La première raison est que l'incorrection est détectée via la correspondance de modèles sur les constructeurs, donc les ajouts et les modifications au pipeline nécessiteront des changements partout dans la correspondance de modèles. Imaginez un exemple plus compliqué avec plusieurs étapes de nettoyage et de transformation - en gros, chaque combinaison possible aura besoin de son propre constructeur unique, et toutes les correspondances de motifs devront être non exhaustives, ou répétées absolument partout.

La deuxième raison pour laquelle cela semble limité est qu'un pipeline mal construit n'est détecté que par des échecs à l'exécution. J'ai séquencé toutes les étapes de traitement, donc à chaque étape du pipeline, je sais exactement ce qui est arrivé aux données. Le système de type devrait être en mesure de m'empêcher d'assembler les étapes de manière incorrecte en premier lieu, et l'utilisation d'une fonction s'attendant à des données nettoyées sur une entrée non nettoyée devrait être détectable au moment de la compilation.

J'ai pensé à avoir des types séparés pour chacune des étapes du pipeline, puis à implémenter l'interface "dataset" en tant que classe de type, quelque chose comme:

class Dataset a where
    x :: a -> Vector Double
    y :: a -> Vector Double
    name :: a -> String

data Initial = Initial x y name
instance Dataset Initial where ...

data Cleaned a = Cleaned a
instance Dataset Cleaned where ...

data Transformed a = Transformed a
instance Dataset Transformed where ...

Alors vous pouvez faire des choses (je pense ...) comme:


removeOutliers :: (Dataset a) => a -> Cleaned a
removeOutliers = ...

logTransform :: (Dataset a) => Cleaned a -> Transformed Cleaned a
logTransform = ...

Je pense que cette approche résout le problème numéro 1 ci-dessus: nous pouvons maintenant détecter les erreurs de pipeline au moment de la compilation, et nous ne sommes plus obligés d'avoir tous ces différents constructeurs pour décrire les étapes de traitement.

Cependant, il semble que je viens de déplacer le problème "d'un niveau vers le haut". Je traite maintenant des variables de type et de tous ces types imbriqués. Au lieu d'avoir besoin d'un constructeur Dataset pour chaque combinaison possible d'étapes de pipeline, je dois maintenant créer une instance Dataset pour chaque combinaison de types!

Ce que je veux vraiment, c'est un moyen pour un type dans le pipeline de traitement d'être à la fois très spécifique ou très général dans ses contraintes. J'aimerais utiliser des types / contraintes qui détaillent l'ordre dans lequel des étapes de traitement spécifiques ont été appliquées, mais j'aimerais également qu'un type / contrainte puisse transmettre quelque chose de plus général - c'est-à-dire "En plus d'autres étapes sans importance , la suppression des valeurs aberrantes a été effectuée ". Donc, fondamentalement, le type de choses qui ont fait supprimer les valeurs aberrantes.

La transmission des informations de commande serait un ultra-bonus - "En plus d'autres étapes sans importance, la suppression des valeurs aberrantes s'est produite et à un moment donné plus tard une transformation de journal s'est produite". Le type d'éléments pour lesquels les valeurs aberrantes ont été supprimées avant d'être transformées dans le journal (et pas nécessairement immédiatement avant).

Est-ce que ce genre de chose est possible en utilisant le système de types de Haskell?

7
Matt 31 août 2020 à 19:13

2 réponses

Meilleure réponse

Oui, le système de type Haskell moderne peut gérer cela. Cependant, par rapport à la programmation habituelle au niveau du terme, la programmation au niveau du type dans Haskell est toujours difficile. La syntaxe et les techniques sont compliquées et la documentation fait quelque peu défaut. Il a également tendance à être le cas que des modifications relativement petites des exigences peuvent conduire à de grands changements dans l'implémentation (c'est-à-dire que l'ajout d'une nouvelle «fonctionnalité» à votre implémentation peut se transformer en une réorganisation majeure de tous les types), ce qui peut rendre la tâche difficile pour trouver une solution si vous n'êtes toujours pas sûr de vos besoins.

Le commentaire de @ JonPurdy et la réponse de @ AtnNn donnent quelques idées de ce qui est possible. Voici une solution qui tente de répondre à vos besoins spécifiques. Cependant, il est susceptible de s'avérer difficile à utiliser (ou du moins difficile à adapter à vos besoins) à moins que vous ne soyez prêt à vous asseoir et à vous apprendre un peu de programmation de type type.

Quoi qu'il en soit, supposons que vous souhaitiez baliser une structure de données fixe (c'est-à-dire toujours les mêmes champs avec les mêmes types) avec une liste au niveau du type des processus qui ont été exécutés dessus, avec un moyen de vérifier la liste de processus par rapport une sous-liste ordonnée des processus requis.

Nous aurons besoin de quelques extensions:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

Les balises de processus elles-mêmes sont définies comme des constructeurs dans un type de somme, avec l'extension DataKinds faisant passer les balises du niveau du terme au niveau du type:

data Process = Cleaned | Transformed | Scaled | Inspected | Analyzed

La structure de données est ensuite balisée avec une liste de processus appliqués, son "pipeline":

data Dataset (pipeline :: [Process])
  = Dataset { x :: [Double]
            , y :: [Double]
            , name :: String }

REMARQUE: Il sera plus pratique que le pipeline soit dans l'ordre inverse, avec le plus récent Process appliqué en premier.

Pour nous permettre d'exiger qu'un pipeline ait une sous-séquence ordonnée particulière de processus, nous avons besoin d'une fonction au niveau du type (c'est-à-dire, une famille de types) qui vérifie les sous-séquences. Voici une version:

type family a || b where
  True  || b = True
  False || b = b

type family Subseq xs ys where
  Subseq '[]      ys  = True
  Subseq nonempty '[] = False
  Subseq (x:xs) (x:ys) = Subseq xs ys || Subseq (x:xs) ys
  Subseq xs     (y:ys) = Subseq xs ys

Nous pouvons tester cette fonction au niveau du type dans GHCi:

λ> :kind! Subseq '[Inspected, Transformed] '[Analyzed, Inspected, Transformed, Cleaned]
Subseq '[Inspected, Transformed] '[Analyzed, Inspected, Transformed, Cleaned] :: Bool
= 'True
λ> :kind! Subseq '[Inspected, Transformed] '[Analyzed, Transformed, Cleaned]
Subseq '[Inspected, Transformed] '[Analyzed, Transformed, Cleaned] :: Bool
= 'False
λ> :kind! Subseq '[Inspected, Transformed] '[Transformed, Inspected]
Subseq '[Inspected, Transformed] '[Transformed, Inspected] :: Bool
= 'False

Si vous souhaitez écrire une fonction qui nécessite qu'un ensemble de données ait été transformé puis nettoyé des valeurs aberrantes (dans cet ordre), éventuellement mélangé avec d'autres étapes sans importance avec la fonction elle-même appliquant une étape de mise à l'échelle, alors la signature ressemblera à ceci:

-- remember: pipeline type is in reverse order
foo1 :: (Subseq [Cleaned, Transformed] pipeline ~ True)
     => Dataset pipeline -> Dataset (Scaled : pipeline)
foo1 = undefined

Si vous souhaitez éviter la double mise à l'échelle, vous pouvez introduire une autre fonction au niveau du type:

type family Member x xs where
  Member x '[] = 'False
  Member x (x:xs) = 'True
  Member x (y:xs) = Member x xs

Et ajoutez une autre contrainte:

foo2 :: ( Subseq [Cleaned, Transformed] pipeline ~ True
        , Member Scaled pipeline ~ False)
     => Dataset pipeline -> Dataset (Scaled : pipeline)
foo2 = undefined

Alors:

> foo2 (Dataset [] [] "x" :: Dataset '[Transformed])
... Couldn't match type ‘'False’ with ‘'True’ ...
> foo2 (Dataset [] [] "x" :: Dataset '[Cleaned, Scaled, Transformed])
... Couldn't match type ‘'False’ with ‘'True’ ...
> foo2 (Dataset [] [] "x" :: Dataset '[Cleaned, Transformed])
-- typechecks okay
foo2 (Dataset [] [] "x" :: Dataset '[Cleaned, Transformed])
  :: Dataset '[ 'Scaled, 'Cleaned, 'Transformed]

Vous pouvez rendre tout cela un peu plus convivial, à la fois en termes de syntaxe de contrainte et de messages d'erreur, avec quelques alias de type et familles de types supplémentaires:

import Data.Kind
import GHC.TypeLits

type Require procs pipeline = Require1 (Subseq procs pipeline) procs pipeline
type family Require1 b procs pipeline :: Constraint where
  Require1 True procs pipeline = ()
  Require1 False procs pipeline
    = TypeError (Text "The pipeline " :<>: ShowType pipeline :<>:
                 Text " lacks required processing " :<>: ShowType procs)
type Forbid proc pipeline = Forbid1 (Member proc pipeline) proc pipeline
type family Forbid1 b proc pipeline :: Constraint where
  Forbid1 False proc pipeline = ()
  Forbid1 True proc pipeline
    = TypeError (Text "The pipeline " :<>: ShowType pipeline :<>:
                 Text " must not include " :<>: ShowType proc)

foo3 :: (Require [Cleaned, Transformed] pipeline, Forbid Scaled pipeline)
     => Dataset pipeline -> Dataset (Scaled : pipeline)
foo3 = undefined

Qui donne:

> foo3 (Dataset [] [] "x" :: Dataset '[Transformed])
...The pipeline '[ 'Transformed] lacks required processing '[ 'Cleaned, 'Transformed]...
> foo3 (Dataset [] [] "x" :: Dataset '[Cleaned, Scaled, Transformed])
...The pipeline '[ 'Cleaned, 'Scaled, 'Transformed] must not include 'Scaled...
> foo3 (Dataset [] [] "x" :: Dataset '[Cleaned, Transformed])
-- typechecks okay
foo3 (Dataset [] [] "x" :: Dataset '[Cleaned, Transformed])
  :: Dataset '[ 'Scaled, 'Cleaned, 'Transformed]

Un exemple de code complet:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Kind
import GHC.TypeLits

data Process = Cleaned | Transformed | Scaled | Inspected | Analyzed

data Dataset (pipeline :: [Process])
  = Dataset { x :: [Double]
            , y :: [Double]
            , name :: String }

type family a || b where
  True  || b = True
  False || b = b

type family Subseq xs ys where
  Subseq '[]      ys  = True
  Subseq nonempty '[] = False
  Subseq (x:xs) (x:ys) = Subseq xs ys || Subseq (x:xs) ys
  Subseq xs     (y:ys) = Subseq xs ys

type family Member x xs where
  Member x '[] = False
  Member x (x:xs) = True
  Member x (y:xs) = Member x xs

type Require procs pipeline = Require1 (Subseq procs pipeline) procs pipeline
type family Require1 b procs pipeline :: Constraint where
  Require1 True procs pipeline = ()
  Require1 False procs pipeline
    = TypeError (Text "The pipeline " :<>: ShowType pipeline :<>:
                 Text " lacks required processing " :<>: ShowType procs)
type Forbid proc pipeline = Forbid1 (Member proc pipeline) proc pipeline
type family Forbid1 b proc pipeline :: Constraint where
  Forbid1 False proc pipeline = ()
  Forbid1 True proc pipeline
    = TypeError (Text "The pipeline " :<>: ShowType pipeline :<>:
                 Text " must not include " :<>: ShowType proc)


foo1 :: (Subseq [Cleaned, Transformed] pipeline ~ True)
     => Dataset pipeline -> Dataset (Scaled : pipeline)
foo1 = undefined

foo2 :: ( Subseq [Cleaned, Transformed] pipeline ~ True
        , Member Scaled pipeline ~ False)
     => Dataset pipeline -> Dataset (Scaled : pipeline)
foo2 = undefined

foo3 :: (Require [Cleaned, Transformed] pipeline, Forbid Scaled pipeline)
     => Dataset pipeline -> Dataset (Scaled : pipeline)
foo3 = undefined
6
K. A. Buhr 31 août 2020 à 21:00

Vous pouvez utiliser un type fantôme pour stocker des informations sur votre ensemble de données dans son type, par exemple:

data Initial
data Cleaned
data Scaled

data Dataset a = Dataset { x :: Vector Double, y :: Vector Double, name :: String }

createDataset :: Vector Double -> Vector Double -> String -> Dataset Initial
createDataset x y name = Dataset x y name

removeOutliers :: Dataset Initial -> Dataset Cleaned
removeOutliers (Dataset x y n) =
    let (x', y') = clean x y
    in Dataset x' y' (n ++ "_clean")

Avec quelques extensions GHC, vous pouvez restreindre le type fantôme à un type d'état donné et éviter de déclarer explicitement des types de données vides. Par exemple:

{-# LANGUAGE DataKinds, KindSignatures #-}

data State = Initial | Cleaned | Scaled

data Dataset (a :: State) = Dataset { x :: Vector Double, y :: Vector Double, name :: String }
6
AtnNn 31 août 2020 à 20:27