是否可以在 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

确实如此，看看沉本人的de作者的解释：

"Qi does include facilities for handling dependent types... The type notation is actually Turing equivalent... Shen has one important innovation not found in Qi II, which is the ability to extend the resident type checker with type secure tactics..." https://groups.google.com/forum/#!msg/Qilang/EkdF25yRrNM/sOuRYN2s85IJ

Answer 2

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

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

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

Is it possible to do dependent types in Shen?

types

lisp

dependent-type

shen