This reminds me of Guarded Dependent Type theory, which isn't about stream programming, but has the same dimension analysis built into it. Guarded Dependent Ty

This reminds me of Guarded Dependent Type theory, which isn't about stream programming, but has the same dimension analysis built into it. Guarded Dependent Type Theory (GDTT) has dimensions (called clocks), fby/sby (called later), clock quantification (to introduce new dimensions), and dimension analysis built into the type system in the form of "clocked universes" (type universes which depend on clocks). The latter is required for the semantics to make sense, but it also allows an implementation without implicit caching. In particular, GDTT does not have an analogue of first for all types, but only for those types which don't themselves depend on the clock parameter and this requires clock dependence to be tracked in the type system. Maybe not so interesting for stream processing as is, but it could probably be extended along those lines...