From eb8605fde88f5991cc678e0f10376ba9aa165f05 Mon Sep 17 00:00:00 2001 From: ice1000 <13892181+ice1000@user.noreply.gitee.com> Date: Tue, 19 Nov 2024 04:22:26 +0000 Subject: [PATCH] update projects/Aya/sample.md. Signed-off-by: ice1000 <13892181+ice1000@user.noreply.gitee.com> --- projects/Aya/sample.md | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/projects/Aya/sample.md b/projects/Aya/sample.md index 263a55a..631602e 100644 --- a/projects/Aya/sample.md +++ b/projects/Aya/sample.md @@ -11,10 +11,12 @@ 5. 项目简介。 -Aya 语言的特色是它强大的类型系统。这个类型系统拥有『依值类型（dependent type）』、『参数化多态（polymorphism）』这两个功能， -且支持等号类型。换言之，「两个值相等」这件事是一个类型，而它的实例就是这两个值相等的证明。 -例如，`插入排序 = 归并排序` 是一个合法的类型，且它等价于函数 `(x : 列表) -> 插入排序(x) = 归并排序(x)`, -也就是接收一个列表、返回它被两种排序算法排序后结果相同的证明。这样的证明可以在编程的同时证明一些关于程序的性质。 +Aya 语言是类似 Haskell 和 Lean4 的函数式编程语言，使用归纳类型、模式匹配、一等公民的函数等语言特性作为主要的代码组织工具。 + +比起 Haskell，Aya 拥有更强大的类型系统，支持『依值类型（dependent type）』，且支持比 Lean4 性质更好的等号类型。 +换言之，「两个值相等」这件事是一个类型，而它的实例就是这两个值相等的证明。 +例如，`插入排序 = 归并排序` 是一个合法的类型，并且在 Aya 中它直接等价于函数 `(x : 列表) -> 插入排序(x) = 归并排序(x)`， +这个类型的实例需要接收一个列表、返回它被两种排序算法排序后结果相同的证明。这样的证明可以在编程的同时证明一些关于程序的性质。 在 Aya 团队的招募贴 中， 有更详细的项目动机介绍。 @@ -23,7 +25,7 @@ Aya 语言的特色是它强大的类型系统。这个类型系统拥有『依 6. 项目分类：免费、开源（MIT）、通用、接受社区贡献 语言类别：高级编程语言、函数式语言、多范式语言 -工具类别：类型检查器、解释器，实时编译器尚未完成。另外有官方维护的编辑器插件的服务端 +工具类别：类型检查器、解释器、实时编译器（JIT 编译器）。另外有官方维护的编辑器插件的服务端 应用领域：通用、行业应用、计算数学。更具体来说，有编写算法类的程序、开发编译器、形式化数学等应用 7. 联系方式: ice1000kotlin@gmail.com（电子邮箱） -- Gitee