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:[EMAIL PROTECTED] >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 [EMAIL PROTECTED], http://ptolemy.eecs.berkeley.edu/~eal ---------------------------------------------------------------------------- Posted to the ptolemy-hackers mailing list. Please send administrative mail for this list to: [EMAIL PROTECTED]