我在Coq的SSReflect扩展中找到了两个公约,这些公约看起来特别有用,但我还没有看到在新的依赖类型语言(Lean,Agda,Idris)中广泛采用的公约.
首先,可能的谓词表示为布尔返回函数,而不是归纳定义的数据类型.这默认带来可判定性,通过计算开辟了更多的证明机会,并通过避免校对引擎携带大量证明条件来提高检查性能.我看到的主要缺点是需要使用反射词来在证明时操纵这些布尔谓词.
其次,具有不变量的数据类型被定义为包含简单数据类型和不变量证明的从属记录.例如,固定长度序列在SSReflect中定义,如:
Structure tuple_of : Type := Tuple {tval :> seq T; _ : size tval == n}.
A seq和证明该序列的长度是一定值.这与Idris如何定义此类型相反:
data Vect : (len : Nat) -> (elem : Type) -> Type
一种依赖类型的数据结构,其中不变量是其类型的一部分.SSReflect方法的一个优点是它允许重用,因此例如许多定义的函数seq和关于它们的证明仍然可以使用tuple(通过对底层操作seq),而使用Idris的方法函数reverse,append等等需要被重写Vect.Lean实际上在其标准库中具有等效的SSReflect样式vector,但它也具有Idris样式array,似乎在运行时具有优化的实现.
一本面向SSReflect的书甚至声称Vect n A风格方法是反模式:
依赖类型语言和Coq中的常见反模式特别是将这样的代数属性编码到数据类型和函数本身的定义中(这种方法的规范示例是长度索引列表).虽然这种方法看起来很吸引人,因为它展示了依赖类型捕获它们的数据类型和函数的某些属性的能力,但它本质上是不可扩展的,因为总会有另一个感兴趣的属性,这是设计者没有预见到的.数据类型/函数的数据,因此它必须被编码为外部事实.这就是为什么我们提倡这种方法,其中数据类型和函数被定义为尽可能接近程序员定义的方式,并且它们的所有必要属性都是分开证明的.
因此,我的问题是,为什么没有更广泛地采用这些方法.我缺少哪些缺点,或者它们的优势在具有比Coq更好支持依赖模式匹配的语言中不那么重要？
如果我有以下OCaml功能:
let myFun = CCVector.map ((+) 1);;
它在Utop中运行良好,Merlin不会将其标记为编译错误.但是,当我尝试编译它时,我收到以下错误:
错误:此表达式的类型, (int,'_ a)CCVector.t - >(int,'_ b)CCVector.t,包含无法泛化的类型变量
如果我eta-expand它然后它编译好:
let myFun foo = CCVector.map ((+) 1) foo;;
所以我想知道为什么它不能以eta-reduced形式编译,以及为什么eta-reduced表单似乎在顶层(Utop)中工作但在编译时不起作用？
哦,CCVector的文档就在这里.'_a部分可以是`RO或`RW,具体取决于它是只读还是可变.
Go语言有一个select语句,可用于轮询多个通道并执行特定操作,具体取决于哪个通道首先是非空的.
例如
select {
case a := <- chanA:
foo(a)
case b := <- chanB:
baz(b)
case c := <- chanC:
bar(c)
}
这将等到chanA,chanB或者chanC非空,然后如果例如chanB非空,它将读取chanB并存储结果b,然后调用baz(b).default:还可以添加一个子句,这意味着select语句不会在通道上等待,而是default在所有通道都为空的情况下执行该子句.
TChan在Haskell中为STM实现这样的事情的最佳方法是什么？它可以通过if-else链天真地完成:检查每个chan isEmptyChan,如果它不是空的,那么从它读取并调用适当的函数,或者retry如果所有通道都是空的则调用.我想知道是否会有更优雅/惯用的方式来做到这一点？
请注意,Go的select语句在其情况下也可以包含send语句,并且只有在其通道为空时才会完成send语句.如果功能也可以重复,那将是很好的,虽然我不确定是否会有一种优雅的方式.
只是略微相关,但我刚注意到的东西,我不知道在哪里发布它:在描述中的Control.Monad.STM页面上有一个拼写错误retry:
"该实现可能会阻止该线程,直到它读取的其中一个TVAR已被更新."
Standard Haskell是惰性评估的，因此if myCondition then someValue else doSomeLargeComputation x y z将避免评估doSomeLargeComputation x y z是否myCondition为真。我的问题是，如果启用语言扩展，XStrict那么doSomeLargeComputation x y z即使myCondition为true，现在也将对其进行评估？
如果是这样，除了明确标记doSomeLargeComputation x y z为惰性以外，是否还有控制流构造可用于避免对其进行计算（例如，严格语言中的if语句短路）？
他们似乎服务于类似的目的.到目前为止我注意到的一个区别是,虽然Program Fixpoint会接受一个复合测量{measure (length l1 + length l2) },但Function似乎拒绝这个并且只会允许{measure length l1}.
是否Program Fixpoint比Function它们更强大,或者它们更适合不同的用例？
假设我有两个归纳定义的数据类型:
Inductive list1 (A : Type) : Type :=
| nil1 : list1 A
| cons1 : A -> list1 A -> list1 A.
和
Inductive list2 (A : Type) : Type :=
| nil2 : list2 A
| cons2 : A -> list2 A -> list2 A.
对于任何P (list1 a)我应该能够以构造P (list2 a),通过施加予用于构造完全相同的方法P (list1 a),只是用nil1与nil2,list1与list2和cons1用cons2.类似地,任何list1 a作为参数的函数都可以扩展为a list2 a.
是否有类型系统允许我以这种方式说两个具有相同形状的数据类型(具有相同形状的构造函数),并证明 …
我正在使用 Haskell Stack 包管理器的 2.1.1 版。
清华大学在中国防火墙后面提供了一个 Hackage 镜像，如https://mirrors.tuna.tsinghua.edu.cn/help/hackage/ 所述。
但是，当我按照这些说明进行操作时，添加
package-indices:
- name: Tsinghua
download-prefix: http://mirrors.tuna.tsinghua.edu.cn/hackage/package/
http: http://mirrors.tuna.tsinghua.edu.cn/hackage/00-index.tar.gz
hackage-security:
keyids:
- 0a5c7ea47cd1b15f01f5f51a33adda7e655bc0f0b0615baa8e271f4c3351e21d
- 1ea9ba32c526d1cc91ab5e5bd364ec5e9e8cb67179a471872f6e26f0ae773d42
- 280b10153a522681163658cb49f632cde3f38d768b736ddbc901d99a1a772833
- 2a96b1889dc221c17296fcc2bb34b908ca9734376f0f361660200935916ef201
- 2c6c3627bd6c982990239487f1abd02e08a02e6cf16edb105a8012d444d870c3
- 51f0161b906011b52c6613376b1ae937670da69322113a246a09f807c62f6921
- 772e9f4c7db33d251d5c6e357199c819e569d130857dc225549b40845ff0890d
- aa315286e6ad281ad61182235533c41e806e5a787e0b6d1e7eef3f09d137d2e9
- fe331502606802feac15e514d9b9ea83fee8b6ffef71335479a2e68d84adc6b0
key-threshold: 3 # number of keys required
# ignore expiration date, see https://github.com/commercialhaskell/stack/pull/4614
ignore-expiry: yes
到~/.stack/config.yml，然后当我stack run在我的项目目录中运行时，我看到：
惊天动地文件信息没有发现aeson-1.4.2.0@sha256：8166752a9669597db375343df19805069595fed9c613f98504e418849f40fe18,7007，更新所选的镜像 http://mirrors.tuna.tsinghua.edu.cn/hackage/package/下载根未能进行反序列化/root.json：格式不正确：（第 1 行，第 1 列）：意外的“<”需要空格或 JSON 值
它还有一个 Stackage 镜子；我尝试通过添加resolver: https://mirrors.tuna.tsinghua.edu.cn/stackage/lts-haskell/lts-13.25.yaml到stack.yaml我的项目来更改 Stackage 解析器，但失败了：
从 …
我正在使用Mioco。mio::net::tcp::TcpStream没有实现Clone，所以似乎不可能TcpStream跨多个线程/协程共享 a （或者如果可能，我不确定如何；我对 Rust 很陌生）。因此，我假设要同时读取/写入单个TcpStream，有必要使用单个协程来进行读取和写入。
为了避免在传入数据不频繁时无限期地阻塞读取，似乎有必要在从TcpStream. std::net::TcpStream有set_read_timeout实现这一目标，但我找不到等效的mio::net::tcp::TcpStream. 我该怎么办？或者有没有办法TcpStream在多个协程之间共享 mio ，避免超时的需要？
我想覆盖 stdenv 以mkShell使用 gcc10Stdenv。我查看了https://nixos.wiki/wiki/Using_Clang_instead_of_GCCmkShell ，它提供了覆盖 stdenv 的说明，但它没有描述在不引用任何特定包的情况下制作 shell 时如何执行此操作（仅适用于“在现有包上使用 Nix CLI”）。
我的问题是是否可以在没有现有包的情况下覆盖 mkShell 的 stdenv ？如果是这样，怎么办？