[kepler-dev] question on typing processes and higher-order

[kepler-dev] question on typing processes and higher-order

Post by eal » Thu, 27 May 2004 12:12:51


Bertram and 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...

In practice, we've relied on just making a choice, clearly documenting
it, and then judiciously using SequenceToArray and ArrayToSequence actors.
These have type <a> --> <[a]> and <[a]> --> <a>. But this solution has its
problems. For SDF, the ArrayToSequence actor needs to set a static
input array size, but this is not represented in the type system...
Similarly, SequenceToArray has a parameter arrayLength that has to be
static for SDF.

Steve Neuendorffer introduced a solution to this in version 4.0 where
parameters that affect scheduling can change dynamically, and it is
well-defined when schedules have to be recomputed, but this still
doesn't help in deciding whether types should be streams or
streams of arrays...

The short answer is that we don't have to conclude
that <<a>> == <a>. We can instead insist that ArrayToSequence
or SequenceToArray be used to convert types, which is what the
type system does today (modulo type inference, which can create
unexpected answers if you don't know whether you are dealing
with <<a>> or <a>).

But the long answer is harder... I don't have it...
Interesting question though...

Edward



At 01:08 PM 5/25/2004 -0700, Bertram Ludaescher wrote:


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


----------------------------------------------------------------------------
Posted to the ptolemy-hackers mailing list. Please send administrative
mail for this list to: XXXX@XXXXX.COM
 
 
 

[kepler-dev] question on typing processes and higher-order

Post by eal » Thu, 27 May 2004 22:14:14


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



------------
Edward A. Lee, Professor
518 Cory Hall, UC Berkeley, Berkeley, CA 94720
phone: 510-642-0455, fax: 510-642-2739
XXXX@XXXXX.COM , http://www.yqcomputer.com/ ~eal


----------------------------------------------------------------------------
Posted to the ptolemy-hackers mailing list. Please send administrative
mail for this list to: XXXX@XXXXX.COM