是否可以在沈中做依赖类型？答案

【问题标题】：Is it possible to do dependent types in Shen?是否可以在沈中做依赖类型？
【发布时间】：2015-02-02 10:18:00
【问题描述】：

我们看到了依赖类型in a paper written by Ana Bove and Peter Dybjer 的好处：

依赖类型是依赖于其他类型元素的类型。一个例子是长度为 n 的向量类型 An，其分量类型为 A。另一个例子是 m n 矩阵的类型 Amn。我们说类型 An 取决于数 n，或者说 An 是由数 n 索引的类型族。

我们还看到了Cedric's blog 的好处：

只有一个元素的列表是类型错误，所以上面的 sn-p 中的第二行不应该编译。

Shen language 具有高级类型系统。

这里评论员将沉描述为having a Turing-Complete type system。

这里the commentator writes：

但是，您可以在 Shen 中以不会产生问题的方式使用依赖类型。

我的问题是：Shen可以做依赖类型吗？

【问题讨论】：

这句话似乎暗示它是？我猜你在追求更具体的东西，但我不确定是什么。

标签： types lisp dependent-type shen

【解决方案1】：

Here is an example 来自 Shen OS 内核手册的 Shen 中的依赖类型

(datatype my-prover-types

  P : Type;
  _______________________
  (myprog Type X) : Type;)
type#my-prover-types

(define myprog
  Type P -> P)

(myprover symbol p)
p : symbol

(myprog number p)
type error

【讨论】：

【解决方案2】：

确实，看看沉本身的作者的解释：

“Qi 确实包含处理依赖类型的工具...类型表示法实际上是图灵等价的...Shen 有一个 Qi II 中没有的重要创新，那就是使用安全类型扩展常驻类型检查器的能力战术..." https://groups.google.com/forum/#!msg/Qilang/EkdF25yRrNM/sOuRYN2s85IJ

【讨论】：

【解决方案3】：

这是在类型检查器中定义任意转换的示例。 meta.uncons 将 [cons a [cons b []] 映射到 [a b]。

(0-) (datatype meta.uncons

            (meta.uncons X X*);
            (meta.uncons Y Y*);
  _____________________________________
       (meta.uncons [X|Y] (X*|Y*));

  _____________________________________
            (meta.uncons X X); )

type#meta.uncons

(1-) (prolog? (shen.t* [meta.uncons [cons a [cons b [cons c []]]] Z] [])
              (return Z))

[a b c]

【讨论】：