Idris准报价概述

Question

直到我遇到测试套件中的一些测试，我才意识到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

我想知道这是怎么回事。简要的概述和/或一些参考将不胜感激！

Answer 1

本文定义了Idris核心语言TT的Idris表示。

核心语言由两种独立的数据类型表示：Raw和TT。Raw用于表示要提交给类型检查器的术语，而TT表示由类型检查器生成的术语。

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

-变量名称数据TTName =.-常数数据Const =I Int \ Str String .-绑定数据绑定器：(tmTy : Type) ->类型，其中Lam：(ty : a) -> Binder a Pi：(ty，种类: a) -> Binder a设：(ty，val : a) -> Binder a PVar：(ty : a) -> Binder a Hole：(ty : a) -> Binder a猜测：(ty，val:a)-> Binder a PVar：(ty:a)->Binder a Hole：(ty:a)->Binder a Pi：(ty，ty:a)->Binder a PVar：(ty:a)->Binder a Hole：(ty:a)->Binder a Pi：(ty，ty:a)->Binder a PVar：(ty:a)->Binder a Hole：(ty:a)->val : a) -> Binder a-尚未被键入的术语-数据Raw = Var TTName RBind TTName (Binder Raw)

文中还参考了描述准报价机制的论文http://davidchristiansen.dk/pubs/type-directed-elaboration-of-quasiquotations.pdf。