Syntaxe de promotion des données

Question

J'ai récemment découvert le Data.Promotion moitié de célibataires.Il contient de nombreuses familles de types qui permettent des calculs essentiellement arbitraires au niveau du type.J'ai quelques questions sur l'utilisation:

1. Quelle est la différence entre ($), (%$), ($$), et sont-ils liés à :++$, :.$, etc?S'agit-il réellement d'opérateurs infixes ?J'étais l'impression tous les constructeurs de types infixes devaient commencer par un :.

2. J'essaie de mapper un constructeur sur une liste :

   {-# LANGUAGE DataKinds, TypeOperators, PolyKinds #-}
   import Data.Promotion.Prelude
   
   data Foo a b
   type MyList = '[Int, Double, Float]
   
    -- expects one more argument to `Foo`
   type FooList1 b = Map ((Flip Foo) $ b) MyList
   
   -- parse error on the second `b`
   type FooList2 b = Map (($ b) :. Foo) MyList 
   

   mais j'ai du mal à utiliser un constructeur de type multi-paramètres.Des idées ?

3. J'ai pu remplacer toutes les fonctions de type que j'avais écrites par des fonctions équivalentes de Data.Promotion sauf celui-là :

   type family ListToConstraint (xs :: [Constraint]) :: Constraint
   type instance ListToConstraint '[] = ()
   type instance ListToConstraint (x ': xs) = (x, ListToConstraint xs)
   

   Y a-t-il une sorte de magie qui opère avec le Constraint genre qui empêcherait sa manipulation en tant que paires imbriquées ?

Answer 1

1. Comme cela a été expliqué dans les commentaires, il n'y a plus d'exigence syntaxique pour que les fonctions infixes au niveau du type commencent par deux points.Alors oui, ce sont tous des opérateurs infixes.Il n'y a pas deux opérateurs infixes automatiquement liés les uns aux autres, mais la bibliothèque singletons utilise certaines conventions de dénomination en interne pour relier les symboles utilisés pour défonctionnalisation (voir ci-dessous) à leurs homologues normaux.

2. Il y a tout un tas de problèmes liés au fait que les familles de types ne peuvent pas être partiellement appliquées, alors que les types de données le peuvent.C'est pourquoi la bibliothèque singletons utilise une technique appelée défonctionnalisation:pour chaque fonction de type partiellement appliquée, il définit un type de données.Il existe alors une famille de type (très grande et ouverte) appelée Apply qui prend tous ces types de données qui représentent des fonctions partiellement appliquées et des arguments appropriés et exécute l'application réelle.

   Le type de telles représentations défonctionnalisées des fonctions de type est

   TyFun k1 k2 -> *
   

   pour diverses raisons (d'ailleurs, une bonne introduction à tout cela se trouve dans le billet de blog de Richard Eisenberg "Défonctionnalisation pour la victoire"), alors que le type de fonction de type "normal" correspondant serait

   k1 -> k2
   

   Désormais, toutes les fonctions de type d'ordre supérieur dans les singletons attendent des arguments défonctionnalisés.Par exemple, le genre de Map est

   Map :: (TyFun k k1 -> *) -> [k] -> [k1]
   

   et pas

   Map :: (k -> k1) -> [k] -> [k1]
   

   Examinons maintenant les fonctions avec lesquelles vous travaillez :

   Flip :: (TyFun k (TyFun k1 k2 -> *) -> *) -> k1 -> k -> k2
   

   Le premier argument est une fonction curry défonctionnelle de type k -> k1 -> k2, et cela transforme cela en une fonction de type normale de type k1 -> k -> k2.

   Aussi:

   ($) :: (TyFun k1 k -> *) -> k1 -> k
   

   C'est juste un synonyme de Apply Je l'ai mentionné ci-dessus.

   Regardons maintenant votre exemple :

   type FooList1 b = Map ((Flip Foo) $ b) MyList  -- fails
   

   Ici, nous avons deux problèmes:D'abord, Foo est un type de données et non un symbole défonctionnalisé comme Flip attend.Deuxième, Flip est une famille de types et attend trois arguments, mais un seul est fourni.Nous pouvons résoudre le premier problème en appliquant TyCon2, qui prend un type de données normal et le transforme en un symbole défonctionnalisé :

   TyCon2 :: (k -> k1 -> k2) -> TyFun k (TyFun k1 k2 -> *) -> *
   

   Pour le deuxième problème, nous avons besoin d’une des applications partielles de Flip que les singletons définissent déjà pour nous :

   FlipSym0 :: TyFun (TyFun k1 (TyFun k2 k -> *) -> *)
                     (TyFun k2 (TyFun k1 k -> *) -> *)
               -> *
   FlipSym1 ::    (TyFun k1 (TyFun k2 k -> *) -> *)
               -> TyFun k2 (TyFun k1 k -> *) -> *
   
   FlipSym2 ::    (TyFun k1 (TyFun k2 k -> *) -> *)
               -> k2 -> TyFun k1 k -> *
   
   Flip     ::    (TyFun k (TyFun k1 k2 -> *) -> *)
               -> k1 -> k -> k2
   

   Si vous regardez attentivement, alors FlipSymN est la représentation requise si Flip est partiellement appliqué à N arguments, et Flip correspond à l'imaginaire FlipSym3.Dans l'exemple, Flip est appliqué à un argument, donc l'exemple corrigé devient

   type FooList1 b = Map ((FlipSym1 (TyCon2 Foo)) $ b) MyList
   

   Et ça marche :

   GHCi> :kind! FooList1 Char
   FooList1 Char :: [*]
   = '[Foo Int Char, Foo Double Char, Foo Float Char]
   

   Le deuxième exemple est similaire :

   type FooList2 b = Map (($ b) :. Foo) MyList
   

   Ici, nous avons les problèmes suivants :encore, Foo doit être transformé en un symbole défonctionnalisé en utilisant TyCon2;sections d'opérateur telles que $ b ne sont pas disponibles au niveau du type, d'où l'erreur d'analyse.Nous devrons utiliser Flip encore une fois, mais cette fois FlipSym2, car nous l'appliquons à l'opérateur $ et b.Ah mais alors $ est partiellement appliqué, nous avons donc besoin d'un symbole correspondant à $ avec 0 argument.Ceci est disponible sous forme $$ en singletons (pour les opérateurs symboliques, les symboles défonctionnalisés ont été ajoutés $s).Et enfin, :. est également partiellement appliqué :il attend trois opérateurs, mais n'en a reçu que deux.On passe donc de :. à :.$$$ (trois dollars car un dollar correspond à 0, et trois dollars correspondent à 2).En tout:

   type FooList2 b = Map ((FlipSym2 ($$) b) :.$$$ TyCon2 Foo) MyList
   

   Et encore une fois, ça marche :

   GHCi> :kind! FooList2 Char
   FooList2 Char :: [*]
   = '[Foo Int Char, Foo Double Char, Foo Float Char]
   

3. Je suis peut-être aveugle, mais je ne pense pas que cela soit contenu dans les singletons, ce qui ne concerne pas vraiment Constraints.C'est cependant une fonction utile.C'est dans un bibliothèque sur laquelle je travaille actuellement.Il est encore inachevé et pour l’essentiel non documenté, c’est pourquoi je ne l’ai pas encore publié.