Idris 中的准引用概述

Question

直到遇到 some tests in the test suite，我才意识到 Idris 有一个准引号。

这是 REPL 中的一个简短示例：

Idris> :module Language.Reflection
Idris> `(S Z)
App (P (DCon 1 1)
       (NS (UN "S") ["Nat", "Prelude"])
       (Bind (MN 0 "_t")
             (Pi (P (TCon 0 0) (NS (UN "Nat") ["Nat", "Prelude"]) Erased)
                 (TType (UVar "./Prelude/Nat.idr" 22)))
             (P (TCon 0 0) (NS (UN "Nat") ["Nat", "Prelude"]) Erased)))
    (P (DCon 0 0)
       (NS (UN "Z") ["Nat", "Prelude"])
       (P (TCon 0 0) (NS (UN "Nat") ["Nat", "Prelude"]) Erased)) : TT

我想了解这是怎么回事。简要概述 and/or 一些参考资料将不胜感激！

Answer 1

论文 Elaborator Reflection: Extending Idris in Idris 定义了 Idris 核心语言的 Idris 表示 TT:

The core language is represented by two separate data types: Raw and TT. Raw is used to represent terms that are to be submitted to the type checker, while TT represents terms produced by the type checker.

图3给出了Raw和TT的如下轮廓：

-- Variable names
data TTName = ...

-- Constants
data Const = I Int | Str String | ...

-- Binders
data Binder : (tmTy : Type) -> Type where
    Lam : (ty : a) -> Binder a
    Pi : (ty, kind : a) -> Binder a
    Let : (ty, val : a) -> Binder a
    PVar : (ty : a) -> Binder a
    Hole : (ty : a) -> Binder a
    Guess : (ty, val : a) -> Binder a

-- Terms which have not yet been typechecked
data Raw = Var TTName
    | RBind TTName (Binder Raw) Raw
    | RApp Raw Raw
    | RType
    | RConstant Const

-- Well typed, de Bruijn indexed terms
data TT = P NameType TTName TT
    | V Int
    | Bind TTName (Binder TT) TT
    | App TT TT
    | TConst Const
    | TType TTUExp

它还引用了描述准报价机制的论文Type-Directed Elaboration of Quasiquotations。

Idris 中的准引用概述

Overview of quasiquotation in Idris

reflection

idris