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

[Edward A Lee]

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