granule

                     ___
                    /\_ \
   __   _  _    __      ___   __  __\//\ \      __
 / _  \/\`'__\/ __ \  /' _ `\/\ \/\ \ \ \ \   /'__`\
/\ \_\ \ \ \//\ \_\ \_/\ \/\ \ \ \_\ \ \_\ \_/\  __/
\ \____ \ \_\\ \__/ \_\ \_\ \_\ \____/ /\____\ \____\
 \/___/\ \/_/ \/__/\/_/\/_/\/_/\/___/  \/____/\/____/
   /\____/
   \_/__/

Granule 是一种具有线性类型系统和通过分级模态类型实现细粒度效果和副作用的函数式编程语言。

关于 Granule 的介绍可以在我们的论文《使用分级模态类型进行量化程序推理》中找到。更多项目详情可以在项目网站上查看。

示例

线性性意味着以下代码是类型错误的:

dupBroken : forall {a : Type} . a -> (a, a)
dupBroken x = (x, x)

然而，可以使用分级模态来精确解释参数可以使用的次数:

dup : forall {a : Type} . a [2] -> (a, a)
dup [x] = (x, x)

在 Granule 中结合索引类型和有界重用会导致标准 map 函数在大小固定的列表("向量")上有一个有趣的类型:

--- Map 函数
map : forall {a : Type, b : Type, n : Nat}
    . (a -> b) [n] -> Vec n a -> Vec n b
map [_] Nil = Nil;
map [f] (Cons x xs) = Cons (f x) (map [f] xs)

这个类型解释了参数函数 f 被使用了恰好 n 次，其中 n 是输入列表的大小。线性性确保整个列表被精确地消耗一次以产生结果。

安装

目前仅为 MacOS 提供二进制发布版。如果您需要比可用版本更新的发布版，请开一个 issue。

要从源代码构建 Granule，请确保您的系统上安装了 Z3 和 Stack。

现在运行

git clone https://github.com/granule-project/granule \
&& cd granule \
&& stack setup \
&& stack install

这将安装主要前端 gr 和交互模式 grepl。

有关如何安装的更多详细信息可以在 wiki 页面上找到。

文档

Granule 标准库文档

您可以在编译器顶层的 docs 目录中运行 Granule 的文档生成模式，使用以下命令:

 gr --grdoc filename

您可以通过运行以下命令为标准库生成所有文档:

 gr --grdoc StdLib/*.gr
 gr --grdoc StdLib/*.gr

(注意这里的第二次运行，它可以稳定多文件运行之间的模块超链接)。

编译器

Granule -> Haskell 编译器

这由 grc 提供，它以 .gr 文件作为输入，输出编译为 Haskell 的 .hs 文件，该文件导入 Language.Granule.Runtime 模块(所以如果你想编译生成的 .hs 文件，你需要将这个模块放在路径中)。

LLVM 编译器

如果您还想安装 LLVM 编译器(实验性的，仍在开发中)，您可以从它的单独仓库获取，并通过以下命令安装:

stack install :grc

运行检查器 + 解释器

Granule 程序文件的扩展名为 .gr。使用 gr 命令运行解释器:

$ gr examples/NonEmpty.gr
Checking examples/NonEmpty.gr...
OK, evaluating...
1

学习 Granule 的一个好起点是 examples/intro.gr.md 中给出的教程。

在 Windows 上，您可能会遇到 Unicode 问题，解决方法是将代码页设置为 UTF-8 (通过 chcp.com 65001 https://stackoverflow.com/questions/25373116/how-can-i-set-my-ghci-prompt-to-a-lambda-character-on-windows)。您可能还想不使用颜色运行 gr --no-color。

设置路径

Granule 有一个非常基本的导入系统。当 gr 在文件中遇到 import A.B.C 这样的行时，它会尝试加载位于 $GRANULE_PATH/A/B/C.gr 的文件，其中 $GRANULE_PATH 默认为 StdLib，即当你在这个项目内运行 gr 时应该可以正常工作。为了获得更稳定的设置，让你可以从任何目录运行 gr，你可以使用 --include-path 标志设置路径（见下文）。

配置

使用 --help 标志运行 gr 可以获得标志概览。标志可以通过以下方式设置：

1. 在 ~/.granule 中（与命令行上的方式相同）
2. 在命令行上
3. 在文件顶部（前面加上 -- gr ）

优先级按上述顺序，例如，命令行上设置的标志将覆盖配置文件中的标志。

.granule 文件示例：

$ cat ~/.granule
--include-path /Users/alice/granule/StdLib
--solver-timeout 2000

命令行补全

关于如何为你的 shell 安装补全脚本，请参见这里，不过我们建议在 shell 的启动脚本中动态加载补全，以适应 gr 接口的变化；例如，对于 MacOS 上的 fish：

echo "#granule
gr --fish-completion-script (which gr) | source" >> ~/.config/fish/config.fish

可访问性

我们致力于使 Granule 尽可能具有包容性。如果你遇到任何可访问性障碍，请开启一个 issue。

替代颜色

--alternative-colors/--alternative-colours 标志会使成功消息以蓝色而非绿色打印，这可能有助于色盲用户。

--no-color/--no-colour 标志会完全关闭颜色。

多字节 Unicode

以下符号可以互换。你可以通过传递 --ascii-to-unicode/--unicode-to-ascii 来破坏性地重写源文件中的所有出现。--keep-backup 将保存输入文件最新副本的备份，并附加 .bak。

ASCII	Unicode
forall	∀
exists	∃
Inf	∞
->	→
=>	⇒
<-	←
/\	∧
\/	∨
<=	≤
>=	≥
==	≡
\	λ

操作符 ∘ 的用法被解析为 compose 的应用。

文学化 Granule

Granule 对 Markdown 和 TeX 的文学程序有一些基本支持。默认情况下，granule 代码环境中的代码将被运行。这可以通过 --literate-env-name 标志覆盖。

Markdown

解释器也接受扩展名为 .md 的 markdown 文件，在这种情况下，所有标记为 granule 的围栏代码块都将被解析为输入源代码。所有其他行都被忽略，但作为空白计数以保留错误消息的行号。

# 文学化 granule（markdown）文件示例

代码块可以用波浪线围起来...

~~~ granule
a : Int
a = 1
~~~

... 或者反引号。

```granule
b : Int
b = 2
```

以下代码块将被忽略。

~~~
int c = 3;
~~~

```haskell
d :: Int
d = 4
```

TeX

你可以使用 gr --literate-env-name verbatim 在下面的 TeX 文件上运行 Granule。 你可以使用 XeLaTeX 正确显示多字节 Unicode 字符。

\documentclass{article}

\title{文学化 Granule（\TeX{}）示例}
\begin{document}
\author{Grampy Granule}
\maketitle

在这里写东西。

\begin{verbatim}
import Prelude

foo : String
foo = "在这里运行代码"
\end{verbatim}
\end{document}

注意事项

Granule 是一个研究项目，旨在帮助我们获得关于在编程中使用线性性和分级模态的直觉。它采用宽松的许可证，所以你可以将其用于任何用途，但请暂时不要用 Granule 编写你的下一个航天器控制器。接口不稳定（代码也不稳定）。你已经被警告过了...

            （欢迎所有贡献！）
      __//   /
    /.__.\
    \ \/ /
 '__/    \
  \-      )
   \_____/
_____|_|______________________________________
     " "