Hexixi

为啥很多场景管 utf-8 叫字符集(charset)呢?

比如 MIME Content Type、HTML meta 和 MySQL。

utf-8 不应该是一种使用 unicode 字符集的字符编码(character encoding)吗

ice1000

Row polymorphism的实现有什么好的阅读材料?

最近在看https://www.microsoft.com/en-us/research/wp-content/uploads/1999/01/recpro.pdfhttps://people.cs.uchicago.edu/~blume/papers/icfp06.pdf ,感觉已经会用了,但是对实现还是有点把握不准,特别是当我要把这个东西放进 bidirectional type-checking 的时候

ice1000

为什么我只能看最近的一些问题?

我好像不能查看【fcom就是hcom的一种特殊形式吗】之前的问题了。这是一个新feature吗?

ice1000

HOL 的【AI】是什么东西?

https://github.com/HOL-Theorem-Prover/HOL/tree/develop/src/AI 这个东西。 难道 HOL 已经开始把机器学习应用到自动证明里面了吗?

Colliot

为什么 text-deocration 的属性分开写,在某些 Android 手机上就无法生效?

比如

.dummy {
  text-decoration-line: underline;
  text-decoration-style: solid; /* 有没有都不影响 */
  text-decoration-color: currentcolor; /* 有没有都不影响 */
}

这样写就没有效果,不展示下划线。一定要这样写:

.dummy {
  text-decoration: underline;
}

才行。

这是为什么呢?这是可预期的行为吗?

ice1000

Dependent Type 语言一般会设计哪几层AST?

目前就我所知,可能会需要Concrete Syntax Tree(和表层代码一一对应)和Abstract Syntax Tree(已经没有语法糖,但是可能不 well-typed。有的语言会在产生 Abstract 时进行 ScopeCheck,有的不会)以及 Value (TypeCheck 导出的 term,已经确保是 well-typed,可以直接对它进行值操作,比如函数调用)。

ice1000

Dependent Type的Core Language中Lambda一般都不存参数类型,为什么我们可以这么做?

说【一般】是因为 MiniAgda,Agda,MiniTT 都没存参数类型,但是也有例外,比如 Idris 存了。

ice1000

基于 Sized Types 的 termination check 有优化空间吗?

目前用的是一个 Floyd 求解。作为一个 OI 出身的人,我感觉这当中可以改进……尤其是考虑到图论算法的复杂性和 Haskell 语言中对 mutation 的支持,我觉得可以怀疑 MiniAgda 和 Agda 在选用算法上采取了一些妥协

ice1000

Cubical Type Theory 还有什么可以进一步发展的地方?

比如,我记得目前涉及Dimension的tyck是非常昂贵的,而且这个性能问题似乎还没有很好的解决方案。

ice1000

MiniAgda的ScopeChecker和TypeChecker是分离的,如何评价这种做法?

因为似乎这和不少其他的DT语言背道而驰。

ice1000

是什么在驱动HOL的长期开发?

他们的代码一直在活跃维护,我十分好奇他们是不是有什么金主在投资。但是还有一个有趣的问题是,他们目前在着力于给HOL解决什么问题?

ice1000

JetBrains Research除了Arend之外还在做什么?

他们似乎是比较General的HoTT Research Group。

ice1000

Standard ML到底应该使用哪个工具链?

MLton?SML/NJ?PolyML?

ice1000

如何理解PHOAS?和HOAS相比添加了什么?

因为它解决了positivity的问题

Home

Babel

Knowledge

Epistemology

Settings