Type checker as staged computations [Fwd: [stack] Digest Number 26]

[Massimo Dentico]

On Concatenative mailing list concatenative@egroups.com
- http://www.egroups.com/group/concatenative

Massimo Dentico wrote:
> 
> Mark van Gulik wrote:
> > [...]
> > I'm mostly concerned, however, with the ability to build *restrictions* in the
> > language.
> 
> I completely agree with this. In particular, the key concept is
> ".. the ability to build *restrictions* in the language". This means
> that *you*, the programmer, build the restrictions when you really
> need it and it's not the language designer that in arbitrary way
> restricts you.
>
> The ability to restrict a language is crucial to reconcile
> extensibility and safety. Plan-P is such an example:
> 
> - http://www.irisa.fr/compose/plan-p/
> 
> ---------------------------------------------------------------------------
> 
> PLAN-P : a Programming Language for Active Networks and Protocols
> 
> Active networks are aimed at incorporating programmability into the
> network to achieve extensibility. An approach to obtaining extensibility
> is based on downloading router programs into network nodes. Although
> promising, this approach raises several critical issues: expressiveness
> to enable programmability at all levels of networking, safety and security
> to protect shared resources, and efficiency to maximize usage of bandwidth.
> 
> PLAN-P is a domain-specific language for implementing application-specific
> protocols. It allows applications to program network routers. [...] The key
> characteritics of PLAN-P are:
> 
> [...]
> 
> Safety and security. Because the language is restricted, many properties
> are automatically verifiable. For exemple PLAN-P ensures global termination
> and guarantees no packet loss or exponential duplication.
> 
> [...]
> 
> ---------------------------------------------------------------------------
 
[...]

> > As for "the language is the type system" in Avail...  that's only because I
> > got to the implementation of the type system before most of the other things
> > in my stacks of notes.  Hm, maybe you meant it in the sense of "the type
> > declarations of Avail are written in Avail code".  I think I was
> > interpreting it more like "everything interesting in Avail has to do with
> > the type system" when I first read it.
> 
> This is what I meant: "the type declarations of Avail are written in Avail code".
> Another way to express it is: "you blur the distinction between expression
> languages for values and types". This means that you reduce the number of
> different syntactic *and* semantic elements in the language. This is closely
> related to staged computations in my mind:
> 
> a type system in a language (statically or dynamically checked) is useful
> for restricting run-time values of expressions (and in case variables);
> a static typing ensures at compile-time that the program will satisfy these
> restrictions; but, in a language where type declarations are written in
> the language itself, the only element that differentiates these (type
> declarations) and other code is the stage (compile-time vs run-time).
> In a language which offers explicit stage annotations (as in Forth with
> words like IMMDEDIATE) the distinction between the language and the type
> checker is completely blur (the code for the checker is not different
> from other IMMEDIATE code).
> 

Of course, such a language needs to be carefully designed. In fact is
simple to see problems of circularity: "how to type check the type
checker?". Note that this is usually hidden but *always* present:
a compiler designer could write (and usually do) the compiler, and so
the type checker, in a statically typed language.

Comments? Is it relevant for Tunes HLL?

-- 
Massimo Dentico