Is it possible to do dependent types in Shen?

Question

We see the benefits of Dependent Types 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.

We also see the benefits on 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.

The Shen language has an advanced type system.

Here the commentator describes Shen as having a Turing-Complete type system.

Here the commentator writes:

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

My question is: Is it possible to do dependent types in Shen?

Answer 1

Here is an example of Dependent Types in Shen from The Shen OS Kernel Manual

(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