[TYPES] Questions regarding a clock inference system for data-flow languages
Rajagopal Pankajakshan
rajagopal.pankajakshan at live.com
Fri Aug 30 03:15:24 EDT 2013
Esteemed type theory experts,
During my internship at google this summer I was assigned to study type theory applied to stream-processing languages. One approach we considered was that of the so called clock calculi, as found for instance in Lucid-Synchrone [3].
Lucid-synchrone defines a type inference system to analyse synchronisation between data-flow streams. In this calculus, a stream clock s can be the base execution clock, the sample of another clock s on some condition (a name X or a variable n) or a variable α. The paper claims that clock analysis can be performed using Hindley-Milner type inference. The basic mechanism of type polymorphism is to universally quantify the free clocks α1,...,αn and names X1,...,Xm of a definition in its context H, here:
gen(H, cl) = ∀α⃗.∀X⃗.cl where α⃗ = FV(cl) - FV(H) and X⃗ = FN(cl) - FN(H)
This allows to reuse that definition where it is used, by considering an instantiation relation:
cl[⃗s/α⃗][⃗c/X⃗] ≤ ∀α⃗.∀X⃗.cl
My first question arises from the understanding that names X do not seem to have the same status as variables α in this type system. They are generalised and instantiated in the same manner. For instance, consider the following Lucid program:
node flip (x) = x when yes where clock yes = true
The boolean stream function flip samples all occurrence of x according to a local stream yes. According to the type system [3, figure 5], it has clock ∀α.∀X.α→α on X, as the following derivation shows:
|- true : s
_________________________________________________________________________
|- clock yes = true : (m:s)
_________________________________________________________________________
[yes : (m:s), x : s] |- x when yes : s on m
_________________________________________________________________________
[x : s] |- x when yes where clock yes = true : s on m (m not in [x : s])
_________________________________________________________________________
|- node flip (x) = x when yes where clock yes = true : [flip : s->s on m]
Gen([],s->s on m) = ∀s∀m.s->s on m
The opposite stream function flop, below, can also be given type ∀t∀n.t-> t on n.
node flop (x) = let x when no where clock no = false : [flop : ∀s∀n.t->y on n]
Now, if we let H = [flip,:∀s∀m.s-> s on m,flop:∀t∀n.t-> t on n] then, by rule (Inst) in [3, Figure 5], we can assign the same clock to of flip and flop with the following type derivation
u -> u on o ≤ ∀s.∀m.s->s on m u -> u on o ≤ ∀t.∀n.t->t on n
______________________________ ______________________________
H[x:s] |- flip : u -> u on o H[x:s] |- flop : u -> u on o H[x:s] |- x : s
_______________________________________________________________________________
H[x:s] |- flip (x) : u on o H[x:s] |- flop (x) : u on o
______________________________________________________________
H[x:s] |- flip (x) + flop (x) : u on o
______________________________________________________________
(1) H |- node sum (x) = flip (x) & flop (x) : [sum : u-> u on o]
Doesn't function flipflop deadlock or does this mean that it needs a buffer ?
I tried to figure this out by testing the example with the implementation of Lucid-Synchrone available on the web [2]. Actually, it behaves differently from what the paper says. For instance, if we try to define function flip as above, the compiler says:
"This expression has clock 'c but is used with clock (__c1:'d)"
It refuses to consider the assumption 'c as a sampled clock (__c1:'d) generated by the when operator. Shouldn't it infer (__c1:'d) instead ? However, if we add a clock declaration to do that:
let node sample (x, clock y) = x when y
let node yes (x) = sample (x, true)
let node no (x) = sample (x, false)
let node yesandno (x) = yes x & no x
then the compiler replies:
# lucyc -i yesandno.ls
val sample : 'a * bool => 'a
val sample :: 'a * 'a -> 'a on ?_y0
val yes : 'a => 'a
val yes :: 'a -> 'a on ?_y0
val no : 'a => 'a
val no :: 'a -> 'a on ?_y0
val yesandno : bool => bool
val yesandno :: 'a -> 'a on ?_y0
and produces a Caml program. But there are so many clocks in it that I can't really figure out what it does. Instead, I looked as the user manual [1] to determine which of [2] or [3] to focus on. Concerning instantiation, page 67, it says something different:
"The clock (carrier-clock : stream-clock) of a stream e means that e has value carrier-clock which has the stream clock stream-clock. The value may be either a global value (defined at top-level) or an identifier. This identifier is unique and is an abstraction of the actual value of e."
I don't understand how this uniqueness rule is specified in the paper [3] and, more generally, how it relates to type polymorphism. Doesn't it instead refer to existential quantification ? Also, in which cases does it apply in the implementation ?
In the end, I'm a bit confused and wonder whether polymorphism matters at all. As long as one is not using streams of functions, doesn't a simple sub-typing rule suffice (to handle a base clock and samples "c on x") ?
REFERENCES
[1] Marc Pouzet. Lucid Synchrone Release, version 3.0. Tutorial and Reference Manual. April 2006.
[2] Lucid-Synchrone v3.0b byte-code. URL http://www.di.ens.fr/~pouzet/lucid-synchrone/lucid-synchrone-3.0b.byte.tar.gz (md5 87ffdb559ad882a0d92a1213466c2a3c)
[3] Jean-Louis Colaço, Alain Girault, Grégoire Hamon, and Marc Pouzet. Towards a Higher-order Synchronous Data-flow Language. In ACM Fourth International Conference on Embedded Software (EMSOFT'04), Pisa, Italy, september 2004.
More information about the Types-list
mailing list