Multidimensional arrays, parameterized types

[Johannes Engels]

Hello, still I am puzzling with the definition of multidimensional
arrays. I guess they should be parameterized by a) their element type
and b) their dimension. I tried to define such a type analogously to
the last two posts in the following thread:
http://comments.gmane.org/gmane.lisp.qi/2420


(datatype array

X:(vector A);
=============
X:(array A 1);


X:(array A (+ 1 N));
=====================
X:(vector (array A N));
)

(define nested-array
{(list number) --> (array A K)}
[N] -> (vector N)
[N | Ns] -> (let New-Vector (vector N)
(nest-array-set-elems New-Vector 1 N Ns)
)
)

(define nest-array-set-elems
{(vector B) -->
number -->
number -->
(list number) -->
(vector (array A L))}

Vector Limit Limit Ns ->
(vector-> Vector Limit (nested-array Ns))
Vector Index Limit Ns ->
(let New-Vec (vector-> Vector Index (nested-array Ns))
(nest-array-set-elems New-Vec (+ Index 1) Limit Ns)
)
)

(Boiled this down to the essential.) Compiling this I get the error
message
"type error in rule 1 of nested array".
Could anybody give me a hint?
Best regards
Johannes

[Mark Tarver]

Well it does look rather iffy

> (define nested-array
> {(list number) --> (array A K)}
>     [N]      -> (vector N)
>     [N | Ns] -> (let New-Vector (vector N)
>                  (nest-array-set-elems New-Vector 1 N Ns)
>                 )
> )

says that given a list of numbers it generates an array of any type
and dimensionality. This surely cannot be right.

> (datatype array
>
>    X:(vector A);
>    =============
>    X:(array A 1);
>
>    X:(array A (+ 1 N));
>    =====================
>    X:(vector (array A N));
> )

I'd expect the def to have the structure

(datatype array

   X : (vector A);
   ==========

   X : (array A 1);

  ......................
   ==============
   X : (array A (+ N 1)); )

where ....... remains to be filled.

Mark

[Johannes Engels]

On May 28, 9:46 pm, Mark Tarver <dr.mtar...@gmail.com> wrote:
> Well it does look rather iffy
>
> > (define nested-array
> > {(list number) --> (array A K)}
> >     [N]      -> (vector N)
> >     [N | Ns] -> (let New-Vector (vector N)
> >                  (nest-array-set-elems New-Vector 1 N Ns)
> >                 )
> > )
>
> says that given a list of numbers it generates an array of any type
> and dimensionality.  This surely cannot be right.
>

Would it be possible somehow to define K (i.e. the dimensionality of
the array) as the length of the (list number), i.e. of the first
argument within the type declaration?
Johannes

[Mark Tarver]

Yes. What is missing, as you have noticed, is something linking the
size of the list of numbers with the dimensionality of the array.
However even if you were to do that I think you would encounter
problems. You should read this:

http://www.lambdassociates.org/studies/inductive.htm

The solution is to integrate an environment for interactive proof into
Shen to enable such proofs to be conducted. (Such is the focus of my
work after TBoS in case people are wondering my direction. This forms
part of a work called 'The Specification of Programming Languages' and
is concerned with safety critical verification). However from where
you are sitting now, something like this cannot be easily be done.

Mark

[Johannes Engels]

Well, you are right: that looks amazing, but is not feasible for me. I
guess it would be easier to define an array as a structure or class,
consisting in a list of numbers (the dimensions) and a flat vector
(containing the elements in row- or column-major sequence). So the
construction would look like

(defclass myarray [(@p dimensions (list number)) (@p array-elements
(vector A))])

(define foldl
{(A --> B --> A) --> A --> (list B) --> A}
_ Akku [] -> Akku
F Akku [X | Xs] -> (foldl (F Akku X) Xs)
)


(define newarray
{(list number) --> (myarray A)}
Ns -> (let Totnum (foldl * 1 Ns)
Newvec (vector Totnum)
Newarr (make-instance myarray)
Dummy (change-value Newarr dimensions Ns)
(change-value Newarr array-elements Newvec)
)
)

(At the moment this gives a type error as well, seems that the Qi
classes cannot be simply used as they are in Shen.)
I guess however that you, Mark, have some objections: In your reply to
Joel Shellman's post on March 30 in the thread "Some Beginner's
Questions" you stated that this approach would lead into "deeper
waters". Could you please briefly comment on this?
Johannes

[Mark Tarver]

The deeper waters were the ones in my essay; that's what I felt you
might get into and I was right. I think the essay pretty much states
the challenge. I'll be looking at it after TBoS.

Mark

On May 29, 9:38 am, Johannes Engels <johannes.eng...@hft-stuttgart.de>
wrote:

[Joel Shellman]

In this blog post, we apparently have a vector-of-length type:

http://sandycat.info/blog/deptypes-shen/

But it does not appear to use inductive types. So, in your essay:

http://www.lambdassociates.org/studies/inductive.htm

you mention the issues of inductive types. However, is there a way to
create the matrix type (and multidimensional arrays) and such things
without inductive types?

[Mark Tarver]

Looking at the blog, it doesn't seem that inductive types are involved
in the way my matrix example uses them. Generally if you have an
inductive type, you do need at some point to use induction to work
with it. The problem arises because Shen's sequent calculus allows us
to express types for which T* (powerful though it is) is unsuited as a
proof procedure. The general solution to this class of problems and
indeed all problems beyond T* is the subject of my research post TBoS.

Mark

[Mark Tarver]

> you mention the issues of inductive types. However, is there a way to
> create the matrix type (and multidimensional arrays) and such things
> without inductive types?

I think if you are going to define a type like 'matrix' you will need
inductive types. However supposing that you wished to avoid them and
yet have type checking then the only way to do it would be to define
'matrix' as an abstract datatype by formulating a set of constructor/
selector/recognisor functions sufficient to do the job and each
function F in that specification would be assigned a type. In that way
the exact concrete realisation of your matrix would be a matter of
choice and not part of the type specification. It is an exercise in
thinking to do such a thing.

Mark