Haskell AST avec types récursifs

Question

J'essaie actuellement de construire un solveur de lambda-calcul, et j'ai un léger problème avec la construction de l'AST. Un terme de calcul de lambda est inductivement défini comme suit:

1) Une variable

2) lambda, une variable, un point, et une expression lambda.

3) Une parenthèse, une expression lambda, une expression lambda et une parenthèse.

Ce que je voudrais faire (et d'abord essayé) est la suivante:

data Expr = 
    Variable 
    | Abstract Variable Expr 
    | Application Expr Expr 

travailler Maintenant, évidemment cela ne veut pas, car variable est pas un type, et abstraite Expr variable attend types. Donc, ma solution à ce hacky est d'avoir:

type Variable = String 

data Expr = 
    Atomic Variable 
    | Abstract Variable Expr 
    | Application Expr Expr 

Maintenant, ce qui est vraiment gênant puisque je n'aime pas la variable atomique sur son propre, mais abstraite prenant une chaîne plutôt qu'une expr. Y a-t-il un moyen de rendre cela plus élégant et de le faire comme la première solution?

Answer 1

Votre première solution est juste une définition erronée sans signification. Variable n'est pas un type, c'est un constructeur de valeur nulle. Vous ne pouvez pas faire référence à Variable dans une définition de type un peu comme vous ne pouvez pas faire référence à aucune valeur, comme True, False ou 100.

La deuxième solution est en fait la traduction directe de quelque chose que nous pourrions écrire dans BNF:

var ::= <string> 
term ::= λ <var>. <term> | <term> <term> | <var> 

Et donc il n'y a rien de mal avec elle.

Answer 2

Qu'est-ce que vous voulez exactement est d'avoir un certain type comme

data Expr 
    = Atomic Variable 
    | Abstract Expr Expr 
    | Application Expr Expr 

Mais contraindre premier Expr dans Abstract constructeur à seulement Atomic. Il n'y a pas de moyen simple de le faire dans Haskell car la valeur d'un type peut être créée par n'importe quel constructeur de ce type. La seule approche consiste donc à créer un alias de type ou de type de données distinct pour le type existant (comme votre alias de type Variable) et à y insérer toute la logique courante. Votre solution avec Variable semble très bien pour moi.

Mais. Vous pouvez utiliser d'autres fonctionnalités avancées dans Haskell pour atteindre votre objectif de manière différente. Vous pouvez vous inspirer du paquet glambda qui utilise GADT pour créer un calcul lambda typé.Voir aussi cette réponse: https://stackoverflow.com/a/39931015/2900502

je peux venir avec une solution à côté de vous atteindre les objectifs minimaux (si vous voulez seulement limiter le premier argument de Abstract):

{-# LANGUAGE GADTs   #-} 
{-# LANGUAGE KindSignatures #-} 

data AtomicT 
data AbstractT 
data ApplicationT 

data Expr :: * -> * where 
    Atomic  :: String -> Expr AtomicT 
    Abstract :: Expr AtomicT -> Expr a -> Expr AbstractT 
    Application :: Expr a -> Expr b -> Expr ApplicationT 

Et exemple suivant, fonctionne très bien:

ex1 :: Expr AbstractT 
ex1 = Abstract (Atomic "x") (Atomic "x") 

Mais cet exemple ne compile pas en raison de non-concordance de type:

ex2 :: Expr AbstractT 
ex2 = Abstract ex1 ex1