Cast implicite et statique (coercition) dans Haskell

9

Problème

Considérez le problème de conception suivant dans Haskell. J'ai un EDSL simple et symbolique dans lequel je veux exprimer des variables et des expressions générales (polynômes multivariés) comme x^2 * y + 2*z + 1. De plus, je veux exprimer certaines équations symboliques sur des expressions, disons x^2 + 1 = 1, ainsi que des définitions , comme x := 2*y - 2.

Le but est de:

  1. Avoir un type distinct pour les variables et les expressions générales - certaines fonctions peuvent être appliquées aux variables et non aux expressions complexes. Par exemple, un opérateur de définition:= peut être de type (:=) :: Variable -> Expression -> Definitionet il ne devrait pas être possible de passer une expression complexe comme paramètre de gauche (bien qu'il devrait être possible de passer une variable comme paramètre de droite, sans transtypage explicite ) .
  2. Ayez une expression dans les expressions Num, de sorte qu'il est possible de promouvoir des littéraux entiers en expressions et d'utiliser une notation pratique pour les opérations algébriques courantes comme l'addition ou la multiplication sans introduire certains opérateurs d'encapsuleur auxiliaires.

En d'autres termes, j'aimerais avoir un transtypage de type implicite et statique (coercition) de variables en expressions. Maintenant, je sais qu'en tant que tel, il n'y a pas de transtypages implicites dans Haskell. Néanmoins, certains concepts de programmation orientée objet (héritage simple, dans ce cas) sont exprimables dans le système de type de Haskell, avec ou sans extensions de langage. Comment pourrais-je satisfaire les deux points ci-dessus tout en conservant une syntaxe légère? Est-ce même possible?

Discussion

Il est clair que le problème principal ici est Numla restriction de type de, par exemple

(+) :: Num a => a -> a -> a

En principe, il est possible d'écrire un seul type de données algébrique (généralisé) pour les variables et les expressions. Ensuite, on pourrait écrire :=de telle manière que l'expression de gauche est discriminée et seul un constructeur de variable est accepté, avec une erreur d'exécution sinon. Ce n'est cependant pas une solution propre et statique (c'est-à-dire au moment de la compilation) ...

Exemple

Idéalement, j'aimerais obtenir une syntaxe légère telle que

computation = do
  x <- variable
  t <- variable

  t |:=| x^2 - 1
  solve (t |==| 0)

En particulier, je veux interdire une notation comme t + 1 |:=| x^2 - 1puisque :=devrait donner une définition d'une variable et non une expression entière à gauche.

Maciej Bendkowski
la source
1
peut-être pourriez-vous utiliser un class FromVar eavec une méthode fromVar :: Variable -> eet fournir des instances pour Expressionet Variable, puis avoir vos variables ont des types polymorphes x :: FromVar e => eetc. Je n'ai pas testé à quel point cela fonctionne depuis que je suis sur mon téléphone en ce moment.
Mor A.
Je ne sais pas en quoi la FromVarclasse de caractères serait utile. Je veux éviter les transtypages explicites tout en conservant Exprune instance de Num. J'ai édité la question en ajoutant un exemple de notation que j'aimerais atteindre.
Maciej Bendkowski

Réponses:

8

Pour tirer parti du polymorphisme plutôt que du sous-typage (parce que c'est tout ce que vous avez dans Haskell), ne pensez pas "une variable est une expression", mais "les variables et les expressions ont des opérations en commun". Ces opérations peuvent être placées dans une classe de type:

class HasVar e where fromVar :: Variable -> e

instance HasVar Variable where fromVar = id
instance HasVar Expression where ...

Ensuite, plutôt que de lancer des choses, rendez les choses polymorphes. Si c'est le cas v :: forall e. HasVar e => e, il peut être utilisé à la fois comme expression et comme variable.

example :: (forall e. HasVar e => e) -> Definition
example v = (v := v)  -- v can be used as both Variable and Expression

 where

  (:=) :: Variable -> Expression -> Definition

Squelette pour faire le code ci-dessous typecheck: https://gist.github.com/Lysxia/da30abac357deb7981412f1faf0d2103

computation :: Solver ()
computation = do
  V x <- variable
  V t <- variable
  t |:=| x^2 - 1
  solve (t |==| 0)
Li-yao Xia
la source
Intéressant, merci! J'ai envisagé de cacher les variables et les expressions derrière les types existentiels pendant un bref instant, mais j'ai rejeté l'idée car elle introduisait une notation supplémentaire, voyez la vôtre V. Au départ, ce n'était pas ce que je voulais, mais j'ai peut-être été trop rapide pour le rejeter ... Je ne peux probablement pas me débarrasser de l'opaque V. Sur une note connexe, comment puis-je créer une instance de V (forall e . HasVar e => e)? Dans Coq, j'utiliserais des calculs de type et des correspondances de motifs sur un type inductif, mais on ne sait pas comment y parvenir dans Haskell.
Maciej Bendkowski
1
Vous pouvez saisir une w :: Variablecertaine façon et d' appliquer fromVarà elle: variable = (\w -> V (fromVar w)) <$> (_TODO_ :: Solver Variable).
Li-yao Xia
1
Et Vpourrait être évité avec des types imprédicatifs, mais c'est toujours WIP. Ou on peut faire variableprendre la suite avec un argument polymorphe explicitement au lieu de indirectement via (>>=).
Li-yao Xia