5eqn

PLT

题解(12)

/ 注册

全部文章 / PLT （共3篇）

立方类型论在软件工程中的用例设想

背景对于本篇文章，你只需要知道将立方类型论理解成一种通过改变形如 A=BA = BA=B 的「相等类型」的构造形式，使得相等类型更能拟合人类直觉（例如过去一些人感觉显然成立的命题，例如函数外延性 (x:A)→f(x)=g(x)→f=g(x : A) \rightarrow f(x) = g(x) ...

CuTT Idris2

2023-07-17

1 653

对上一篇提出的类型论的探讨

上一期博客中我提出了 APTT, 简而言之就是把所有的类型都当作是 x = y 的形式，以提高格式的统一度。但这带来的问题是，进行格式统一后虽然正常的依值类型可以表达，但失去了讨论类型本身的能力。直观来讲，在 APTT 里面要创建一个类型，往往会得到一个形如 A = refl U 的形式，但我们只...

Idris2 CuTT

2023-07-13

0 414

一个抽象的类型论想法

最近在学习 CuTT, 虽然没怎么学会，但我在学的时候产生了一个不太一样的类型论构造想法。我的想法是先尝试把我的想法表述出来，这样后续我可能更能理解为什么 CuTT 的一些特定地方采取不同的设计，以及这样会带来什么优势和劣势。同时我也没有搜索有没有人形成过和我一样的类型论想法，暂时我先当作只有我提...

Idris2 CuTT

2023-07-11

0 376