run ()





run (() | () | ())


                   _
x!y   stands for   x y

x?y=P stands for   x(y).P



in PICT also the syncronization signal: []
and "concrete" values



run ( print!"peering"
    | print!"absorbing"
    | print!"translating"
     )




peering
absorbing
translating



print is NOT a command, but the name of a channel
enabling to communicate to the "hidden" process that prints



run ( x?[] = print!"Got it!"
    | x![]
    )




Got it!



run x?[] = (print!"Got it!" | x![])






run ( x!y
    | x?z = z!u
    | y?w = print!"Got it!"
    )


Got it!




run ( x!y
    | x?z = a!z
    | a?w = print!"Got it!"
    )


Got it!




a channel is a value

tuple of values are values  [v1...vn]



x, [x y], and [x [[y x]] y [] x]  are then values


The "signal" is then simply the empty tuple


For the time being strings are values only for the print channel


In the version of  pi-calculus only channels were values


x!v

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)

x@p    (layered pattern)


run ( new ch: ^[String String]
      ( ch!["Hello" "world"]
      | ch?a@[b c] = ( print!b
                     | print!c
    ) )              )



Hello
world



>>> PICT is typed!!!








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



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



Variable declarations:

val i = 50
val b = true
val message = "Hello"



types are inferred


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







     type X = T




 - higher-order polymorphism,
 - subtyping, 
 - records, 
 - recursive types,
 - type-inference mechanism.

                       


                     CHANNELS

New channel names are introduced by 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.”



(Not the only possible approach: channels carrying any
sort of values.
Types can be used to ensure the right sequence (protocol)
Session Types.)




   new x:^Int
   new y:^Int
 
   run x!y


Expected type does not match actual since ^Int is not
a subtype of Int since ^Int and Int do not match.



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)


  run ( new x:^[]
        ( x![]
        | x?[] = ()
      ) )


   run ( new x:^[]
         run x![]
         x?[] = ()
        )



alpha-conversion for bound channel names:

  run ( ( new x:^[]
          ( x![]
          | x?[] = ()
        ) )
      | ( new x:^[]
          ( x![]
          | x?[] = ()
          ) 
         ) 
       )


scope extrusion:

  run ( new x:^[]
          ( z!x
          | x?[] = print!"Continuing..."
          ) 
       )



replication:

in pi-calculus infinite behaviours provided by 
means of replication operrator !P (*P)

in PICT, use of def construct


  def hailer [] =
    print!"Hail!"



so, it is like replication restricted to 
input-prefixed processes


process above equivalent to 


  new hailer : ^[]

  run ( hailer?[] = print!"Hail!"
      | hailer?[] = print!"Hail!"
      | hailer?[] = print!"Hail!"
      | ...
      )


so hailer channel 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!




recursive processes:

  def hailer n:Int =
    if (== n 0) then
                    ()
    else
      ( print!"Hail!"
      | hailer!(dec n)
      )

  run hailer!5


Hail!
Hail!
Hail!
Hail!
Hail!


mutually recursive processes:

 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




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


Version of "if" also for expressions (in the functional sense)



Running the compiler

pict prog.pi






typechecking 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




  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, once received ch, 
could use it also to receive integers

Violation of POLA!!!  (PrincipleOfLeastAuthority)
                       -        - -    -


So we rewrite the program as


  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 typecheck

new ch:^Int
    ^^^^^^^
with

def consumer channel:?Int = ...  ?
             ^^^^^^^^^^^^


Subtyping is used by typececker!!!!


      ^Int < ?Int 

      ^Int < !Int


Exercises:

-- describe the subsumption rule used by PICT type system


-- define a formal system for subtype judgments of PICT types

                    S < T








Another refinement of channel types:

                Responsive Output channels



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 more difficult to implement




Types and Type system used to statically know
which outputs will communicate with definitions

channels created by def have type /T


  new x : ^[/Bool]
  
  def d b:Bool =
    if b then
      print!"True"
    else
      print!"False"

  run x![d]
  run x?[a] = a!false
 

False


from the type of x 
a!false 
knows that it is communicating with a def.


So,
types as sort of directives to the compiler .....



Useful... but I do not like it!  





                      /T < !T



  new y : ^[!Bool]

  run y![d]

  run y?[a] = a!false



False



An allowed cast from !T to /T








The primitive channel "pr"

             pr : /[String /[]]






Using pr:

 def d [] = print!"done"

 run pr!["pr... " d]


pr... done


  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



allowed cast:

  new c : ^[]

  run pr!["pr... " (rchan c)]
 
  run c?[] = print!"done"


pr... done



In a programmaing language based on the notion of process,
basic operations like addition, multiplication etc.
are basic processes

So, +, * etc. are channels through which we
communicate with such basic processes


+ : /[Int Int /Int]


Example: 

  run +![10 20 printi]

30








  run ( new r:^Int
        ( +![10 20 (rchan r)]
        | r?sum = *![sum 30 printi]
      ) )


900





  run ( new r1:^Int
        new r2:^Int
        ( +![10 20 (rchan r1)]
        | +![30 40 (rchan r2)]
        | r1?sum1 = r2?sum2 = *![sum1 sum2 printi]
      ) )



2100


PICT has syntactic sugar 
that enables us to write such programs easier!!!



Example: factorial  (no syntactic sugar)


  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: Fibonacci




Characters and Strings
-----------------------




print defined in terms of the lower-level 
predefined channel pr:


def print s:String =
  ( def r[] = ()
    pr![s r]
  )


=============================

A usual practice in programming language implementations:

Define a Core Language and then define the whole language in
terms of the core one.

Before the actual translation, derived forms are translated
into the core language.

Motivation?  programs easier to write and read.




              Complex values


Simple values in the core language:

 (channel) variables
 basic values and channels (+,*,..)
 record values


they are entities that can be passed along channels
and partecipate in pattern matching 



PICT extends the core language with

Complex values: 
              expressions of the form (d v) 
              to be used in any place a simple value 
              is expected



     x!(new n:T n)


     x![23 (new x:A x) (new y:B y)]


Notice that, since the name of a channel is a value
we can also have something like

             (d v)!(d' v')


We need to formally define the "meaning" of complex values
           --------


(1) first define a "continuation-passing" style 
    interpretation of complex values, [[v → c ]]
(2) then define a traslation for process expressions 
    containing complex values




Let v be a complex value and c a channel.
We define

             [[v → c ]] 

denotes a process that evaluates v and sends the resulting 
simple value along c





The interpretation [[-]] defined by induction on the
syntax of value expressions



   [[x → c]] = c!x




   [[k → c]] = c!k



   [[(new x:T v) → c]] = (new x:T [[v → c]])




[[(def x1 a1 ... and xn an v) → c]] =

    (def x1 [[a1]] ... and xn [[an]] [[v → c]])




[[(run e v) → c]] = ([[e]] | [[v → c]])





[[if:T v then v1 else v2 → c]] =

(def d x:Bool = if x then [[v1 → c]] else [[v2 → c]] [[v → d]])



SEE TEXT for records

      [l1 fv1...ln fvn] has type [l1FT1...lnFTn]
  _____________________________________________________
    [[[l1fv1...lnfvn] → c]] = [[ | l1fv1...lnfvn → c]]







      [[l1fv1...lnfvn | → c]] = c![l1fv1...lnfvn]





                     vi has type Ti
   ___________________________________________________________________________
     [[l1fv1... | livi...lnfvn → c]] = 
    (def ci xi:Ti = [[l1fv1...lixi | li+1fvi+1...lnfvn → c]] [[vi → ci]])



We can now translate process expression containing 
complex values:


[[v1!v2]] = 

(def c1 x1:T1 = (def c2 x2:T2 = x1!x2 [[v2 → c2]]) [[v1 → c1]])



where T1 and T2 are the types calculated by the type-checker
for v1 and v2



[[v?p=e]] = 

(def c x:T = x?p=[[e]] [[v → c]])

where T is the type calculated by the type-checker for v



[[if v then e1 else e2]] = 

(def c x:Bool = if x then [[e1]] else [[e2]] [[v → c]])



Exercise: which approach to typing for PICT (a' la Curry, or Church)




            Value Declarations
            __________________



A construct to bind values to names:


   (val x = (new n:T [n n]) 
    e)


binds x to the result of evaluating (new n:T [n n]) and
then executes e







[[(val p = v e)]] = 

(def c p = [[e]] [[v → c]])










Since declarations can also appear in value expressions, 
we also need to add a clause to the definition
of CPS-conversion for values:


[[(val p = v1 v2) → c]] = 

(def d p = [[v2 → c]] [[v1 → d]])









             Application
             ___________


We extend the syntax with 

               (v v1...vn)


which enables to look at def channels as functions






def double [s:String r:/String] = +$![s s r]


now, instead of  

        double!["soothe" print]

we can write

              print!(double "soothe")

soothesoothe


by interpreting (v v1...vn) as follows


[[(v v1...vn) → c]]  =   [[ v![v1...vn c] ]]


(we can also use labelled values l1 fv1 ... )


Let us see what is the result of the translation of
print!(double "soothe")

[[print!(double "soothe")]]

=

(def c1 x1:/String = 
  (def c2 x2:String = x1!x2 
      [[(double "soothe") → c2]])
 [[print → c1]])

=

(def c1 x1:/String = 
  (def c2 x2:String = x1!x2 
      [[ double!["soothe" c2] ]])
 c1!print)


= (for simplicity's sake we translate [[ double!["soothe" c2] ]]
   directly in double!["soothe" c2] . We can assume 
   the translation of Core PICT expressions or processes
   to be the identity)


(def c1 x1:/String = 
  (def c2 x2:String = x1!x2 
      double!["soothe" c2])
 c1!print)

To convince ourselves that the above process
does exactly what 

double!["soothe" print] 

does, let us execute it (mind that there is the def of double
that precedes all)

(def c1 x1:/String = 
  (def c2 x2:String = x1!x2 
      double!["soothe" c2])

 c1!print)

--> 

(def c1 x1:/String = 
  (def c2 x2:String = x1!x2 
      double!["soothe" c2])
 
 (def c2 x2:String = print!x2 
      double!["soothe" c2]) )

-->

(def c1 x1:/String = 
  (def c2 x2:String = x1!x2 
      double!["soothe" c2])
 
  (def c2 x2:String = print!x2 
      +$!["soothe" "soothe" c2]))

the string appending process will then execute
the process  c2!"soothesoothe" whose execution
will cause the execution of

print!"soothesoothe"

che provoca la stampa di

soothesoothe










Exercise: translate the following in core pict

  x![(* (+ 2 3) (+ 4 5))]





Exercise: rewrite previous exercises (like fact or fibonacci)
          using application syntax (and also the function
          definition syntax as defined below)





The defs that can be looked at as functions have the form

def f [a1:A1 a2:A2 a3:A3 r:/T] = r!v

(the v can be looked at as the "result" of the function
that is given through the channel r)





A special syntax for defs that can be looked at 
as function definitions


instead of 

def f [a1:A1 a2:A2 a3:A3 r:/T] = r!v



we can write

def f (a1:A1 a2:A2 a3:A3):T = v




Anonymous process declarations


(def x p = e x)


example of use:  (def x p = e x)!v






So, anonymous function can be defined by means of the
following derived form

     \p=e

stands for (is translated into)

    (def x p = e x)


Exercise: we can write in PICT the following process

new y: ^Int

 y!((\x=(+ x 1)) 4)

Show, using the translation),
that the effect of executing the above process
is exactly that of executing y!5




Example: using the "for" process.


"for" process defined in the standard library



  def for [min:Int max:Int f:![Int /[]] done:/[]] =
   ( def loop x:Int =
      if (<= x max) then
        ( new c : ^[]
          ( f![x (rchan c)]
          | c?[] = loop!(+ x 1)
        ) )
      else
        done![]
 
     loop!min
   )





we can use "for" as in the following process

  run ( new done : ^[]
        ( for![ 1 4
                \[x c] = (printi!x | c![])
                (rchan done)
              ]
        | done?[] = print!"Done!") )


1
2
3
4
Done!



Another use of anonymous functions: definition of a
record whose fields are two anonymous functions
that take simply a syncronization signal as output.


  val r = [
    one = \[] = print!"Low hangs the moon"
    two = \[] = print!"O it is lagging"
  ]


run (r.one![] | r.two![])


O it is lagging
Low hangs the moon


Records can be used to implement distributed objects.




         Sequencing



  run
   ( val [] = (pr "the ")
     val [] = (pr "musical ")
     val [] = (pr "shuttle")

     ()
   )

the musical shuttle


See the (translation) semantics to understand its meaning




“invoke an operation, wait for a signal as a result, 
and continue” 

appears so frequently that it is worth providing some 
convenient syntax.

  sequential declaration:

    v;      is translated into      val [] = v