Installations pour générer des types Haskell à Haskell ("second order Haskell")?

Question

Excuses d'avance si cette question est un peu vague. C'est le résultat de quelques rêveries de fin de semaine.

Avec le système de type merveilleux de Haskell, il est délicieusement agréable d'exprimer une structure mathématique (en particulier algébrique) comme typeclasses. Je veux dire, jetez un oeil à numeric-prelude! Mais tirer parti d'une telle structure de type en pratique m'a toujours semblé difficile.

Vous avez une belle façon de type système de CONSTATANT que v1 et v2 sont des éléments d'un espace vectoriel V et que w est un élément d'un espace vectoriel W. Le système de type vous permet d'écrire un programme en ajoutant v1 et v2, mais pas v1 et w. Génial! Mais en pratique, vous voudrez peut-être jouer avec potentiellement des centaines d'espaces vectoriels, et vous ne voulez certainement pas créer les types , V2, ..., V100 et déclarez-les instances de la typeclass de l'espace vectoriel! Ou peut-être que vous lisez certaines données du monde réel résultant des symboles a, b et c - vous pouvez vouloir exprimer que l'espace vectoriel libre sur ces symboles est vraiment un espace vectoriel!

Alors vous êtes coincé, n'est-ce pas? Pour faire beaucoup de choses que vous aimeriez faire avec les espaces vectoriels dans un environnement de calcul scientifique, vous devez abandonner votre système de types en supprimant un type de classe d'espace vectoriel et avoir des fonctions effectuant des vérifications de compatibilité au moment de l'exécution. Devriez-vous? Ne devrait-il pas être possible d'utiliser le fait que Haskell est purement fonctionnel pour écrire un programme qui génère tous les types dont vous avez besoin et les insère dans le vrai programme? Est-ce qu'une telle technique existe? Par tous les moyens font remarquer si je néglige simplement quelque chose de fondamental ici (je suis probablement) :-)

Editer: Tout à l'heure ai-je découvert fundeps. Je vais devoir réfléchir un peu à la façon dont ils se rapportent à ma question (des commentaires éclairants à ce sujet sont appréciés).

Answer 1

Template Haskell le permet. Le wiki page a quelques liens utiles; en particulier Bulat'stutorials.

La syntaxe de déclaration de niveau supérieur est celle que vous souhaitez. En tapant:

mkFoo = [d| data Foo = Foo Int |] 

vous créez un modèle épissure Haskell (comme une fonction de compilation) qui va créer une déclaration pour data Foo = Foo Int juste en insérant la ligne $(mkFoo).

Bien que ce petit exemple ne soit pas trop utile, vous pouvez fournir un argument à mkFoo pour contrôler le nombre de déclarations que vous souhaitez. Maintenant, un $(mkFoo 100) produira 100 nouvelles déclarations de données pour vous. Vous pouvez également utiliser TH pour générer des instances de classe de type. Mon paquet adaptive-tuple est un très petit projet qui utilise Template Haskell pour faire quelque chose de similaire.

Une approche alternative consisterait à utiliser Derive, qui dérivera automatiquement les instances de classe de type. Cela pourrait être plus simple si vous avez seulement besoin des instances.

Answer 2

Il existe également des techniques de programmation de niveau type simples dans Haskell.Un exemple canonique suit:

-- A family of types for the natural numbers 
data Zero 
data Succ n 

-- A family of vectors parameterized over the naturals (using GADTs extension) 
data Vector :: * -> * -> * where 
    -- empty is a vector with length zero 
    Empty :: Vector Zero a 
    -- given a vector of length n and an a, produce a vector of length n+1 
    Cons :: a -> Vector n a -> Vector (Succ n) a 

-- A type-level adder for natural numbers (using TypeFamilies extension) 
type family Plus n m :: * 
type instance Plus Zero n = n 
type instance Plus (Succ m) n = Succ (Plus m n) 

-- Typesafe concatenation of vectors: 
concatV :: Vector n a -> Vector m a -> Vector (Plus n m) a 
concatV Empty ys = ys 
concatV (Cons x xs) ys = Cons x (concatV xs ys) 

Prenez un moment pour prendre que je pense qu'il est assez magique que cela fonctionne.. Cependant, la programmation au niveau du type dans Haskell est dans la caractéristique-uncanny-valley - juste assez pour attirer l'attention sur ce que vous ne pouvez pas faire. Des langages à typage indépendant tels que Agda, Coq et Epigram prennent ce style à sa limite et à sa pleine puissance. Modèle Haskell ressemble beaucoup plus au style de LISP-macro habituel de la génération de code. Vous écrivez du code pour écrire du code, puis vous dites "ok insérez le code généré ici". Contrairement à la technique ci-dessus, vous pouvez écrire n'importe quel code calculé de cette façon, mais vous n'obtenez pas le contrôle de typage très général comme on le voit dans concatV ci-dessus.

Vous avez donc quelques options pour faire ce que vous voulez. Je pense que la métaprogrammation est un espace vraiment intéressant, et à certains égards encore assez jeune. Amusez-vous à explorer. :-)