Cast implicite et statique (coercition) dans Haskell

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.

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)