imKiva 最近的时间轴更新
imKiva

imKiva

V2EX 第 336871 号会员,加入于 2018-07-29 07:36:09 +08:00
今日活跃度排名 777
imKiva 最近回复了
@GeruzoniAnsasu #8

> 列举的所有 !check <exp>:<type>我都没看到结论,即断言为真还是假,搞得我一头雾水

这个 check! 的意思是要求编译器进行类型检查,即 check <exp> against <type>,如果 <exp> 确实是 <type> 的 inhabitant (或者说 <exp> 具有 <type> 类型),则检查通过。否则应该产生一个类型错误。

> 本来还以为有什么可等性的定义方法,或者可等类型是什么特殊类型。然而似乎也不是。是说 Equal 这个三元组是一个抽象类型?我就搞不懂了如果「 Equal(X,Y,Z)三元组」

「相等类型」相关的内容非常复杂,与这门语言选择的类型论有关。我太菜了,可能回答不了这个问题。

> 那这样理解的话 Equal()也是一个泛型,List 的参数列表是类型,Equal 里却可以有表达式……为什么?规范是啥……

这是 dependent type (依值类型),即类型可以依赖值。在 DT 的语言中,类型和值并没有什么不同。

> ctrl+f 了一下没看到 return induction ( 这个 induction 函数是哪讲的就放弃了

这个 induction 可以视为「模式匹配」,是编译器内建的操作(比如 rust 的 match ),是一种对归纳数据类型(比如 Nat 类型)归纳证明的一种方法。你可以理解为「分类讨论」。

> 文档全文也没看出来如何 prove something ,甚至如何定义公理都没讲明白

文档这一部分: https://readonly.link/manuals/gitlab.com/cicada-lang/cicada/-/datatype/01.1-proving-theorems-about-nat.md
以加法交换律为例展示了证明,即:add_commute(x: Nat, y: Nat,): Equal(Nat, add(x, y), add(y, x))
这个函数签名的意思是:对于任意两个自然数 x y ,都有 x + y = y + x
而这个函数的 body 就是对这个命题的证明。
关于这个问题,更多可以参考: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
45 天前
回复了 Vindroid 创建的主题 Linux WSL debian vim 编辑文件不显示文本内容
换个终端试试
75 天前
回复了 Higurashi 创建的主题 问与答 NaN 的二进制形式
`Float.intBitsToFloat` 的[文档]( https://docs.oracle.com/javase/8/docs/api/java/lang/Float.html#intBitsToFloat-int-)中有一句:`If the argument is any value in the range 0x7f800001 through 0x7fffffff or in 0xff800001 through 0xffffffff, the result is a NaN.`

`Float.floatToIntBits` 的[文档]( https://docs.oracle.com/javase/8/docs/api/java/lang/Float.html#floatToIntBits-float-)中有一句:`If the argument is NaN, the result is 0x7fc00000.`
我写过一个用快捷键在终端的 emacs 里打开的,楼主可以自己修改一下。双击打开的我也没找到什么好办法
150 天前
回复了 icemanpro 创建的主题 C++ 如何将 list 的值传给函数的可变参数?
这个问题感觉最方便的办法是用 libffi,之前遇到同样问题的时候想了很久,因为需要支持多种 arch,所以最后选择了 libffi
PYJK7RE44MHF 已经使用,谢谢楼主~
Process#waitFor() 返回的就是退出状态
关于   ·   帮助文档   ·   API   ·   FAQ   ·   我们的愿景   ·   广告投放   ·   感谢   ·   实用小工具   ·   1072 人在线   最高记录 5497   ·     Select Language
创意工作者们的社区
World is powered by solitude
VERSION: 3.9.8.5 · 13ms · UTC 23:46 · PVG 07:46 · LAX 15:46 · JFK 18:46
Developed with CodeLauncher
♥ Do have faith in what you're doing.