[kepler-dev] question on typing processes and higher-order fu nctions a la map

[Willink, Ed]

Hi Edward

Unfortunately, I'm not well-versed in 'dependent type system's
so I cannot comment on that.

I don't doubt that a set of contradictory type constriants can be
set up, but that's a detectable error, that can be made in a
simpler system too.

I see type inference as a multi-axis lattice problem, rather than
the single axis approach of Ptolemy. Typical axes are:

	minimum value
	maximum value
	fixed-point epsilon
	floating-point epsilon
	overflow behaviour (a small enumeration)
	rounding behaviour (a small enumeration)
	overflow bit-truth (2-valued)
	rounding bit-truth (2-valued)
	is-complex
	each array dimension
	array form (a small enumeration)

Each axis is orthogonal and therefore amenable to independent lattice
or number line maximisation/minimisation as appropriate. Whereas in
a single axis system valid solutions satisfy e.g a GE operator
consistently, in a multi-axis system valid solutions must satisfy
a GE operator on all axes. Perhaps the GT case on one axis, LT on
another is what you mean by undecideable. With orthogonal axes
it's just insoluble.

I think that it may be the failure to move from single-axis in
Ptolemy that may be creating a variety of problems. It was certainly
the case that the Ptrolemy lattice had to double-up for Complex
variants of all scalar types.

My ptolemy.math.Quantization contribution makes some progress in this
direction and allowed for independent treatment of some of the above
axes. Ultimately the work stalled through lack of response to a number
of emails.

C++ (and I think Fortran) are examples of conventional
languages where array dimensions can participate in the type
checking. If this is not part of the type system then I'm
not sure what you mean.

Ultimately if 'dependent type system' does mean that
dimensioned arrays are difficult, it just means that
practical designs are difficult. We cannot run away
from it. FFT frame sizes must be type-checked.

	Regards

		Ed Willink

> This is a nice idea, but doesn't this give you a dependent
> type system?  This means type inference is undecidable in
> theory, and extremely complicated in practice...
> 
> The only difference between:
> 
>     <double> --> <double>
> 
> and
> 
>     A sequential array (distributed in time over sequential samples)
>     with type T1[N] --> T2[N]
> 
> is the "N", which is what makes it a dependent type system...
> 
> Lots of people have tried to put array sizes into type systems
> in conventional languages... It's no accident that none of them
> have it...
> 
> Edward
> 
> At 11:55 AM 5/26/2004 +0100, Willink, Ed wrote:
> >Hi Edward, Bertram, Liying
> >
> > > You have hit upon something that has bothered me for some time,
> > > and have expressed it better than I ever did...  There are several
> > > examples of this tension in the Ptolemy II library.  E.g., the
> > > FFT actor has type <double> --> <double>.  Why isn't it
> > > <[double]> --> <[double]>?  It could just as well be, and I don't
> > > know of any way to choose between these...
> >
> >Surely <double> --> <double> is just wrong. It uses the COSSAP
> >fudge to support Arrays in a non-Array tool via accidental sequences.
> >Any type system that requires exaplanatory text, (use N successive
> >samples) is not a type system.
> >
> >For the proposed WDL, Waveform Description Language,
> >(http://www.computing.surrey.ac.uk/personal/pg/E.Willink/wdl/
wdl.html)
>I identified three distinct forms of array.
>
>A conventional array (distributed over adjacent memory addresses)
>A spatial array (distributed in space over a multi-port/multiple ports)
>A sequential array (distributed in time over sequential samples)
>
>(There is no limitation to 1D, provided the rasterising policy is
>well defined.)
>
>An FFT specification therefore is always T1[N} --> T2[N].
>Particular specialisations may choose different forms of array
distribution.
>
>Once these three forms are treated uniformly, it is also very easy
>to do automated conversions between them. For instance in Caltrop,
>each conversion would be just an 'assignment', with the distribution
>being an externally inferable property. In Ptolemy the multi-axis
>type lattice needed for fixed point must be extended with a further
>axis for the array-form lattice.
>
>         Regards
>
>                 Ed Willink
>
>------------------------------------------------------------------------
>E.D.Willink,                             Email: mailto:EdWillink at iee.org
>Thales Research and Technology (UK) Ltd, Tel:  +44 118 923 8278 (direct)
>Worton Drive,                            or  +44 118 986 8601 (ext 8278)
>Worton Grange Business Park,             Fax:  +44 118 923 8399
>Reading,   RG2 0SB
>ENGLAND          http://www.computing.surrey.ac.uk/personal/pg/E.Willink
>------------------------------------------------------------------------

------------
Edward A. Lee, Professor
518 Cory Hall, UC Berkeley, Berkeley, CA 94720
phone: 510-642-0455, fax: 510-642-2739
eal at eecs.Berkeley.EDU, http://ptolemy.eecs.berkeley.edu/~eal