types - 是否可以在 Shen 中做依赖类型？

Question

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

Dependent types are types that depend on elements of other types. An example is the type An of vectors of length n with components of type A. Another example is the type Amn of m n-matrices. We say that the type An depends on the number n, or that An is a family of types indexed by the number n.

我们还在 Cedric's blog 上看到了好处:

Having a list with one element would be a type error, so the second line in the snippet above should not compile.

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

此处评论员将沉描述为having a Turing-Complete type system .

在这里the commentator writes :

You can however use dependent types in a way in Shen that does not create problems.

我的问题是:是否可以在 Shen 中进行依赖类型？

Answer 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