Relog

几个强归一化字符串重写系统的实现

Relog (简化逻辑) 风格

a = Int;
List<a>
---output----
List<Int>

A<b,C<d>> = A<Int,C<Bool>>;
R<b>
---output-------------------
R<Int>

A<b,c> := R<c>;
A<B,C>
---output----------
R<C>

Print<"hello world">
---output-----------
[stdout]hello world
0

For<n,99,0,
   Print<"{n} bottles of beer on the wall
        \r{n} bottles of beer
        \rTake one down, pass it around
        \r{n} bottles of beer on the wall">
>
---output------------------------------
[stdout]99 bottles of beer on the wall
...
0

Relog 语法

Relog 是一种类型系统，而不是编程语言。它不是图灵完备的，它是强归一化的。

Relog 程序的基本语法由统一性定义，后跟一个结果。

统一性有一个左侧和一个右侧，由一个等号分隔，每个统一性后面跟一个分号

Pair<a,b> = Pair<Int,Int>;

结果是单个项，可以引用之前操作绑定的统一性变量

Pair<a,a>

一个示例程序可能表示应用一个函数 a -> Maybe<a>，参数为 Int，如下所示

a = Int;
Maybe<a>

当运行此程序时，统一性将 Int 绑定到 a 并返回结果 Maybe<Int>。

Relog 类型系统

$$apply \ \ \frac{unify(f,fx)⊢r}{f⇻r⊢reify(apply(r))}$$