Haskell AST mit rekursiven Typen

Question

Ich versuche gerade, einen Lambda-Kalkül-Löser zu bauen, und ich habe ein kleines Problem mit der Konstruktion der AST. Ein Lambda-Calculus Begriff wird induktiv definiert als:

1) Eine variable

2) Eine Lambda, eine Variable, ein Punkt und ein Lambda-Ausdruck.

3) Ein Träger, ein Lambda-Ausdruck, ein Lambda-Ausdruck und eine Halterung.

Was würde ich tun (und zunächst versucht), ist dies:

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

Jetzt offensichtlich das nicht funktioniert, da Variable kein Typ ist, und abstrakte Variable Expr erwartet Typen. Also meine hacky Lösung ist zu haben:

type Variable = String 

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

Nun ist dies wirklich ärgerlich, da ich nicht die Atomic Variable auf eigenem mögen, aber Abstrakte einen String statt einer ausdr nehmen. Gibt es eine Möglichkeit, das eleganter zu machen und es wie die erste Lösung zu machen?

Answer 1

Ihre erste Lösung ist nur eine fehlerhafte Definition ohne Bedeutung. Variable ist kein Typ, es ist ein Nullwert Konstruktor. Sie können in einer Typdefinition nicht auf Variable verweisen, so dass Sie nicht auf einen Wert wie True, False oder 100 verweisen können.

Die zweite Lösung ist die direkte Übersetzung von etwas in der Tat haben wir in BNF schreiben konnte:

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

Und so gibt es nichts zu beanstanden.

Answer 2

Was Sie genau wollen, ist eine Art wie

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

haben Aber zuerst Expr in Abstract Konstruktor beschränken nur Atomic zu sein. Es gibt keine direkte Möglichkeit, dies in Haskell zu tun, da der Wert eines Typs von jedem Konstruktor dieses Typs erstellt werden kann. Der einzige Ansatz besteht also darin, einen separaten Datentyp oder Typalias für den vorhandenen Typ (wie Ihren Aliasnamen Variable) zu erstellen und die gesamte allgemeine Logik darin zu verschieben. Ihre Lösung mit Variable scheint mir sehr ok zu sein.

Aber. Sie können einige andere erweiterte Funktionen in Haskell verwenden, um Ihr Ziel auf andere Weise zu erreichen. Sie können durch glambda Paket inspiriert werden, das GADT verwendet, um typisierte Lambda-Kalkül zu erstellen.Siehe auch diese Antwort: https://stackoverflow.com/a/39931015/2900502

ich mit der nächsten Lösung kommen können Sie minimale Ziele zu erreichen (wenn Sie nur erste Argument von Abstract einschränken wollen):

{-# 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 

Und nächstes Beispiel funktioniert gut:

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

Aber dieses Beispiel wird wegen Typenkonflikt nicht kompilieren:

ex2 :: Expr AbstractT 
ex2 = Abstract ex1 ex1