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

Answer 2

Indeed, look at the expanation from de author of Shen itself:

"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 3

Here is an example of defining an arbitrary transformation within the type checker. meta.uncons maps [cons a [cons b []] to [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]