Dependent types and vectors (again)

[4DA]

Hi!
As an exercise i finished simple dependent vector stuff.

And also made a small blog post about that:
http://sandycat.info/blog/deptypes-shen/

What do you think?
Does shen need that kind in its standard lib?

Code below
-----------------------------------------------------------
(datatype subtype
(subtype B A); X : B;
_____________________
X : A;)

(datatype positive
if (and (number? X) (> X 0))
____________
X: positive;

________________________
(subtype positive number);

_______________________________________
+: (positive --> positive --> positive);
)

(datatype integer
if (integer? X)
___________
X: integer;

________________________
(subtype integer number);
)

(datatype natural
X: positive;
X: integer;
============
X: natural;
)

(define positive?
{number --> boolean}
X -> (> X 0))

(define natural?
{number --> boolean}
X -> (and (integer? X) (positive? X)))

(datatype index
X: natural;
=============
X: (index X);

if (and (natural? X) (natural? Y) (< X Y))
_____________
X: (index Y);
)

(datatype safevec

K: (index K);
=========================
(vector K): (safevec A K);

\* K: (index K); *\
______________________________________________
<-vector: ((safevec A K) --> ((index K) --> A));

______________________________________________
vector->: ((safevec A K) --> (index K) --> A --> (safevec A K));
)

\*
--------------------------------------------------------------------------------
*\
(define safevec-init
{(index N) --> (safevec A N)}
N -> (vector N))

\*
--------------------------------------------------------------------------------
*\
(define safevec-ref
{(safevec A K) --> (index K) --> A}
V L -> (<-vector V L))

\*
--------------------------------------------------------------------------------
*\
(define safevec-set
{(safevec A K) --> (index K) --> A --> (safevec A K)}
Vec I Val -> (vector-> Vec I Val))

\* Test with this: *\
\* (safevec-ref (safevec-set (safevec-init 10) 3 3) 3) - OK*\
\* (safevec-ref (safevec-set (safevec-init 10) 3 3) 12) - type error*\

[Mark Tarver]

I think that the idea of a vector type theory which statically checks
for out of bounds calls is a good idea.

Mark

> ---------------------------------------------------------------------------­-----

> *\
> (define safevec-init
>  {(index N) --> (safevec A N)}
>  N -> (vector N))
>
> \*

> ---------------------------------------------------------------------------­-----

> *\
> (define safevec-ref
>   {(safevec A K) --> (index K) --> A}
>   V L -> (<-vector V L))
>
> \*

> ---------------------------------------------------------------------------­-----

[Artella Coding]

Hi, I tried out the above code but I get a type error, and I think it has to do with safevec-init. Does anyone know what modification I might need to make to get the above code to work? Thanks.

[Artella Coding]

Hmm not sure I completely understand what I am doing. Anyways found that I had to add :

  X: natural >> P;

  __________________

  X: (index Y) >> P;

to "datatype index" and : 

  V: (vector K);

  ________________

  V: (safevec A K);

to "datatype safevec". So the following now seems to work : 

===========================================

===========================================

===========================================

  X: natural >> P;
  __________________
  X: (index Y) >> P;
)

(datatype safevec

  V: (vector K);
  ________________
  V: (safevec A K);

===========================================

===========================================

===========================================

[Artella Coding]

Reposting because there was a problem with the formatting of the above. 

The modified version of Dmitry's code is : 

===================================================
===================================================

===================================================

===================================================

===================================================

===================================================