[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Thanks a lot for your explanations Adrien, > Date: Fri, 30 Aug 2013 18:01:42 +0200 > From: [email protected] > To: [email protected] > CC: [email protected] > Subject: Re: [TYPES] Questions regarding a clock inference system for > data-flow languages > > Hello Rajagopal and TYPES list, > > I am doing my PhD under the supervision of prof. M. Pouzet and A. > Cohen, working on extended clock calculi for data-flow langages. I'll > try to answer your questions to the best of my knowledge. > > From: Rajagopal Pankajakshan <[email protected]> > To: "[email protected]" <[email protected]> > Subject: [TYPES] Questions regarding a clock inference system for > data-flow languages Date: Fri, 30 Aug 2013 07:15:24 +0000 > Sender: "Types-list" <[email protected]> > > > 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]. > > First, you may want to read "Clocks at First Class Abstract > Types" (Colaço and Pouzet, EMSOFT'03), because the section dedicated to > clock typing in EMSOFT'04 is indeed very terse. However, the full > system as implemented in Lucid Synchrone has never been described > anywhere, as far as I know. I had a look at the suggested [EMSOFT'03] paper and there seems to be the same problem there in Figure 3. Since a stream type s is also a clock cl you can use the (let) rule to generalise its type the same way, even thought the intended rule is (let-clock). > > 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. > > It is indeed HM-like, but it needs to be extended with first-class > abstract datatypes (restricted existential types) à la Laufer & > Odersky. See EMSOFT'03 above for references. > > > 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 > > If I'm not mistaken, in your example m is a name, not a condition > variable X. Thus it does not get generalized by Gen(). Indeed this > program gets rejected by Lucid v3, as you note: a condition name may > not escape its scope. The m&ns are really arbitrary in this example, I presume the intended meaning would probably to use is with names, but the judgment equally holds with variables as it should, shouldn't it: |- true : s _________________________________________________________________________ |- clock yes = true : (X:s) _________________________________________________________________________ [yes : (X:s), x : s] |- x when yes : s on X _________________________________________________________________________ [x : s] |- x when yes where clock yes = true : s on X (X not in [x : s]) _________________________________________________________________________ |- node flip (x) = x when yes where clock yes = true : [flip : s->s on X] Gen([],s->s on X) = ∀s∀X.s->s on X > > 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 ? > > Indeed, from the pure data-flow point of view, this program either > needs an infinite buffer on the left input of (&), or deadlocks if (&) > is synchronous (i.e. has no buffers on its inputs and outputs). Right, so the clocking rules fail to check the program synchronous from the (where) rule, in fact. > > 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. > > Strange, this code fails to compile on my machine with the same version > of the compiler. The clock types that you get are clearly incorrect. > This bug seems to be triggered by the "clock" keyword on inputs. If you > remove it, you get a saner clock signatures and "yes" and "no" are > rejected: > > val sample : 'a * clock => 'a > val sample :: 'a * (__c0:'a) -> 'a on __c0 > val yes : 'a => 'a > File "test.ls", line 2, characters 27-34: > >let node yes (x) = sample (x, true) > > ^^^^^^^ > This expression has clock 'b * 'c, > but is used with clock 'b * (__c1:'b). I just used the bytecode distribution available from your website: http://www.di.ens.fr/~pouzet/lucid-synchrone/lucid-synchrone-3.0b.byte.tar.gz (md5 87ffdb559ad882a0d92a1213466c2a3c). It would be kind if you could update it. > > 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 ? > > You are right and I have a hard time figuring out from EMSOFT'04 too. > It appears in a clearer form in EMSOFT'03, but I believe the final > system of LSv3 is still quite a bit different. > > The basic idea is simple: you may not have an expression with a clock > "'a on ?_c" if the condition ?_c is not present in the current scope. > Thus, when clocking "e where D", one basically checks that the > conditions "?_c_i" appearing in the clock type of "e" are still present > in current environment. > > It may help to consider this property in relation with the code > generation scheme. In the generated code, equations get translated to > imperative statements, each one conditioned according to its clock type > interpreted as a boolean formula. The current values of both clocks > variables and conditions will thus have to be accessible from the > current scope, at run-time. > > The compiler could automatically pass condition variables around, but > it is a design choice that prof. Pouzet deliberately rejected. > > > 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") ? > > I am not sure to follow what you have in mind, but note that in Lucid > Synchrone, a node do not have a single "base clock" in general. Please > consider the following example, where f is parametric in two clock > variables that get instantiated to two different clock types in g: > > # cat when.ls > let node f x y = (0 fby x, 0 fby y) > let node g x c = f x (x when c) > # lucyc -i test.ls > val f : int -> int => int * int > val f :: 'a -> 'b -> 'a * 'b > val g : int -> clock => int * int > val g :: 'a -> (__c0:'a) -> 'a * 'a on __c0 > > Also, and although experts on this list are far more knowledgeable than > me on this matter, it seems to be common knowledge that type inference > for HM-style parametric polymorphism is simpler (and thus easier to > implement) and more scalable than (non-structural?) subtyping. An > implementation of clock typing following the principles outlined above > and using destructive unification takes less than a thousand lines of > ML code and is very efficient. > > To conclude, you may be interested in the heavily simplified version of > clock typing that appears in "Clock-Directed Modular Code Generation > for Synchronous Data-Flow Languages" by Biernacki et al. (LCTES'08), > even if it is restricted to the first-order setting. The paper may also > serve as a nice introduction to the code generation machinery. Thanks a lot for these detailed explanations, I will certainly look at the other LCTES'08 paper. > Hope that helps, do not hesitate to send me follow-up questions. Sure, regards. --- Raj > -- Adrien Guatto > http://www.di.ens.fr/~guatto/index_en.html
