fumeboy

你们好,关于论坛的设计,有几个纠结的地方,希望讨论一下?

问题是很简单的:用户创建帖子后要不要使他可以再次编辑、删除自己的帖子呢?如果这样做的话,可能会令其他参与这个帖子的用户产生困惑

Colliot

在 WebStorm 中如何根据文件名对导出变量名进行自动补全?

如果我新建了一个文件,比如叫 SomeEntity.ts,那么当我打出 export class 后,它就会提供直接补全类名为 SomeEntity 的选项。但是如果我是用 export const,就不会有这样的提示。

是否可以通过某种开关打开这样的提示呢?

ring3

容器云在网站开发中有哪些应用场景?

纯好奇 净土在开发过程中有没有用到相关技术呢

ice1000

CuTT的comp为什么要设计成“对几个Interval模式匹配”的样子?

为什么我们不能提供类似(a == b) -> (b == c) -> (a == c)comp,而是要做成对Interval的值匹配的样子呢?再者,Interval是用De Morgan Algebra而不是Boolean Algebra的根本原因不就是它们其实不是端点、不能被模式匹配吗?为何我们提供的comp却是这么设计的(Agda, CubicalTT, RedPrl)? 题主是初学者,还没看CuTT的论文,求各位不吝赐教

ice1000

可以在函数类型检查的时候使用case tree,然后在reduce的时候使用完整的pattern吗?

这是我的前面的问题的继续讨论:https://www.eliseos.org/en/epistemology/question/61

这样做的好处是,我们有了eliminator,totality可以很轻易地检查,但是同时也能保留term equal,不至于出现原问题中那个agda.readthedocs链接里面提到的情况。

Colliot

V8 虚拟机的模型是如何的?

为什么网上几乎找不到相关资料呢?如何整理出一堆可用的资料?

ice1000

Rust 能不能『把一个结构体的一个成员 move 出来然后马上补一个值进去』?

如题,目前我借助借用把成员的指针拿出来用的。

感觉这操作其实应该叫 swap……

ice1000

为什么我们不直接用 isomorphism 来 rewrite,而是引入 univalence?

为什么我们不能提供类似 (a == b) -> (b == c) -> (a == c)comp,而是要做成对 Interval 的值匹配的样子呢?再者,Interval 是用 De Morgan Algebra 而不是 Boolean Algebra 的根本原因不就是它们其实不是端点、不能被模式匹配吗?为何我们提供的 comp 却是这么设计的 (Agda, CubicalTT, RedPrl)?

题主是初学者,还没看 CuTT 的论文,求各位不吝赐教

ice1000

如何理解 Cubical Agda 的 Partial 类型?

似乎就是 comp 的返回类型?但是它里面那几个参数是什么意思呢?

可能因为 CubicalTT 语言里没有这个概念,因此题主感到有些困惑。

ice1000

HIT 中定义的 Path 是怎么参与运算的?

上下文: Cubical Type Theory

普通的 Path 我能理解,但是感觉 HIT 的 Path 还是和实际运算有些出入

YangKeao

在$\mathbb{R}^n$中n>4时,platonic solid只有4种?

在$n=3$时platonic solid有5种是大家都会证明的。 而在$n=4$时platonic solid有6种,在更大的时候只有4种,没有找到相关的资料,它们是如何证明的呢?

ice1000

既然模式匹配和 eliminator 在进行归纳证明时的能力相同,我们有没有把后者翻译为前者的算法?

Jesper Cockx说Agda的实现是不标准的。我们有没有一个形式化的方法可以把模式匹配翻译成eliminator呢?为什么Agda没有这么做,是因为它太垃圾了吗(就是其实能做但是就是没做的意思)?如果有,能不能适用于HIT(高阶归纳类型)的模式匹配呢?

ice1000

Core Language 中保留 Case Tree 有什么坏处?

其他做法是,生成并翻译成eliminator。 关键是,dependent pattern matching翻译成case tree能形式化吗? Case tree的定义参考Agda的文档及相关实现:

ice1000

如何快速理解相继式的含义?

尤其是类型论里面的那种,总是要看好一会才能明白啥意思。阅读这样的东西有什么技巧可言吗?

ice1000

如何理解initiality和finality?

我感觉我有点没搞懂initiality和finality。根据定义,它们分别是一个initial algebra能映射到所有algebra的性质和所有coalgebra能映射到一个final coalgebra的性质。那么,initial algebra的定义是随意的吗?是不是如果我有一堆isomorphic的algebra,它们任意一个都可以是initial algebra?

ice1000

如何理解最大和最小不动点呢?

我感觉我有点没搞懂gfp/lfp。根据定义,它们分别是最大的和最小的不动点,但是不动点一般都只有一个啊?如何看出最大最小的区别呢?什么情况下可以明显地观察到gfp/lfp的区别?

Colliot

如何正确地学习 nginx 配置?

众所周知,nginx 的配置很重要,但是它又很专门。所以我们应该如何入手呢?

Colliot

如何证明牛顿-科斯特公式中的系数和为 1?

牛顿-科斯特公式是说:

$$ \int_a^b f(x) \mathrm{d}x \approx \sum_{i=0}^n w_i\, f(x_i) $$

其中 $k=0, 1, \dots, n$,$w_i$ 是常数(就是问题中的系数,由 $n$ 的值決定),$x_k=a+k \frac{b-a}{n}$。

Colliot

为什么 `Array` 不是 `CallableFunction`?

考虑如下一段代码:

const a = Array(...Array(24));
const b = Array.apply(null, Array(24));

a 能被推导为 any[]b 却只能被推导为 any。我一开始以为是 TS 版本的问题,因为 TS 3.2 才开始支持 strictBindCallApply。但当我升级到 TS 3.2,b 的类型推导结果依然是 any

当我点进 Array.apply 方法的定义,我才发现它被解析到了 Functionapply 方法:

interface Function {
    /**
      * Calls the function, substituting the specified object for the this value of the function, and the specified array for the arguments of the function.
      * @param thisArg The object to be used as the this object.
      * @param argArray A set of arguments to be passed to the function.
      */
    apply(this: Function, thisArg: any, argArray?: any): any;
}

而能被正确推导的 apply,会解析到 CallableFunctionapply 方法:

interface CallableFunction extends Function {
    /**
      * Calls the function with the specified object as the this value and the elements of specified array as the arguments.
      * @param thisArg The object to be used as the this object.
      * @param args An array of argument values to be passed to the function.
      */
    apply<T, R>(this: (this: T) => R, thisArg: T): R;
    apply<T, A extends any[], R>(this: (this: T, ...args: A) => R, thisArg: T, args: A): R;
}

我好奇为什么 Array.apply 不会被解析到此,于是我将 Array 强转为 CallableFunction,发现它们竟然是不相容的,tsc 会提示:

The 'this' context of type 'CallableFunction' is not assignable to method's 'this' of type '(this: null, ...args: any[]) => {}'.
  Type 'CallableFunction' provides no match for the signature '(this: null, ...args: any[]): {}'.

那么,是什么理由导致它们不相容的呢?这样的行为背后有什么深意吗?

Home

Babel

Knowledge

Epistemology

Settings