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[]): {}'.

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

Colliot

在 Rust 中如何处理 `match` 地狱?

在 Rust 中我们采用 Result<R, E> 的类型处理错误,这样(初学者)就特别容易出现错误处理嵌套地狱,比如如下一段利用 libgit2 读取一些 git repo 信息的代码:

    match Repository::open(first_arg) {
        Ok(repo) => {
//            println!("{:?}", repo);
            match repo.find_remote("origin") {
                Ok(mut origin) => {
                    println!("success!");
                    match repo.branches(Some(BranchType::Local)) {
                        Ok(branches) => {
                            for branch_result in branches {
                                match branch_result {
                                    Ok((branch, branch_type)) => {
                                        println!("Iterating at {:?}", branch.name());
                                        match branch.name() {
                                            Ok(Some(branch_name)) => {
                                                origin.fetch(&[branch_name], None, None);
                                            }
                                            _ => {
                                                println!("Error!")
                                            }
                                        }
                                    }
                                    Err(e) => {
                                        println!("{:?}", e)
                                    }
                                }
                            }
                        }
                        Err(e) => {
                            println!("{:?}", e)
                        }
                    }
                }
                Err(e) => {
                    println!("{:?}", e)
                }
            };

            match repo.remotes() {
                Ok(remotes) => {
                    for remote in remotes.iter() {
                        println!("{:?}", remote);
                    }
                }
                Err(e) => {
                    println!("{:?}", e);
                }
            };

            println!("hee");
        }
        Err(e) => panic!("failed to open: {}", e),
    };

每一层都进行 match,导致出现了极不可读的嵌套。

那么,正确的做法是什么呢?如上一段代码,优雅的写法是什么?

Colliot

Elasticsearch 有什么理论基础吗?

这里倒不是想问它的实现原理一类的,而是说,比如关系型数据库有关系代数作为理论基础,有各种范式的严格定义,那么 Elasticsearch 的建模有没有可以参考的理论呢?

Colliot

关于 `Function.prototype.call` 和 `Function.prototype.apply` 的速度快慢,到底有没有个定论?

有些人说它们之间有快慢差别;有些人认为没有,或者微不足道。

有没有一个从实验和原理上都非常详尽、坚实的结论和解释?

Colliot

为什么在 TS 里不可以 `import React from 'react'`?

为什么在 ES6 里可以

import React from 'react'

但是在 TypeScript 里一定要

import * as React from 'react'

而且更神奇的是,这两种看起来应该效果不同,一个是导入 default,一个是导入所有,但实际上的效果却是完全等价的?难道 React 对此做了兼容?

Colliot

为什么在 PHP 中,有时会出现浮点数莫名其妙多了很多精度的问题?

就比如明明内存中是 a = 2.1,但是经过 json_encode 之后,JSON 中的数字却变成了 2.100000000000000088817841970012523233890533447265625

Colliot

不同时期产生的改进同一个产品的想法, 是否会导向同样的结果?

比如几个小时前我认为要改造净土的这些点,但是当时没有去做。过了几个小时,想不起来了,那只要我勤于思考,以后是否还会产生类似的想法?

Home

Babel

Knowledge

Epistemology

Settings