ice1000

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

MLton?SML/NJ?PolyML?

ice1000

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

因为它解决了positivity的问题

ice1000

HOAS的性能很好吗?

感觉比普通的reduction便宜

ice1000

IntelliJ可以把代码导出成文件内点击跳转的信息都保留的网页吗?

我觉得这个对写博客来说是一个杀手级特性

ice1000

What should we return when pattern matching on a Higher Indutive Type and the case is a Path?

Context: Cubical Type Theory

Consider a simple HIT, say, an HitInt:

data HitInt : Set where
  pos : (n : ℕ) → HitInt
  neg : (n : ℕ) → HitInt
  posneg : pos 0 ≡ neg 0


Or, if you don't speak Agda we can use cubicaltt:

data int = pos (n : nat)
         | neg (n : nat)
         | zeroP <i> [ (i = 0) -> pos zero
                     , (i = 1) -> neg zero ]


We want to define, for instance, a succ operation for it. As a functional programmer, we want to pattern matching on this HIT. In Agda, it's:

sucHitInt : HitInt → HitInt
sucHitInt (pos n) = pos (suc n)
sucHitInt (neg zero) = pos 1
sucHitInt (neg (suc n)) = neg n
sucHitInt (posneg x) = pos 1


Or in cubicaltt:

sucInt : int -> int = split
  pos n -> pos (suc n)
  neg n -> sucNat n
    where sucNat : nat -> int = split
            zero -> pos one
            suc n -> neg n
  zeroP @ i -> pos one


What I'm interested in is the last case-split of these two pattern matchings. The function is supposed to return the successor of the input integer, but we need to implement something that "finds the successor of the input _Path_".

My question is, how are we supposed to implement this case-split? In the cubicaltt version (taken from the cubicaltt's GitHub repository, examples/integer.ctt), it matches the Path pos 0 == neg 0 and returns pos 1 -- say, matches a Path, but returns a normal integer. Is this really what we want to do? Why it's not returning a Path like <i> pos 1 (even this is not a member of the higher inductive family)?

What's interesting is that, in Agda it'll fill pos 1 in the case body when I use Agda's proof-search.

ice1000

What does "Kan" mean in "Kan operations"?

I'm studying Cubical Type Theory and I see the word "Kan operations" (ref1, ref2, ref3, and there are many more), which is related to "adding a cap to a tube" (can be also explained as "given a path between a and b, and two paths that are between a and c/b and d respectively, we can use Kan operations to get a path between c and d").

I wonder if there's any references that can explain where this "Kan" word come from -- what does it mean? Is that "Kan extensions" in Category theory?

ice1000

公司开源的项目在不再被公司自己使用时,应该如何处理这个项目?

是继续维护吗?送给开源社区吗?你们有什么想法吗

ice1000

Extensible Record和Row Polymorphism是同一个东西吗?

他们有什么区别(或许还有Record Calculus)?

ice1000

现在Program Synthesis业界都在做什么?

好奇。前几天面基了张震巨佬,进行了一些询问,让我感觉意犹未尽

ice1000

有什么简单的解析Meta variable的教程?

最近需要写一些简单的Program Synthesizer,不想写太复杂的……

目前有一个很大的问题,就是我在check生成的term时,此时不知道生成的term是不是well-typed的,在tc的eval时可能会panic

ice1000

有能模块化生成的代码的Parser Generator吗?

我最近在批量生产一些Parser,感觉我甚至需要模块化他们,复用一些公共的部分。 但是我在使用一个叫GrammarKit的Parser Generator,它是设计给那种只支持一个编程语言的IntelliJ插件用的,从根本上杜绝了这么做的可能性。

ice1000

如何评价YACC Type Theory?

YACC是Yet Another Cartesian Cubical,不是那个Parser Generator

ice1000

如何评价RedPRL这一编程语言?

它的tactic似乎海星,不知道为什么停止开发了

ice1000

Cartesian CuTT和DeMorgan CuTT是如何合并到一起的?

这其实是在问Anders Mortburg最近发的论文讲的是啥,我太菜了

ice1000

基于Layout的语法是IDE的敌人吗?

我最近在我的IDE里支持了Agda这一需要layout解析的语言。我觉得这个语法让做IDE的人非常难受。

ice1000

如何评价Haskell的Parser Generator::BNFC?

它是不是直接解决了Alex和Happy用户搞不定Layout的痛点?

Home

Babel

Knowledge

Epistemology

Settings