Programming components

[Joe Armstrong (AL/EAB)]

> -----Original Message-----
> From: Fabien Dagnat [mailto:fabien.dagnat@REDACTED]
> Sent: den 23 augusti 2005 14:28
> To: Joe Armstrong (AL/EAB)
> Cc: erlang-questions@REDACTED
> Subject: Re: Programming components
> 
> 
> Hello ,
> Joe Armstrong (AL/EAB) a écrit :
> > 
> >   Hello world,
> > 
> >   Comments?
> 
> > Open questions
> > ==============
> > 
>  > 4) Which style of component specification is best
> >    CSP, or RCP?
> To get intesting guaranties from the contract checker, I would like to
> keep some of the state information of CSP.
> What I like in UBF is this state information and I think that 
> state view
> is consistent with a Finite State Machine approach to concurrent
> programming.

   This is tricky - when you add all the states the CSP or UBF rapidly becomes
unreadable and becomes more and more like a program.

   If you omit the state and just use "stateless RPCs" then you loose a lot
of detail BUT the specification is readable.

    

> 
> >    2) Dynamic type checking of these types is trivial - but 
> can a type
> >     checker *prove* that your program follows a given 
> component spec.
> Previous works have demonstrated (I think), that if your 
> erlang program
> is not too complex (that is it does not use some dynamic code: eval,
> building of atoms, ...). We can prove some correctness.
> 
> The remaining problem is that of type equivalence in the presence of
> type aliasing. After "Type fileName = str()." do you consider that str
> == filename or not?

Yes - this is just pure syntactic sugar.

If I say

	Type foo = bar();
	Type bar = baz();
	Type baz() = int();

Then 12 is an instance of a foo, or bar or baz.

If I see (say) an <int>12</int> on some typed channel I can easily check
to see if it a foo or a bar or a baz, so type checking a contract is pretty easy if
I happen to know that at some point in time I am expecting a foo or a bar or a baz.

>  - If you consider them equivalent then the type checker 
> could <<*prove*
> that your program follows a given component spec.>>, but then the only
> interest of defining fileName type is documentation of the protocol.

    Yes - but with suitable type definitions the program nicely documented:

    Compare some part of an FTP like protocol

	Type fileName = str()
	Type getFile = {"get", fileName}
      Type theFile = {"yes", str()}
	Type noSuchFile = "no"

	getFile => theFile | noSuchFile

    With:

	{"get", str()} => {"ok", str()} | "no"

/Joe

>  - If you do not consider them as equivalent, the type checker must be
> able to relate Erlang value with those types (perhaps the programmer
> have to add type annotation to his program).
> 
> Fabien
> -- 
> Fabien Dagnat -- Maître de Conférences
>  Mel : Fabien.Dagnat@REDACTED
>  Web : perso-info.enst-bretagne.fr/~fdagnat
>  Tel : (0|33) 2 29 00 14 09 Fax : (0|33) 2 29 00 12 82
>  Adr : Ecole Nationale Superieure des Télécommunication de Bretagne
>        Departement Informatique
>        Technopôle Brest-Iroise - CS 83818 - 29238 Brest Cedex 3
>