5eqn

PLT

题解(12)

/ 注册

全部文章 / PLT （共11篇）

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

背景对于本篇文章，你只需要知道将立方类型论理解成一种通过改变形如 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

DTmpl: 基于依值类型和模板的高级语言代码生成思路

模板是针对高级语言代码生成的一种已有方案之一，工业上的例子包括 ANTLR 等。依值类型被广泛用于证明验证或自动证明，例子包括 Agda 等。然而目前来看模板的自由度极低，应对一些需要展开的任务，例如生成 Golang 代码中的大量错误处理，实现起来比较困难。依值类型虽然允许直接通过搜索生成想要的程...

Idris2 Go

2023-07-15

0 317

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

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

Idris2 CuTT

2023-07-13

0 414

一个抽象的类型论想法

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

Idris2 CuTT

2023-07-11

0 376

FStar 官方习题 A First Model of Computational Effects

官网写在前面 F* 目前只在 Emacs 有功能全面的编辑器插件，但可惜本人太菜，只会用 Vim，因此只能在线写码。 State Monad 可以理解为封装后的计算，接受初始状态，返回计算结果和后状态。 let st a = int -> a & int read 是一个计算，不...

F*

2023-01-23

2 323

FStar 官方习题 Constructive & Classical Connectives

链接官网内容讲述了各种数理逻辑符号在 F* 里的原始实现，以及接近数学形式的 squashed form。提供了语法糖来书写用于操作 squashed form 的命题。个人感觉 F* 提供的语法糖相比 Lean 更冗长，使用体验也比较差，有种 Brainf**k 的感觉习题一大意...

2023-01-22

0 285

FStar 官方习题 Equality Types

可参考官网内容讲述了不同的等价关系，例如定义相等由于采用 Inductive Type 机制，原先表现形式不同的表达式经过自动化简后程序无法区分例 (fun x -> x) a 和 a (factorial 3) 和 6 证明相等使用 equal a b 这个类型...

2023-01-22

0 301

FStar 官方习题 Length-indexed Lists

可参考官网。内容可以将类型的一些属性作为类型的编号，这样在递归定义类型时就可以将属性直接计算出来。例如，以下是定长数组的定义： type vec (a:Type) : nat -> Type = | Nil : vec a 0 | Cons : #n:nat -> hd:...

F*

2023-01-21

0 359

FStar 官方习题 Case Study: Quicksort

概要这一小节讲述了如何用 F* 实现快排算法，并且证明其确实有排序的功能。铺垫：快排实现递归计算 list 长度： let rec length #a (l:list a) : nat = match l with | [] -> 0 | _ :: tl ->...

F*

2023-01-20

0 413

FStar 官方习题 Lemmas and proofs by induction

FStar 是什么？ F* 是一种面向证明的编程语言，运用大量奇技淫巧实现程序自证明，例如：依值类型，Dependent Type，简而言之就是允许类型依赖于具体的值函数式编程，Functional Programming，函数是一等公民，能像值一样作为参数和返回值元语言，Meta Lang...

F*

2023-01-19

1 361