沉可以做依赖类型吗？

Question

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

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

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

拥有一个包含一个元素的列表将是一个类型错误，因此上面代码段中的第二行不应该编译。

Shen language有一个先进的类型系统。

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

在这里the commentator writes：

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

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

Answer 1

沉从OS内核手册中沉从属的Here is an example

(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

Answer 2

确实，看看沉从文的作者的扩张：

“Qi确实包含了处理依赖类型的设施......类型符号实际上是图灵等价的...沉有一个在Qi II中找不到的重要创新，即能够使用类型安全策略扩展常驻类型检查器...... “https://groups.google.com/forum/#!msg/Qilang/EkdF25yRrNM/sOuRYN2s85IJ

Answer 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]