34 votes

Est-il possible de représenter une syntaxe abstraite d'ordre supérieur en Rust ?

En Haskell, il est très facile d'écrire types de données algébriques (ADT) avec des fonctions. Cela nous permet d'écrire des interprètes qui s'appuient sur les fonctions natives pour les substitutions, c'est-à-dire qu'un syntaxe abstraite d'ordre supérieur (HOAS) qui est connu pour être très efficace. Par exemple, voici un simple interpréteur de -calculs utilisant cette technique :

data Term
  = Hol Term
  | Var Int
  | Lam (Term -> Term)
  | App Term Term

pretty :: Term -> String
pretty = go 0 where
  go lvl term = case term of
    Hol hol     -> go lvl hol 
    Var idx     -> "x" ++ show idx
    Lam bod     -> "x" ++ show lvl ++ ". " ++ go (lvl+1) (bod (Hol (Var lvl)))
    App fun arg -> "(" ++ go lvl fun ++ " " ++ go lvl arg ++ ")"

reduce :: Term -> Term
reduce (Hol hol)     = hol
reduce (Var idx)     = Var idx
reduce (Lam bod)     = Lam (\v -> reduce (bod v))
reduce (App fun arg) = case reduce fun of
  Hol fhol      -> App (Hol fhol) (reduce arg)
  Var fidx      -> App (Var fidx) (reduce arg)
  Lam fbod      -> fbod (reduce arg)
  App ffun farg -> App (App ffun farg) (reduce arg)

main :: IO ()
main
  = putStrLn . pretty . reduce
  $ App
    (Lam$ \x -> App x x)
    (Lam$ \s -> Lam$ \z -> App s (App s (App s z)))

Remarquez comment les fonctions natives ont été utilisées plutôt que les indices de Bruijn. Cela rend l'interpréteur considérablement plus rapide qu'il ne le serait si nous substituions les applications manuellement.

Je suis conscient que Rust a des fermetures et beaucoup de Fn() mais je ne suis pas sûr qu'ils fonctionnent exactement comme les fermetures Haskell dans cette situation, et encore moins comment exprimer ce programme étant donné la nature bas niveau de Rust. Est-il possible de représenter HOAS en Rust ? Comment le Term être représenté ?

0 votes

Qu'est-ce qui vous fait penser que ce ne serait pas possible ? Après tout, Rust est Turing Complete...

1 votes

@MatthieuM. c'est no possible sur une machine de Turing, car celle-ci n'a aucune notion de "fonctions natives". Vous ne pourriez que l'émuler, mais cela nécessiterait quelque chose comme les indices de De Bruijn mentionnés dans la question.

3 votes

@MatthieuM. La complétude de Turing signifie qu'il peut reproduire tout comportement d'entrée-sortie qu'une machine de Turing peut avoir. Cela ne signifie pas que le langage peut exprimer directement des concepts de haut niveau. Par exemple, le C n'a pas de fermetures natives (même s'il peut être utilisé pour écrire un interprète Rust, qui a des fermetures). Rust n'a pas de types dépendants (même s'il peut interpréter Agda qui en a).

26voto

yzb3 Points 426

En tant que fan du lambda calculus, j'ai décidé de tenter l'expérience et c'est effectivement possible, bien que ce soit un peu moins évident qu'en Haskell ( lien vers l'aire de jeux ):

use std::rc::Rc;
use Term::*;

#[derive(Clone)]
enum Term {
    Hol(Box<Term>),
    Var(usize),
    Lam(Rc<dyn Fn(Term) -> Term>),
    App(Box<Term>, Box<Term>),
}

impl Term {
    fn app(t1: Term, t2: Term) -> Self {
        App(Box::new(t1), Box::new(t2))
    }

    fn lam<F: Fn(Term) -> Term + 'static>(f: F) -> Self {
        Lam(Rc::new(f))
    }

    fn hol(t: Term) -> Self {
        Hol(Box::new(t))
    }
}

fn pretty(term: Term) -> String {
    fn go(lvl: usize, term: Term) -> String {
        match term {
            Hol(hol) => go(lvl, *hol),
            Var(idx) => format!("x{}", idx),
            Lam(bod) => format!("x{}. {}", lvl, go(lvl + 1, bod(Term::hol(Var(lvl))))),
            App(fun, arg) => format!("({} {})", go(lvl, *fun), go(lvl, *arg)),
        }
    }

    go(0, term)
}

fn reduce(term: Term) -> Term {
    match term {
        Hol(hol) => *hol,
        Var(idx) => Var(idx),
        Lam(bod) => Term::lam(move |v| reduce(bod(v))),
        App(fun, arg) => match reduce(*fun) {
            Hol(fhol) => Term::app(Hol(fhol), reduce(*arg)),
            Var(fidx) => Term::app(Var(fidx), reduce(*arg)),
            Lam(fbod) => fbod(reduce(*arg)),
            App(ffun, farg) => Term::app(Term::app(*ffun, *farg), reduce(*arg)),
        },
    }
}

fn main() {
    // (x. x x) (s. z. s (s (s z)))
    let term1 = Term::app(
        Term::lam(|x| Term::app(x.clone(), x.clone())), 
        Term::lam(|s| Term::lam(move |z| 
            Term::app(
                s.clone(),
                Term::app(
                    s.clone(),
                    Term::app(
                        s.clone(),
                        z.clone()
    ))))));

    // b. t. f. b t f
    let term2 = Term::lam(|b| Term::lam(move |t| 
        Term::lam({
            let b = b.clone(); // necessary to satisfy the borrow checker
            move |f| Term::app(Term::app(b.clone(), t.clone()), f)
        })
    ));

    println!("{}", pretty(reduce(term1))); // x0. x1. (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1)))))))))))))))))))))))))))
    println!("{}", pretty(reduce(term2))); // x0. x1. x2. ((x0 x1) x2)
}

Merci à BurntSushi5 pour la suggestion d'utiliser Rc que j'oublie toujours d'exister et à Shepmaster pour avoir suggéré de supprimer les éléments inutiles Box sous Rc en Lam et comment satisfaire le vérificateur d'emprunts en plus longtemps Lam chaînes.

4 votes

Vous pouvez satisfaire Clone en utilisant le comptage de référence : play.rust-lang.org/ --- Je pense que ce code pourrait être nettoyé en grande partie à l'aide de quelques constructeurs pratiques au lieu d'utiliser des constructeurs de valeur directement partout.

0 votes

Impressionnant ! Je n'espérais pas une réponse aussi complète, mais j'espère qu'elle deviendra une référence pour tous ceux qui essaient de faire du HOAS en Rust. Il utilise en effet de nombreuses fonctionnalités dont je n'avais pas connaissance. Juste une précision : comment reproduirais-tu Lam$ \a -> Lam$ \b -> Lam$ \c -> c ? J'ai essayé Term::lam(|a| Term::lam(move |b| Term::lam(move |c| c))) mais je reçois une erreur liée à la move .

0 votes

@MaiaVictor êtes-vous sûr ? Je viens juste d'essayer votre code exact avec l'implémentation ci-dessus et j'obtiens x0. x1. x2. x2 : lien vers l'aire de jeux .

5voto

Earth Engine Points 1795

En solution acceptée utilise Rc pour créer une fermeture allouée au tas clonable.

Techniquement parlant, ce n'est pas nécessaire car il n'y a pas de comptage de références à l'exécution. Tout ce dont nous avons besoin est une fermeture en tant qu'objet de trait et qui est également clonable.

Cependant, Rust 1.29.2 ne nous permet pas d'avoir des choses comme dyn Clone + FnOnce(Term) -> Term Cette restriction pourrait être assouplie à l'avenir. La restriction comporte deux facteurs : Clone n'est pas sûr pour les objets (ce qui ne sera probablement pas assoupli) et si nous combinons deux traits ensemble, l'un d'entre eux doit être un trait automatique (ce qui peut être assoupli IMHO).

En attendant l'amélioration du langage, nous pouvons introduire un nouveau trait pour contourner ce problème :

// Combination of FnOnce(Term) -> Term and Clone
trait TermLam {
    // The FnOnce part, declared like an Fn, because we need object safety
    fn app(&self, t: Term) -> Term;
    // The Clone part, but we have to return sized objects 
    // (not Self either because of object safety), so it is in a box
    fn clone_box(&self) -> Box<dyn TermLam>;
}

// Blanket implementation for appropriate types
impl<F> TermLam for F
where
    F: 'static/*' highlighting fix */ + Clone + FnOnce(Term) -> Term
{
    // Note: when you have a Clone + FnOnce, you effectively have an Fn
    fn app(&self, t: Term) -> Term {
        (self.clone())(t)
    }

    fn clone_box(&self) -> Box<dyn TermLam> {
        Box::new(self.clone())
    }
}

// We can now clone the box
impl Clone for Box<dyn TermLam> {
    fn clone(&self) -> Self {
        self.clone_box()
    }
}

Nous pouvons alors supprimer la nécessité d'utiliser Rc .

#[derive(Clone)]
enum Term {
    Hol(Box<Term>),
    Var(usize),
    Lam(Box<dyn TermLam>),
    App(Box<Term>, Box<Term>),
}

impl Term {
    fn app(t1: Term, t2: Term) -> Self {
        App(Box::new(t1), Box::new(t2))
    }

    fn lam<F>(f: F) -> Self
    where
       F: 'static/*' highlighting fix */ + Clone + FnOnce(Term) -> Term        
    {
        Lam(Box::new(f))
    }

    fn hol(t: Term) -> Self {
        Hol(Box::new(t))
    }
}

fn pretty(term: Term) -> String {
    fn go(lvl: usize, term: Term) -> String {
        match term {
            Hol(hol) => go(lvl, *hol),
            Var(idx) => format!("x{}", idx),
            Lam(bod) => format!("x{}. {}", lvl, go(lvl + 1, bod.app(Term::hol(Var(lvl))))),
            App(fun, arg) => format!("({} {})", go(lvl, *fun), go(lvl, *arg)),
        }
    }

    go(0, term)
}

fn reduce(term: Term) -> Term {
    match term {
        Hol(hol) => *hol,
        Var(idx) => Var(idx),
        Lam(bod) => Term::lam(move |v| reduce(bod.app(v))),
        App(fun, arg) => match reduce(*fun) {
            Hol(fhol) => Term::app(Hol(fhol), reduce(*arg)),
            Var(fidx) => Term::app(Var(fidx), reduce(*arg)),
            Lam(fbod) => fbod.app(reduce(*arg)),
            App(ffun, farg) => Term::app(Term::app(*ffun, *farg), reduce(*arg)),
        },
    }
}

fn main() {
    // (x. x x) (s. z. s (s (s z)))
    let term1 = Term::app(
        Term::lam(|x| Term::app(x.clone(), x.clone())),
        Term::lam(|s| {
            Term::lam(move |z| {
                Term::app(
                    s.clone(),
                    Term::app(s.clone(), Term::app(s.clone(), z.clone())),
                )
            })
        }),
    );

    // b. t. f. b t f
    let term2 = Term::lam(|b| {
        Term::lam(move |t| {
            Term::lam({
                //let b = b.clone(); No longer necessary for Rust 1.29.2
                move |f| Term::app(Term::app(b.clone(), t.clone()), f)
            })
        })
    });

    println!("{}", pretty(reduce(term1))); // x0. x1. (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1)))))))))))))))))))))))))))
    println!("{}", pretty(reduce(term2))); // x0. x1. x2. ((x0 x1) x2)
}

C'est la voie originale que l'autre réponse a tenté, que l'auteur n'a pas pu résoudre.

Optimisez !

Rust est connu pour obtenir des performances sans sacrifier la sécurité. L'implémentation ci-dessus, cependant, passe toujours Term par valeur et ont beaucoup d'inutiles clone de sorte que certaines optimisations peuvent être effectuées.

De plus, la manière standard de stringifier un élément de données Rust est d'utiliser la balise Display trait. Alors faisons en sorte qu'ils soient corrects !

use std::fmt::{Display, Error, Formatter};
use Term::*;

// Combination of FnOnce(Term) -> Term and Clone
trait TermLam {
    // The FnOnce part, declared like an Fn, because we need object safety
    fn app(&self, t: Term) -> Term;
    // The Clone part, but we have to return sized objects
    // (not Self either because of object safety), so it is in a box
    fn clone_box(&self) -> Box<dyn TermLam>;
}

// Blanket implementation for appropriate types
impl<F> TermLam for F
where
    F: 'static/*' highlighting fix */ + Clone + FnOnce(Term) -> Term,
{
    // Note: when you have a Clone + FnOnce, you effectively have an Fn
    fn app(&self, t: Term) -> Term {
        (self.clone())(t)
    }

    fn clone_box(&self) -> Box<dyn TermLam> {
        Box::new(self.clone())
    }
}

// We can now clone the box
impl Clone for Box<dyn TermLam> {
    fn clone(&self) -> Self {
        self.clone_box()
    }
}

#[derive(Clone)]
enum Term {
    Hol(Box<Term>),
    Var(usize),
    Lam(Box<dyn TermLam>),
    App(Box<Term>, Box<Term>),
}

impl Term {
    fn app(t1: Term, t2: Term) -> Self {
        App(Box::new(t1), Box::new(t2))
    }

    fn lam<F>(f: F) -> Self
    where
        F: 'static/*' highlighting fix */ + Clone + FnOnce(Term) -> Term,
    {
        Lam(Box::new(f))
    }

    fn hol(t: Term) -> Self {
        Hol(Box::new(t))
    }

    // `reduce` is now a by-reference method
    fn reduce(&self) -> Term {
        match self {
            Hol(_) => self.clone(),
            Var(_) => self.clone(),
            Lam(bod) => {
                let bod = bod.clone();
                Term::lam(move |v| bod.app(v).reduce())
            },
            // We reuse the reduced object when possible,
            // to avoid unnecessary clone.
            App(fun, arg) => match fun.reduce() {
                other @ Hol(_) => Term::app(other, arg.reduce()),
                other @ Var(_) => Term::app(other, arg.reduce()),
                Lam(fbod) => fbod.app(arg.reduce()),
                other @ App(_, _) => Term::app(other, arg.reduce()),
            },
        }
    }
}
//The standard way of `pretty` is `Display`
impl Display for Term {
    fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
        // As the API is different from `pretty`, the way we do recursion is
        // a bit different as well
        struct LvlTerm<'a>(usize, &'a Term);
        impl<'a> Display for LvlTerm<'a> {
            fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
                match self {
                    LvlTerm(lvl, Hol(hol)) => write!(fmt, "{}", LvlTerm(*lvl, hol)),
                    LvlTerm(_, Var(idx)) => write!(fmt, "x{}", idx),
                    LvlTerm(lvl, Lam(bod)) => write!(
                        fmt,
                        "x{}. {}",
                        *lvl,
                        LvlTerm(*lvl + 1, &bod.app(Term::hol(Var(*lvl))))
                    ),
                    LvlTerm(lvl, App(fun, arg)) => {
                        write!(fmt, "({} {})", LvlTerm(*lvl, fun), LvlTerm(*lvl, arg))
                    }
                }
            }
        }
        write!(fmt, "{}", LvlTerm(0, self))
    }
}

fn main() {
    // In general, if you need to use a value n+1 times, you need to
    / call clone it n times. You don't have to clone it in the last use.
    // (x. x x) (s. z. s (s (s z)))
    let term1 = Term::app(
        Term::lam(|x| Term::app(x.clone(), x)),
        Term::lam(|s| {
            Term::lam(move |z| Term::app(s.clone(), Term::app(s.clone(), Term::app(s, z))))
        }),
    );

    // No clone is required if all values are used exactly once.
    // b. t. f. b t f
    let term2 =
        Term::lam(|b| Term::lam(move |t| Term::lam(move |f| Term::app(Term::app(b, t), f))));

    println!("{}", term1.reduce()); // x0. x1. (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1)))))))))))))))))))))))))))
    println!("{}", term2.reduce()); // x0. x1. x2. ((x0 x1) x2)
}

Terrain de jeux

Nous pouvons voir que le code ci-dessus peut être encore simplifié : comme les bras de correspondance dans reduce ont une duplication de code, nous pouvons les réduire ensemble. Cependant, comme le but de cette réponse est de démontrer que l'on fait les choses de la MÊME façon que le code Haskell de la question, nous avons laissé cela tel quel.

De plus, en exigeant seulement que les fermetures soient FnOnce pas Fn Dans le site d'utilisation, nous avons assoupli l'obligation de cloner toutes les variables uniquement lorsqu'elles sont utilisées plus d'une fois. Le compromis est que chaque fois que la fermeture a été appelée, toutes les variables qu'elle capture seront clonées. Il est difficile de dire laquelle est la meilleure jusqu'à ce qu'un profilage soit effectué ; je choisis donc celle qui donne au code une meilleure apparence.

Encore une fois, Rust rend ces décisions explicites et garde les différences de choix à l'esprit, c'est bien !

0 votes

@shepmaster Je préfère personnellement (FnOnce(Term) -> Term) + Clone + 'static que (FnOnce(Term) -> Term + Clone + 'static) comme l'indique clairement le premier FnOnce(Term) -> Term est un trait unique, et ne peut pas être compris comme FnOnce(Term) -> (Term + Clone) + 'static ou quelque chose comme ça.

1 votes

Vous pouvez le changer à nouveau, c'est juste ce que rustfmt corrige. J'ai tendance à les mettre avant le Fn : Clone + FnOnce.. . Vous devriez ouvrir un problème de rustfmt si vous pensez qu'il rend votre code moins clair.

0 votes

Vous avez donné une très bonne idée. En général, lorsque la situation n'est pas ambiguë, il est préférable d'écrire le trait principal en premier, puis les traits de décoration, puis les durées de vie. Toutefois, si les choses deviennent confuses, il n'y a aucune raison de ne pas utiliser l'inverse.

Prograide.com

Prograide est une communauté de développeurs qui cherche à élargir la connaissance de la programmation au-delà de l'anglais.
Pour cela nous avons les plus grands doutes résolus en français et vous pouvez aussi poser vos propres questions ou résoudre celles des autres.

Powered by:

X