Rajagopal Pankajakshan | 30 Aug 09:15 2013

[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
(Continue reading)

Adrien Guatto | 30 Aug 18:01 2013
Picon

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

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

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 <rajagopal.pankajakshan <at> live.com>
To: "types-list <at> lists.seas.upenn.edu" <types-list <at> lists.seas.upenn.edu>
Subject: [TYPES] Questions regarding a clock inference system for
data-flow languages Date: Fri, 30 Aug 2013 07:15:24 +0000
Sender: "Types-list" <types-list-bounces <at> lists.seas.upenn.edu>

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

>
> 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
(Continue reading)

Rajagopal Pankajakshan | 3 Sep 10:53 2013

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

[ 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: adrien.guatto <at> laposte.net
> To: rajagopal.pankajakshan <at> live.com
> CC: types-list <at> lists.seas.upenn.edu
> 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 <rajagopal.pankajakshan <at> live.com>
> To: "types-list <at> lists.seas.upenn.edu" <types-list <at> lists.seas.upenn.edu>
> Subject: [TYPES] Questions regarding a clock inference system for
> data-flow languages Date: Fri, 30 Aug 2013 07:15:24 +0000
> Sender: "Types-list" <types-list-bounces <at> lists.seas.upenn.edu>
>
> > 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
(Continue reading)


Gmane