Saisie dynamique statiquement sécurisée à la Python

Salut, Habr.

L'autre jour, dans l'un de mes projets de bricolage, la tâche s'est posée d'écrire un référentiel de métriques.

La tâche elle-même est résolue très simplement, mais mon problème avec le Haskell (en particulier dans les projets pour mon propre divertissement) est qu'il est impossible de simplement prendre et résoudre le problème. Il est nécessaire de décider, d'élargir, d'abstraire, d'abstraire puis de développer davantage. Par conséquent, je voulais rendre le stockage des métriques extensible afin de ne pas spécifier à l'avance ce qu'elles seraient là. C'est en soi un sujet pour un article séparé, et aujourd'hui nous allons considérer un petit ingrédient: écrire un wrapper de type sûr pour les types inconnus auparavant. Quelque chose comme la frappe dynamique, mais avec des garanties statiques que nous ne ferons pas de bêtises.

L'article, je pense, n'ouvrira rien de nouveau pour les Haskellistes expérimentés, mais maintenant nous allons au moins mettre cet ingrédient hors de la boîte et ne nous en distraire pas dans les articles suivants. Eh bien, ou vous ne pouvez pas être si modeste et dire que j'ai déjà proposé un modèle de conception entier.

Donc, nous formulons d'abord le problème. Nous devons être capables d'associer certains objets à des valeurs de types inconnus auparavant. Ou, en d'autres termes, il est nécessaire que les valeurs de types précédemment inconnus agissent comme des clés dans une sorte de carte.

Naturellement, nous ne sommes pas fous et nous n'aurons pas besoin du soutien de valeurs de tout type. Nous exigeons que le type (même s'il est inconnu) prenne en charge la comparaison dans le sens de la commande. En termes Haskell, cela signifie que nous prenons en charge les types a qui implémentent la classe Ord a .

Notez que nous pourrions demander de l'aide pour prendre un hachage et vérifier l'égalité, mais pour un certain nombre de raisons, il serait plus pratique et clair de se limiter à la comparaison.

Lorsqu'il s'agit de stocker des valeurs connues pour implémenter un certain type de classe, les types existentiels sont généralement utilisés dans le Haskell:

 data SomeOrd where MkSomeOrd :: Ord a => a -> SomeOrd 

Donc, si on nous donne un objet de type SomeOrd et que nous faisons une correspondance de motifs pour cela:

 foo :: SomeOrd -> Bar foo (MkSomeOrd val) = ... (1) ... 

puis au point (1) nous ne savons pas quel type val a, mais nous savons (et, surtout, le temporisateur sait également) que val implémente la classe temporelle Ord .

Cependant, si les fonctions de type de la classe impliquent deux (ou plus) arguments, alors l'utilisation d'un tel enregistrement est de peu d'utilité:

 tryCompare :: SomeOrd -> SomeOrd -> Bool tryCompare (MkSomeOrd val1) (MkSomeOrd val2) = ? 

Pour utiliser les méthodes Ord , il faut que val et val2 même type, mais cela ne doit pas du tout être fait! Il s'avère que notre SomeOrd inutile. Que faire?

Malgré le fait que le Haskell est un langage compilé avec un effacement de type agressif (après la compilation, ils ne sont pas là en général), le compilateur peut toujours générer des représentants de type d'exécution si on le lui demande. Le rôle représentatif du type a est la valeur du type TypeRep a , et demande génération est répondu par Typeclass Typeable .

De plus, si nous avons deux instances différentes de rep1 :: TypeRep a, rep2 :: TypeRep b , alors nous pouvons les comparer et vérifier si elles représentent le même type ou non. De plus, s'ils représentent réellement le même type, alors évidemment a coïncide avec b . Et, plus important encore, la fonction de vérification de l'égalité des représentations de type renvoie un résultat qui peut convaincre le typeur de ceci:

 eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~~: b) 

Quel non-sens est écrit ici?

Tout d'abord, eqTypeRep est une fonction.

Deuxièmement, il est polymorphe, mais non seulement par type, mais aussi par variétés de ces types. Ceci est indiqué par la partie pour tous les forall k1 k2 (a :: k1) (b :: k2) - cela signifie que a et b peuvent être non seulement des types ordinaires comme Int ou [String] , mais aussi, par exemple, des constructeurs notoires (voir DataKinds et autres tentatives de certification Haskell). Mais nous n'avons pas besoin de tout cela.

Troisièmement, il accepte deux représentations d'exécution de types potentiellement différents, TypeRep a et TypeRep b .

Quatrièmement, il renvoie une valeur de type Maybe (a :~~: b) . La chose la plus intéressante se produit ici.

Si les types ne correspondent pas, la fonction retourne le Nothing habituel et tout va bien. Si les types correspondent, alors la fonction renvoie Just val , où val est de type a :~~: b . Voyons de quel type il s'agit:

 -- | Kind heterogeneous propositional equality. Like ':~:', @a :~~: b@ is -- inhabited by a terminating value if and only if @a@ is the same type as @b@. -- -- @since 4.10.0.0 data (a :: k1) :~~: (b :: k2) where HRefl :: a :~~: a 

Parlons maintenant. Supposons que nous obtenions une valeur val de type a :~~: b . Comment pourrait-il être construit? La seule façon est avec le constructeur HRefl , et ce constructeur requiert que des deux côtés de l'icône :~~: ce soit la même chose. Par conséquent, a coïncide avec b . De plus, si nous zapternnom-match sur val , le taypcheker le saura également. Par conséquent, oui, la fonction eqTypeRep renvoie la preuve que deux types potentiellement différents sont identiques s'ils sont réellement égaux.

Cependant, dans le paragraphe ci-dessus, j'ai menti. Personne ne nous empêche d'écrire dans Haskell quelque chose comme

 wrong :: Int :~~: String wrong = wrong --    

ou

 wrong :: Int :~~: String wrong = undefined 

ou briser le système avec un tas de moyens légèrement moins évidents. C'est l'une des manifestations du bien connu dans les cercles étroits disant que le Haskell n'est pas cohérent en tant que logique. Dans les langues avec des systèmes de types plus forts, ces définitions ne sont pas estampillées.

C'est pourquoi dans la documentation citée ci-dessus, la valeur finale est mentionnée. Les deux variantes de l'implémentation de wrong ci-dessus ne produisent pas cette valeur très finale, ce qui nous donne un peu de raison et de confiance: si notre programme sur le Haskell s'est terminé (et ne s'est pas exécuté en undefined ), alors son résultat correspond aux types écrits. Ici, cependant, il y a quelques détails liés à la paresse, mais nous n'ouvrirons pas ce sujet.

Et en passant, la deuxième manifestation de la faiblesse de Haskell dans le code ci-dessus est le type de la fonction eqTypeRep . Dans des langages plus forts, cela retournerait une valeur d'un type plus fort, ce qui prouverait non seulement l'égalité des types s'ils sont réellement égaux, mais prouverait également leur inégalité s'ils sont réellement inégaux. L'incohérence de la logique Haskell, cependant, rend ces fonctions un peu inutiles: tout cela est important lorsque vous utilisez le langage comme prouveur de théorèmes, et non pas comme langage de programmation, et n'utilisez pas Haskell comme prouveur.

Eh bien, assez de la théorie des journaux et des types, revenons à nos mesures. Maintenant, dessinez simplement un hibou La discussion ci-dessus laisse entendre qu'il suffit de stocker dans notre type existentiel également c'est la représentation la plus runtime du type, et tout ira bien.

Cela nous amène à l'implémentation suivante de notre type de wrapper:

 data Dyn where Dyn :: Ord a => TypeRep a -> a -> Dyn toDyn :: (Typeable a, Ord a) => a -> Dyn toDyn val = Dyn (typeOf val) val 

Maintenant, nous écrivons une fonction qui prend ce qui suit:

1. deux valeurs de type Dyn ;
2. une fonction qui produit quelque chose pour deux valeurs de tout type ,
   basé uniquement sur les constantes mentionnées lors de la création de Dyn ( forall est responsable),
   et qui est appelée si les deux Dyn stockent des valeurs du même type;
3. et la fonction de secours, qui est appelée à la place de la précédente, si les types sont toujours différents:

 withDyns :: (forall a. Ord a => a -> a -> b) -> (SomeTypeRep -> SomeTypeRep -> b) -> Dyn -> Dyn -> b withDyns f def (Dyn ty1 v1) (Dyn ty2 v2) = case eqTypeRep ty1 ty2 of Nothing -> def (SomeTypeRep ty1) (SomeTypeRep ty2) Just HRefl -> f v1 v2 

SomeTypeRep est un wrapper existentiel sur TypeRep a pour tout a .

Nous pouvons maintenant implémenter, par exemple, la vérification et la comparaison d'égalité:

 instance Eq Dyn where (==) = withDyns (==) (\_ _ -> False) instance Ord Dyn where compare = withDyns compare compare 

Ici, nous avons profité du fait que SomeTypeRep peut être comparé les uns aux autres, donc la fonction de secours pour la commande est également compare .

C'est fait.

Seulement maintenant, c'est un péché de ne pas généraliser: nous notons qu'à l'intérieur de Dyn , toDyn , withDyns nous n'utilisons pas Ord spécifiquement, et cela pourrait être tout autre ensemble de constantes, nous pouvons donc activer l'extension ConstraintKinds et généraliser en paramétrant Dyn ensemble spécifique de restrictions que nous nécessaire dans notre tâche spécifique:

 data Dyn ctx where Dyn :: ctx a => TypeRep a -> a -> Dyn ctx toDyn :: (Typeable a, ctx a) => a -> Dyn ctx toDyn val = Dyn (typeOf val) val withDyns :: (forall a. ctx a => a -> a -> b) -> (SomeTypeRep -> SomeTypeRep -> b) -> Dyn ctx -> Dyn ctx -> b withDyns (Dyn ty1 v1) (Dyn ty2 v2) f def = case eqTypeRep ty1 ty2 of Nothing -> def (SomeTypeRep ty1) (SomeTypeRep ty2) Just HRefl -> f v1 v2 

Ensuite, Dyn Ord sera notre type de Dyn Monoid , et, disons, Dyn Monoid vous permettra de stocker des monoïdes arbitraires et de faire quelque chose de monoïdal avec eux.

Écrivons les instances dont nous avons besoin pour notre nouveau Dyn :

 instance Eq (Dyn Eq) where (==) = withDyns (==) (\_ _ -> False) instance Ord (Dyn Ord) where compare = withDyns compare compare 

... seulement cela ne fonctionne pas. Le typeur ne sait pas que Dyn Ord implémente également Eq ,
vous devez donc copier toute la hiérarchie:

 instance Eq (Dyn Eq) where (==) = withDyns d1 d2 (==) (\_ _ -> False) instance Eq (Dyn Ord) where (==) = withDyns d1 d2 (==) (\_ _ -> False) instance Ord (Dyn Ord) where compare = withDyns d1 d2 compare compare 

Eh bien, maintenant c'est sûr.

... peut-être, dans un Haskell moderne, vous pouvez faire en sorte que le minuteur lui-même affiche les instances du formulaire

 instance C_i (Dyn (C_1, ... C_n)) where ... 

parce que quelque chose de prologique sort, mais je ne l'ai pas encore fait, je vais devoir m'asseoir pour le cueillir. Restez à l'écoute.

Et aussi, si vous plissez les yeux, vous pouvez voir que notre Dyn ressemble étrangement à une paire dépendante du type (ty : Type ** val : ty) des langages cryptiques. Mais seulement dans les langues que je connais, il est impossible de faire correspondre le type, car la paramétricité (qui dans ce cas, à mon humble avis, est interprétée trop largement), mais ici cela semble possible.

Mais la chose la plus importante - maintenant vous pouvez avoir en toute sécurité quelque chose comme Map (Dyn Ord) SomeValue et utiliser toutes les valeurs comme clés, tant qu'elles prennent elles-mêmes en charge la comparaison. Par exemple, les identifiants avec des descriptions de mesures peuvent être utilisés comme clés, mais ceci est un sujet pour l'article suivant.