This means that if we write an Idris program to calculate a factorial by calling interp on eFac, the resulting definition will be specialised, partially evaluating away the interpreter: Int Interp : (env : Env gamma) -> (e : Expr gamma t) -> interpTy t (App (App eMult (App eFac (Op (-) x (Val 1)))) x)) If : Expr gamma TyBool -> Expr gamma a -> Expr gamma a -> Expr gamma aĮMult : Expr gamma (TyFun TyInt (TyFun TyInt TyInt))ĮFac = expr (\x => If (Op (=) x (Val 0))
Op : (interpTy a -> interpTy b -> interpTy c) -> Expr gamma a -> Expr gamma Lam : Expr (a :: gamma) t -> Expr gamma (TyFun a t)Īpp : Lazy (Expr gamma (TyFun a t)) -> Expr gamma a -> Expr gamma t That Idris feature is quite powerful, as shown at the bottom of that page it can even specialize away a little interpreter: data Expr : Vect n Ty -> Ty -> Type where In the Idris language if one function argument is annotated with (or more than one), and you call that function using a compile-time constant for that argument, the Idris compiler creates a partially evaluated (specialised) version of that function for that call point: In this post I present a feature that's not very important, I don't know if it can be added to a quite impure language as Rust, and I don't know if it's a good idea to have in Rust, but it looks nice in theory. In the next weeks/months I'll explain four features I'd like in Rust (and I think no one of them is a breaking change).
0 kommentar(er)
