Pourquoi les types de données ML/Haskell sont-ils utiles pour définir des "langages" comme les expressions arithmétiques ?

Question

Il s'agit plutôt d'une question douce sur les systèmes de types statiques dans les langages fonctionnels comme ceux de la famille ML. Je comprends pourquoi vous avez besoin de types de données pour décrire des structures de données comme les listes et les arbres, mais définir des "expressions" comme celles de la logique propositionnelle dans les types de données semble n'apporter qu'une certaine commodité et n'est pas nécessaire. Par exemple

datatype arithmetic_exp = Constant of int
                        | Neg of arithmetic_exp
                        | Add of (arithmetic_exp * arithmetic_exp)
                        | Mult of (arithmetic_exp * arithmetic_exp)

définit un ensemble de valeurs, sur lesquelles vous pouvez écrire un eval qui vous donnerait le résultat. Vous pourriez tout aussi bien définir 4 fonctions : const: int -> int , neg: int -> int , add: int * int -> int y mult: int * int -> int et ensuite une expression du type add (mult (const 3, neg 2), neg 4) vous donnerait la même chose sans perte de sécurité statique. La seule complication est que vous devez faire quatre choses au lieu de deux. En apprenant SML et Haskell, j'ai essayé de réfléchir aux caractéristiques qui vous apportent quelque chose de nécessaire et celles qui ne sont qu'une commodité, c'est pourquoi je pose la question. Je suppose que cela serait important si vous voulez découpler le processus d'évaluation d'une valeur de la valeur elle-même, mais je ne suis pas sûr que cela soit utile.

Merci beaucoup.

Answer 1

Il existe une dualité entre les encodages initiaux / de premier ordre / basés sur le type de données (alias les encastrements profonds) et les encodages finaux / d'ordre supérieur / basés sur l'évaluateur (alias les encastrements peu profonds). En effet, vous pouvez typiquement utiliser une classe de combinateurs au lieu d'un type de données (et faire des allers-retours entre les deux).

Voici un module montrant les deux approches :

{-# LANGUAGE GADTs, Rank2Types #-}

module Expr where

data Expr where
  Val :: Int -> Expr
  Add :: Expr -> Expr -> Expr

class Expr' a where
  val :: Int -> a
  add :: a -> a -> a

Vous pouvez voir que les deux définitions se ressemblent étrangement. Expr' a c'est essentiellement la description d'une algèbre sur Expr ce qui signifie que vous pouvez obtenir un a à partir d'un Expr si vous avez un tel Expr' a . De même, puisque vous pouvez écrire une instance Expr' Expr vous êtes capable de réifier un terme de type forall a. Expr' a => a en une valeur syntaxique de type Expr :

expr :: Expr' a => Expr -> a
expr e = case e of
  Val n   -> val n
  Add p q -> add (expr p) (expr q)

instance Expr' Expr where
  val = Val
  add = Add

expr' :: (forall a. Expr' a => a) -> Expr
expr' e = e

En fin de compte, le choix d'une représentation plutôt qu'une autre dépend vraiment de votre objectif principal : si vous voulez inspecter la structure de l'expression (par exemple, si vous voulez l'optimiser / la compiler), c'est plus facile si vous avez accès à un AST. Si, d'un autre côté, vous êtes seulement intéressé par le calcul d'un invariant en utilisant un pli (par exemple, la profondeur de l'expression ou son évaluation), un encodage d'ordre supérieur fera l'affaire.

Answer 2

L'ADT se présente sous une forme que vous pouvez inspecter et manipuler autrement qu'en l'évaluant simplement. Une fois que vous avez caché toutes les données intéressantes dans un appel de fonction, vous ne pouvez plus rien faire d'autre que de l'évaluer. Considérez cette définition, similaire à celle de votre question, mais avec un terme Var pour représenter les variables et avec les termes Mul et Neg supprimés pour se concentrer sur l'addition.

data Expr a = Constant a
            | Add (Expr a) (Expr a)
            | Var String
            deriving Show

La fonction évidente à écrire est eval bien sûr. Il faut un moyen de rechercher la valeur d'une variable, et c'est simple :

-- cheating a little bit by assuming all Vars are defined
eval :: Num a => Expr a -> (String -> a) -> a
eval (Constant x) _env = x
eval (Add x y) env = eval x env + eval y env
eval (Var x) env = env x

Mais supposons que vous n'ayez pas encore de mappage de variable. Vous avez une grande expression que vous allez évaluer plusieurs fois, pour différents choix de variables. Et une fonction récursive idiote a construit une expression comme :

Add (Constant 1) 
    (Add (Constant 1) 
         (Add (Constant 1) 
              (Add (Constant 1) 
                   (Add (Constant 1) 
                        (Add (Constant 1) 
                             (Var "x"))))))

Il serait inutile de recalculer 1+1+1+1+1+1 à chaque fois que vous évaluez ceci : ne serait-ce pas bien si votre évaluateur pouvait se rendre compte que c'est juste une autre façon d'écrire Add (Constant 6) (Var "x") ?

Vous écrivez donc un optimiseur d'expression, qui s'exécute avant que les variables ne soient disponibles et tente de simplifier les expressions. Il existe de nombreuses règles de simplification que vous pouvez appliquer, bien sûr ; ci-dessous, je n'en ai implémenté que deux très simples pour illustrer mon propos.

simplify :: Num a => Expr a -> Expr a
simplify (Add (Constant x) (Constant y)) = Constant $ x + y
simplify (Add (Constant x) (Add (Constant y) z)) = simplify $ Add (Constant $ x + y) z
simplify x = x

Maintenant, à quoi ressemble notre expression idiote ?

> simplify $ Add (Constant 1) (Add (Constant 1) (Add (Constant 1) (Add (Constant 1) (Add (Constant 1) (Add (Constant 1) (Var "x"))))))
Add (Constant 6) (Var "x")

Toutes les choses inutiles ont été supprimées et vous avez maintenant une expression propre et agréable à utiliser pour différentes valeurs de x .

Comment faire la même chose avec une représentation de cette expression en fonctions ? C'est impossible, car il n'existe pas de "forme intermédiaire" entre la spécification initiale de l'expression et son évaluation finale : on ne peut considérer l'expression que comme un appel de fonction unique et opaque. En l'évaluant à une valeur particulière de x évalue nécessairement chacune des sous-expressions à nouveau, et il n'y a aucun moyen de les démêler.

Voici une extension du type fonctionnel que vous proposez dans votre question, à nouveau enrichie de variables :

type FExpr a = (String -> a) -> a

lit :: a -> FExpr a
lit x _env = x

add :: Num a => FExpr a -> FExpr a -> FExpr a
add x y env = x env + y env

var :: String -> FExpr a
var x env = env x

avec la même expression idiote à évaluer plusieurs fois :

sample :: Num a => FExpr a
sample = add (lit 1)
             (add (lit 1)
                  (add (lit 1)
                       (add (lit 1)
                            (add (lit 1)
                                 (add (lit 1)
                                      (var "x"))))))

Il fonctionne comme prévu :

> sample $ \_var -> 5
11

Mais il doit faire un tas d'additions à chaque fois que vous l'essayez pour une autre x même si l'addition et la variable sont pour la plupart sans rapport. Et il n'y a aucun moyen de simplifier l'arbre d'expression. On ne peut pas le simplifier en le définissant : c'est-à-dire qu'on ne peut pas faire de add plus intelligente, parce qu'elle ne peut pas du tout inspecter ses arguments : ses arguments sont des fonctions qui, pour autant que l'on sache, ne sont pas des fonctions. add est concerné, pourrait faire n'importe quoi. Et vous ne pouvez pas non plus la simplifier après l'avoir construite : à ce stade, vous avez juste une fonction opaque qui prend une fonction de recherche de variable et produit une valeur.

En modélisant les parties importantes de votre problème comme des types de données à part entière, vous en faites des valeurs que votre programme peut manipuler intelligemment. Si vous les laissez en tant que fonctions, vous obtenez un programme plus court mais moins puissant, car vous enfermez toutes les informations dans des lambdas que seul GHC peut manipuler.

Et une fois que vous l'avez écrit avec des ADT, il n'est pas difficile de ramener cette représentation à la représentation plus courte basée sur les fonctions si vous le souhaitez. C'est-à-dire qu'il peut être intéressant d'avoir une fonction de type

convert :: Expr a -> FExpr a

Mais en fait, nous l'avons déjà fait ! C'est exactement le type que eval a. Vous ne l'avez peut-être pas remarqué à cause de l'alias de type FExpr, qui n'est pas utilisé dans la définition de eval .

Ainsi, d'une certaine manière, la représentation ADT est plus générale et plus puissante, agissant comme un arbre que vous pouvez plier de nombreuses façons différentes. L'une de ces façons consiste à l'évaluer, exactement comme le fait la représentation basée sur les fonctions. Mais il y en a d'autres :

• Simplifier l'expression avant de l'évaluer
• Produire une liste de toutes les variables qui doivent être définies pour que cette expression soit bien formée
• Comptez la profondeur de l'imbrication de la partie la plus profonde de l'arbre, afin d'estimer le nombre de cadres de pile dont l'évaluateur pourrait avoir besoin.
• Convertir l'expression en une chaîne de caractères se rapprochant d'une expression Haskell que vous pourriez taper pour obtenir le même résultat.

Dans la mesure du possible, il est donc préférable de travailler avec des ADT riches en informations aussi longtemps que possible, puis de replier l'arbre dans une forme plus compacte lorsque vous avez quelque chose de spécifique à faire avec.