记录望远镜中的“让”答案

【问题标题】：'let' in record telescope记录望远镜中的“让”
【发布时间】：2014-08-19 17:42:46
【问题描述】：

是否允许在 Agda 记录望远镜内部使用类似 let 或 where 的子句，以便为望远镜引入本地定义？

This discussion 建议以下内容应该是合法的：

record _×_ (let ⋆ = Set) (A B : ⋆) : Set where
   constructor _,_
   field
      fst : A
      snd : B

This change request 描述的语法略有不同：

record _×_ (let ⋆ = Set in (A B : ⋆)) : Set where
   constructor _,_
   field
      fst : A
      snd : B

（问题标记为Accepted，好像有补丁，不知道有没有正式合并。）

但是 Agda 2.4.0.2 不接受其中任何一个。

在冒号之后，我似乎可以使用let，正如我所期望的那样：

record _×_ (A B : Set) : let ⋆ = Set in ⋆ where
   constructor _,_
   field
      fst : A
      snd : B

有什么原因我可以在记录声明的望远镜部分使用let（在给出它的索引时），但在给出它的参数时不能？

【问题讨论】：

标签： record let agda

【解决方案1】：

来自 2.4.0 的发行说明：

望远镜让：望远镜现在接受本地绑定模块、函数类型和lambda-abstractions。

所以不，你提到的补丁还没有被合并（还）。

您可以在最后一个代码 sn-p 中使用let 的原因是您在表达式中使用它。换句话说，声明的索引部分不是望远镜。

【讨论】：

好的，谢谢。这对我目前正在做的事情来说可能是一种痛苦，除非我能找到另一种方式来制定事情。（也许我可以使用一个模块来做一些。）感谢您阐明“望远镜”的含义。
您可以在模块内定义类型并将参数移动到模块望远镜。我不知道这两者之间有什么重大区别。另外，我想我并没有把望远镜的含义说得那么清楚，让我纠正一下：望远镜只是(a1 a2 ... an : T1) ... (b1 b2 ... bn : T2) 的一部分。
再次感谢。我已接受您的回答，但将基于模块的解决方案作为另一个答案。

【解决方案2】：

以下是使用本地模块模拟 let 的方法：

private
   module Dummy (let ⋆ = Set) where
      record _×_  (A B : ⋆) : Set where
         constructor _,_
         field
            fst : A
            snd : B
open Dummy

更好的是，通过使用匿名模块，open Dummy 可以省略：

module _ (let ⋆ = Set) where
   record _×_  (A B : ⋆) : Set where
      constructor _,_
      field
         fst : A
         snd : B

（如Agda 2.3.2 release notes中所解释，后者本质上等同于前者。）

【讨论】：

如果你想使用来自其他全局模块（即来自另一个文件）的_×_，你应该公开打开模块：open Dummy public。据我所知，这（可悲）不能用于匿名模块。