Puis-je contraindre une famille de types?

Certes, l’évidence serait de simplement écrire directement la contrainte souhaitée:

 class (Differentiable (D f)) => Differentiable (f :: * -> *) where 

Hélas, GHC en souffre et refuse de jouer:

 ConstrainTF.hs:17:1: Cycle in class declaration (via superclasses): Differentiable -> Differentiable In the class declaration for `Differentiable' 

Donc, comme c’est souvent le cas lorsque l’on tente de décrire des contraintes de type assez sophistiquées pour laisser le GHC récalcitrant, il faut recourir à une technique de tromperie sournoise.

Rappelant certaines fonctionnalités pertinentes de GHC où le type de piratage est impliqué:

• Il est paranoïaque quant à la non-destruction au niveau du type, bien plus que proportionnée au désagrément réel qu’elle entraîne pour l’utilisateur.
• Il s’engagera joyeusement à prendre des décisions concernant les classes et les instances avant d’avoir tenu compte de toutes les informations disponibles.
• Il tentera consciencieusement de vérifier tout ce que vous lui avez fait croire.

Ce sont les principes sournois qui sous-tendent les anciennes instances de faux-génériques bien connues, où les types sont unifiés post-hoc avec (~) afin d’améliorer le comportement d’inférence de type de certaines constructions de type hackery.

Dans ce cas, cependant, plutôt que de saisir des informations de type au- delà du GHC, nous devrons empêcher GHC de remarquer une contrainte de classe , ce qui est un genre totalement différent de … heeeey, waaaitaminute ….

 import GHC.Prim type family DiffConstraint (f :: * -> *) :: Constraint type instance DiffConstraint f = Differentiable f class (DiffConstraint (D f)) => Differentiable (f :: * -> *) where type D f :: * -> * 

Palan par son propre pétard!

C’est la vraie affaire aussi. Ceux-ci sont acceptés, comme vous l’espérez:

 instance Differentiable (K a) where type D (K a) = K Void instance Differentiable I where type DI = K () 

Mais si nous lui offrons des bêtises à la place:

 instance Differentiable I where type DI = [] 

GHC nous présente précisément le message d’erreur que nous aimerions voir:

 ConstrainTF.hs:29:10: No instance for (Differentiable []) arising from the superclasses of an instance declaration Possible fix: add an instance declaration for (Differentiable []) In the instance declaration for `Differentiable I' 

Il y a un petit accroc, bien sûr, à savoir que ceci:

 instance (Differentiable f, Differentiable g) => Differentiable (f :+: g) where type D (f :+: g) = D f :+: D g 

… se révèle moins que bien fondé, comme nous l’avons dit au GHC pour vérifier que (f :+: g) est Differentiable , de même que (D f :+: D g) , ce qui ne se termine pas bien (ou pas du tout).

Le moyen le plus simple d’éviter cela serait de passer à la vitesse supérieure sur une stack de cas de base explicites, mais ici, GHC semble vouloir diverger à chaque fois qu’une contrainte Differentiable apparaît dans un contexte d’instance. J’imagine que cela demande inutilement de contrôler les contraintes d’instance, et que je pourrais peut-être être distrait assez longtemps avec une autre couche de tromperie, mais je ne sais pas trop par où commencer et j’ai épuisé mes capacités de piratage ce soir.

Un peu de discussion IRC sur #haskell a réussi à me rafraîchir un peu la mémoire sur la façon dont GHC gère les contraintes de contexte de classe, et il semble que nous pouvons modifier un peu les choses avec une famille de contraintes plus pointue. En utilisant ceci:

 type family DiffConstraint (f :: * -> *) :: Constraint type instance DiffConstraint (K a) = Differentiable (K a) type instance DiffConstraint I = Differentiable I type instance DiffConstraint (f :+: g) = (Differentiable f, Differentiable g) 

Nous avons maintenant une récursion beaucoup plus sage pour les sums:

 instance (Differentiable (D f), Differentiable (D g)) => Differentiable (f :+: g) where type D (f :+: g) = D f :+: D g 

Le cas récursif ne peut pas être si facilement divisé en deux pour les produits, et appliquer les mêmes modifications n’a fait qu’améliorer les choses dans la mesure où j’ai reçu un débordement de stack de réduction de contexte plutôt qu’une simple boucle infinie.

Votre meilleur pari pourrait être de définir quelque chose en utilisant le paquet de constraints :

 import Data.Constraint class Differentiable (f :: * -> *) where type D f :: * -> * witness :: pf -> Dict (Differentiable (D f)) 

Vous pouvez alors ouvrir manuellement le dictionnaire chaque fois que vous avez besoin de vous remettre en route.

Cela vous permettrait d’utiliser la forme générale de la solution dans la réponse de Casey, mais de ne pas avoir le compilateur (ou le moteur d’exécution) en rotation indéfiniment lors de l’induction.

Avec les nouvelles UndecidableSuperclasses dans GHC 8

 class Differentiable (D f) => Differentiable (f :: Type -> Type) where 

travaux.

Cela peut être accompli de la même manière qu’Edward suggère avec une toute petite mise en œuvre de Dict . Tout d’abord, récupérons les extensions de langue et les importations.

 {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} import Data.Proxy 

TypeOperators est uniquement pour votre problème d’exemple.

Petit Dict

Nous pouvons faire notre propre petite implémentation de Dict . Dict utilise un GADT et un ConstraintKinds pour capturer toute contrainte dans le constructeur d’un GADT.

 data Dict c where Dict :: c => Dict c 

withDict et withDict2 réintroduisent la contrainte par correspondance de modèle sur le GADT. Il suffit de pouvoir raisonner sur les termes avec une ou deux sources de contraintes.

 withDict :: Dict c -> (c => x) -> x withDict Dict x = x withDict2 :: Dict a -> Dict b -> ((a, b) => x) -> x withDict2 Dict Dict x = x 

Types infiniment différenciables

On peut maintenant parler de types infiniment différenciables, dont les dérivés doivent également être différenciables

 class Differentiable f where type D f :: * -> * d2 :: pf -> Dict (Differentiable (D f)) -- This is just something to recover from the dictionary make :: a -> fa 

d2 prend un proxy pour le type et récupère le dictionnaire pour prendre la dérivée seconde. Le proxy nous permet de spécifier facilement le type de d2 nous parlons. Nous pouvons obtenir des dictionnaires plus profonds en appliquant d :

 d :: Dict (Differentiable t) -> Dict (Differentiable (D t)) d d1 = withDict d1 (d2 (pt (d1))) where pt :: Dict (Differentiable t) -> Proxy t pt = const Proxy 

Capturer le dicton

Les types de foncteurs polynomiaux, les produits, les sums, les constantes et zéro sont tous infiniment différenciables. Nous définirons les témoins d2 pour chacun de ces types

 data K x = K deriving (Show) newtype I x = I x deriving (Show) data (f :+: g) x = L (fx) | R (gx) deriving (Show) data (f :*: g) x = fx :&: gx deriving (Show) 

Zéro et constantes ne requièrent aucune connaissance supplémentaire pour capturer le Dict leurs dérivés

 instance Differentiable K where type DK = K make = const K d2 = const Dict instance Differentiable I where type DI = K make = I d2 = const Dict 

La sum et le produit requièrent tous deux que les dictionnaires des deux dérivés de leur composant puissent déduire le dictionnaire pour leur dérivé.

 instance (Differentiable f, Differentiable g) => Differentiable (f :+: g) where type D (f :+: g) = D f :+: D g make = R . make d2 p = withDict2 df dg $ Dict where df = d2 . pf $ p dg = d2 . pg $ p pf :: p (f :+: g) -> Proxy f pf = const Proxy pg :: p (f :+: g) -> Proxy g pg = const Proxy instance (Differentiable f, Differentiable g) => Differentiable (f :*: g) where type D (f :*: g) = (D f :*: g) :+: (f :*: D g) make x = make x :&: make x d2 p = withDict2 df dg $ Dict where df = d2 . pf $ p dg = d2 . pg $ p pf :: p (f :*: g) -> Proxy f pf = const Proxy pg :: p (f :*: g) -> Proxy g pg = const Proxy 

Récupérer le dictionnaire

Nous pouvons récupérer le dictionnaire pour des contraintes que nous n’aurions pas autrement d’informations à déduire. Differentiable f ne laisserait normalement utiliser que get pour make :: a -> fa , mais ne pas make :: a -> D fa ou make :: a -> D (D f) a .

 make1 :: Differentiable f => pf -> a -> D fa make1 p = withDict (d2 p) make make2 :: Differentiable f => pf -> a -> D (D f) a make2 p = withDict (d (d2 p)) make