___________________________________________ SUMMARY OF [BP] WITH A FEW ADDITIONAL NOTES ___________________________________________ * The present notes are not intended to be used instead of [BP], * * but, in order to support the study of it, they provide a short * * summary together with a few additional comments. * run: ____ Informally, 'run' enables to switch from full PICT (where you can program also in functional style) to Core PICT (which has not much more than pi-calculus) The zero process: _________________ run () Parallel composition: _____________________ run (() | () | ()) pi-calculus notation in PICT: _____________________________ _ x!y stands for x y x?y=P stands for xy.P In PICT we have also "concrete" values, not just channel names. Among which, tuples of values. The empty tuple can be looked at as a syncronization signal: [] Printing: _________ run ( print!"peering" | print!"absorbing" | print!"translating" ) You get: peering absorbing translating print is NOT a command, but the name of a channel enabling to communicate to the "hidden" process that prints Example: run ( x?[] = print!"Got it!" | x![] ) Got it! The above process is NOT equivalent to run x?[] = (print!"Got it!" | x![]) Other example: run ( x!y | x?z = z!u | y?w = print!"Got it!" ) Got it! The following process is different, but we get the same result. run ( x!y | x?z = a!z | a?w = print!"Got it!" ) Got it! Notice that the two processes are not equivalent since you can find a system that behaves differently according to the fact that one or the other of the two processes is used as subprocess. Exercise: Find such a system. Values: _______ Like in the pi-calculus, a channel is a value. As said above, tuple of values are values [v1...vn] (actually we can also have tuples with named fields, i.e. records) x, [x y], and [x [[y x]] y [] x] are then values The "syncronization signal" is then simply the empty tuple. For the time being strings are values only for the print channel In the pi-calculus only channels were values. Similarly to the lambda-calculus, any data type can be represented as a pi-calculus term. Of course, in a real programming language we use predefined data types. Pattern Matching: _________________ We can receive values by means of patter matching (like inputs for haskell functions) Pattern matching produces, like in haskell, bindings for variables Exercise: - define in haskell the data type of pict values - define the data type of patterns - define the data types of bindings - define the pattern matching operation Other useful patterns: _ (wildcard) matches anything, produces no binding x@p (layered pattern) produces the binding for the pattern p, more the one between x and the whole input Example of layered pattern: run ( new ch: ^[String String] ( ch!["Hello" "world"] | ch?a@[b c] = ( print!b | print!c ) ) ) Hello world The binding produced in the above communication is b|->"Hello" c|->"word" a|->["Hello" "world"] Variable declarations: ______________________ In PICT it is possible to have variable declarations (in the functional programming sense): val i = 50 val b = true val message = "Hello" Good news: PICT is typed!!! Types: ______ Languages such as C, C++ and Java created a bad reputation to static type systems. There, in order to do something useful, you had to constantly “cast” values from one type to another. We recommend you to ignore those examples. You should rather look at good examples such as typing in ML or Ocaml. Typing belongs to computer science. [B.Pierce] PICT is statically typed ---------------- primitive types: type | example value _________________________ Bool | true Int | 50 Char | ’c’ String | "The Pict programming language" The type system (statically) guarantees that patterns matches values in communications types are partly inferred (in practice, the type of a channel has to be declared whenever it is introduced). So, an approach a' la Church, even if in some places types can be omitted if they can be inferred by the system. example value | its type ______________________________________ [] | [] [5] | [Int] [5 10 15] | [Int Int Int] [5 "foo"] | [Int String] [[48 8 41] [17 6 46]] | [[Int Int Int] [Int Int Int]] Possibility to give a name to a type (like in Haskell and OCaml) type X = T Channels: _________ New channel names can be introduced by means of the "new" declaration: new x:^T Each channel may be used to send and receive values of exactly one type. If this type is T, then the type of the channel is ^T, read “channel of T” or “channel carrying T.” (The one of PICT is not the only possible approach to typing. We shall give a sketchy overview of session types in [FB7]. In the session types approach, channels can carry any sort of values. Types can be used to ensure that the sequence of values exchanged through a channel respect a specifyed order.) Example new x:^Int new y:^Int run x!y Type error!!! Example of well typed program: new x:^Int new y:^Int new z:^^Int run ( x!50 | y!100 | z!x | z!y ) The keywords new, run, type all introduce declaration clauses. A Pict program is a sequence of declaration clauses. The scope of variables introduced in each clause is all of the following clauses. new x:^Int run ( x?a = () | x!5) new y:^[Int Int] run ( y?[a b] = () | y![5 6] ) Private declarations: _____________________ Any process expression e can be preceded by a sequence d of private declarations d: (d e) Example1: run ( new x:^[] ( x![] | x?[] = () ) ) Example2 (equivalent to Example 1): run ( new x:^[] run x![] x?[] = () ) As expected, processes are considered modulo alpha-conversion for bound channel names. In the following example the 'x' in the first subprocess has nothing to do with the 'x' of the second one. run ( ( new x:^[] ( x![] | x?[] = () ) ) | ( new x:^[] ( x![] | x?[] = () ) ) ) The mechanism of scope extrusion holds as in the pi-calculus. Scope extrusion: run ( new x:^[] ( z!x | x?[] = print!"Continuing..." ) | Q ) Replication: ____________ In PICT an infinite behaviour can be achieved by means of the use of "replication" (see [BP], !P , *P) The replication in PICT is restricted to input-processes, declared by means of the keyword "def". def hailer [] = print!"Hail!" The above definition defines a process which is equivalent to the following pi-calculus process !(hailer?[].print!"Hail!") In general, a def process like def ch pattern = P is equivalent to the following pi-calculus process !(ch?pattern.P) A PICT process like def hailer [] = print!"Hail!" is then equivalent to the following PICT declarations new hailer : ^[] run ( hailer?[] = print!"Hail!" | hailer?[] = print!"Hail!" | hailer?[] = print!"Hail!" | ... -repeated infinite times- ... ) The hailer channel is visible in the body of def and also after the def construct def hailer [] = print!"Hail!" run ( hailer![] | hailer![] | hailer![] | hailer![] | hailer![] ) Hail! Hail! Hail! Hail! Hail! By means of def we can describe recursive processes: def hailer n:Int = if (== n 0) then () else ( print!"Hail!" | hailer!(dec n) ) run hailer!5 Hail! Hail! Hail! Hail! Hail! And mutually recursive processes as well: using def .. and .. and .. def ping n:Int = if (== n 0) then () else ( print!"ping" | pong!(dec n) ) and pong n:Int = if (== n 0) then () else ( print!"pong" | ping!(dec n) ) run ping!6 ping pong ping pong ping pong According to the definition of the language we cannot be sure that the above process produce alternating "ping" and "pong". Actually, the specification of the PICT language does not force any particular scheduling of processes. Any "fair" scheduling is admitted by the language specification. By means of fair schedulers any process can progress (if it is able to) sooner or later. Exercise (ping pong): 1.Make sure the ping-pong process produces alternating "ping" and "pong" in any PICT implementation. 2.Have you done the above exercise? Are you sure it works? In case not, why? 3.Do it again after studying the "pr" channel. Conditional processes: ______________________ run if true then print!"branch1" else print!"branch2" run if false then print!"branch3" else print!"branch4" branch1 branch4 run ( if true then print!"branch1" else print!"branch2" | if false then print!"branch3" else print!"branch4" ) branch1 branch4 There is a version of "if" also for expressions (in the functional sense) In PICT it is possible to typecheck unwanted behaviours, other than pattern matching failure at run time, by means of Input an Output channels: _________________________ It is possible to declare a channel to be used ONLY for input or output. Example: consumer-producer program We wish to program a system with a process producing numbers and a process "consuming" them (printing them in the present case). def consumer channel:^Int = channel?i = ( printi!i | consumer!channel ) def producer [channel:^Int i:Int] = if (== i 0) then () else ( channel!i | producer![channel (dec i)] ) new ch:^Int run consumer!ch run producer![ch 4] 4 3 2 1 The producer, it were badly programmed, once received ch, could use it also to receive integers. In such acase, that would be a Violation of POLA!!! (PrincipleOfLeastAuthority) - - - - Th principle of least authority (also known as the principle of minimal privilege or the principle of least privilege) requires that in a particular abstraction layer of a computing environment, every module (such as a process, a user or a program depending on the subject) must be able to access only the information and resources that are necessary for its legitimate purpose.[Wikipedia] So, in order to respect the POLA, we can rewrite the above program as follows, by using input and output channel in order the process can use the channel only in the direction required by the specification. def consumer channel:?Int = channel?i = ( printi!i | consumer!channel ) def producer [channel:!Int i:Int] = if (== i 0) then () else ( channel!i | producer![channel (dec i)] ) new ch:^Int run consumer!ch run producer![ch 4] 4 3 2 1 How can we typecheck new ch:^Int ^^^^^^^ with def consumer channel:?Int = ... ? ^^^^^^^^^^^^ This problem can be overcome since, also in PICT, we have a notion of Subtyping: __________ The following types are in the Pict subtyping relation. ^T <: ?T ^T <: !T Meaning that a normal channel can be used in any context where an input or output channel is used. Notice how the above instances of the subtype relation in PICT provide an example of how, for channel types, the intuition of '<:' as a subset relation can be misleading. In fact it is not true that the set of channels carrying elements of type T is a subset of those that can be used only to receive or only to send elements of type T. Better here to stick to the principle of substitutability. In order to understand subtyping for PICT it is essential to do the exercise 3.2.1 of [BP]. Try and do that before going on. What does it need to be the relation between T and S in order ?T <: ?S to hold? If I am in a context where I receive (and use) elements of type S through a channel ch, I can replace it by a channel through which I can receive elements of type T if elements of T can be used instead of elements of S, that is if T<:S. This means that T<:S ---------- ?T<:?S What does it need to be the relation between T and S in order !T <: !S to hold? If I am in a context where I send elements of type S, if I send these elements trough a channel of type !T, they will be considered as elements of T. This means that an element of S should be used also as it were an element of T, that is S<:T. This means that S<:T ---------- !T<:!S So, the subtyping relation is covariant w.r.t. '?_' and contravariant w.r.t. '!_'. In order to have an intuition about what said above, think of an example using Int and Real instead of the generic S and T. What about '^_'? Does the solutions of (1) and (2) tell us something about that? Well, a channel of type ^T can be used to receive elements of type T, but also to send elements of T, so it should hold both T<:S and S<:T. This means that ^S<:^T can hold only in case S=T. In other words, the subtyping relation is invariant w.r.t. '^_'. We have no time to fully describe the formal rules describing the type system of PICT, but can describe some of them. First of all, we need to describe the judgments used by the type system. They are of the form B |- P where P is a (possibly open) PICT process, whereas B is a set of elements of the form "ch:T", where ch is a channel name and T a type. Notice that there is no type for P in the judgment, since types are only for channels and what we need to be guaranteed is that channels are used in a type safe manner in the process P. So means B |- P that in P channels are used in a type-safe manner if they have the type described in B. Another sort of judgment is needed: B |- x:T This means that x can be safely used as having type T under the assumptions of B. We have just an axiom and a rule for this latter sort of judgment, namely ------------- (if x:S is in B) B |- x:S B |- x:S S<:T ----------------------- B |- x:T Notice that the subsumption rule is used only for judgments of the form B |- x:T (Actually instead of B |- x:T we should use a more general judgment, namely B |- q:T, where q is a pattern or a value. So some more inference rules should be considered. We do not do that for sake of simplicity, but it an easy exercise). Now, let us have a look at some other rules. B |- x : ^T B, y:T |- P --------------------------------- B |- x?(y:T)=P (we could just write x?y=P since the system can infer the type of the input arriving on y by means of the type of x) B |- x : ^T B |- y : T ----------------------------------- B |- x!y B, x:T |- P ----------------------- B |- new x:T P Notice how the last rule resembles the one for typing a lambda-abstraction. In PICT, another refinement of channel types is possible, my means of Responsive channels: ____________________ The motivation for introducing such type for channel is efficency of compilation. In fact, sending on a channel of a "def" can be implemented essentially as a branch. In fact, for channels created by def clauses: (1) There is always a receiver available (2) all communications received by the same receiver Sending on other channels is instead far more difficult to implement (see [BP]) So, Types and Type system are used to statically know which outputs will communicate with definitions Responsive channels are denoted by /T Channels created by def have type /T Example (*): new x : ^[/Bool] def d b:Bool = if b then print!"True" else print!"False" run x![d] run x?[a] = a!false False By using the type of x, the type system, and hence the compiler, knows that the output action "a!false", if it will be ever performed during the execution of the program, will communicate with a def process. So, responsive types as sort of directives to the compiler. Useful... but they make a bit unclear what a type means. In Pict the following subtyping relation holds /T <: !T Also in such a case the subset interpretation of <: is extremely misleading, The "standard" predefined processes, like the printing one are treated (for efficiency of compilation of communication actions) like def processes Example of use of the above subtyping relation: the following process (**) can safely communicate with the def process described in the Example (*) above. new y : ^[!Bool] run y![d] (**) run y?[a] = a!false False The type system, by the definition of the def process of Example (*) (def d b:Bool = ...) knows that 'd' has type /Bool. Now, in the context new y : ^[!Bool] run y![ _ ] run y?[a] = a!false the symbol ' _ ' is a place where an element of type !Bool is expected, since 'y' is of type ^[!Bool]. The meaning of the subtyping relation S1 <:S2 tells us that in any context an element of type S2 is expected, an element of type S1 can be safely used. Since /T <: !T, we can put 'd', of type /T, in the place ' _ ' where an element of type !T is expected. In other words, the system automatically "casts" d, of type /T, to type !T (We know that uppercasts are type safe). (To cast means to use the subsumption rule). Exercise: Describe the full formal system for subtype judgments of PICT types S <: T The 'pr' channel: _________________ It is possible to communicate with the printing process not only by means of the print channel, but also using the primitive channel 'pr' having the following type pr : /[String /[]] 'pr' is used in order to pass to the printing process a tuple containing a string to be printed and a responsive channel through which the printing process will send a (syncronization) message acknowledging that the string has been printed. Example of use of pr: def d [] = print!"done" run pr!["pr... " d] pr... done In case we wished to receive the acknoledgment message (ack) through a normal channel, a type error would be ensued, as showed by the following example. new c : ^[] run pr!["pr... " c] run c?[] = print!"done" example.pi:2.20: > Expected type does not match actual > since ^[] is not a subtype of /[] > since ^[] and /[] do not match The problem can be solved only using an explicit cast. Casting a normal channel into a responsive one is done by means of the 'rchan' operator. (There could be cases in which rchan causes type problems?) Example of use of 'rchan' new c : ^[] run pr!["pr... " (rchan c)] run c?[] = print!"done" pr... done We can now use the 'pr' channel to find a possible solution for the ping pong Exercise. print is actually defined in terms of the lower-level predefined channel pr: def print s:String = ( def r [] = () pr![s r] ) Predefined operation (processes): _________________________________ In a programming language based on the notion of process, basic operations like addition, multiplication etc. are actually basic processes. So, +, * etc. are the names of the channels through which we communicate with such basic processes. To communicate with the sum process we use the channel '+' having type + : /[Int Int /Int] Example: run +![10 20 printi] 30 Example: run ( new r:^Int ( +![10 20 (rchan r)] | r?sum = *![sum 30 printi] ) ) 900 Example: run ( new r1:^Int new r2:^Int ( +![10 20 (rchan r1)] | +![30 40 (rchan r2)] | r1?sum1 = r2?sum2 = *![sum1 sum2 printi] ) ) 2100 Example: factorial (in the Core Language) run ( def fact [n:Int r:!Int] = ( new br:^Bool ( ==![n 0 (rchan br)] | br?b = if b then r!1 else ( new nr:^Int ( -![n 1 (rchan nr)] | nr?nMinus1 = (new fr:^Int ( fact![nMinus1 fr] | fr?f = *![f n (rchan r)] ) ) ) ) ) fact![5 printi] ) 120 Exercise: Write the Fibonacci process in PICT. Full PICT: __________ We are describing the Core part of PICT but the full language PICT uses syntactic sugar enabling us to write processes like factorial in an easier way. In Full PICT the factorial process can be written as it were a function definition similarly to how it is done in Haskell. It is also possible to have also a sequencing operation. A usual practice in programming language implementations: First define a Core Language and then define the whole language in terms of the core one. Before the actual compilation, derived forms are translated into the core language. Motivation? programs are easier to write and read. We shall not take into account Full PICT in our course. Session Types: ______________ We shall deal with a possible extension of PICT with session types in [FB7].