[TYPES] Questions regarding a clock inference system for data-flow languages

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]




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.