LtU Forum

A Modular, Verifiable Exception-Handling Mechanism

A while back I began tinkering with the idea of continuation-carrying exceptions as an approach to divide error handling policy from the mechanism. Of course, I later discovered I was putting old wine into new bottles. Common Lisp follows a similar approach with its Condition/Restart mechanism.

Anyhow, at that time a friend pointed me towards A Modular Verifiable Exception-Handling Mechanism by S.Yemini and D.Berry (1985).

The following varieties of handler responses to an exception can be identified in the literature:

  1. Resume the signaller: Do something, then resume the operation where it left off.
  2. Terminate the signaller: Do something, then return a substitute result of the required type for the signalling operation; if the operation is not a value returning operation, this reduces to doing something and returning to the construct following the invocation of the operation. This includes using alternative resources, alternative algorithms, and so on.
  3. Retry the signaller: Do something, then invoke the signaller again.
  4. Propagate the exception: Do something, then allow the invoker of the invoker of the signalling operation to respond to the detection of the exception.
  5. Transfer control: Do something, then transfer control to another location in the program. This includes doing something and then terminating a closed construct containing the invocation.

This paper presents a new model for exception handling, called the replacement model. The replacement model, in contrast to other exception-handling proposals, supports all the handler responses of resumption, termination, retry, and exception propagation, within both statements and expressions, in a modular, simple, and uniform fashion. The model can be embedded in any expression-oriented language and can also be adapted to languages which are not expression oriented with almost all the above advantages. This paper presents the syntactic extensions for embedding the replacement model into Algol 68 and its operational semantics.

Without [an exception-handling mechanism], too much information is not hidden and coupling is high. Either the signaler has to be told more about what the invoker is doing, so that the signaler can do what the invoker would want done, or else the invoker has to be given more implementation details so that it can do the exception checking.

Whether the exception-handling mechanism be continuations or something else, I'd really love to see the modern stack-based languages (Java, C++, etc.) implement something much more along these lines. I have been bitten far too often by the high coupling that comes from the inability to separate error handling policy from the exception handling mechanism.

Programmer book club

Some here might be interested in contributing to this thread.

I once made a list of suggestions, some of which may still be relevant.

Constructor classes

What is the benefit of a constructor class in a language like Gofer over type classes in a language like Haskell? Is there way to implement one in terms of the other? If they are worth it, can constructed classes be elegantly implemented in a language that does not support them? I find these types of discussion very interesting. Anyone who can point in me a direction, I would greatly appreciate it.

In which sense Joy is functional?

I am confused. I understand that the language Joy is regarded as a functional language. It also seems that is closer to Backus' FP than, say, Haskell.

The Joy FAQ (http://www.latrobe.edu.au/philosophy/phimvt/joy/faq.html) states that it is functional because expressions are functions operating on a stack, and juxtaposition is function composition. That definition feels (to me) like cheating.

Could not one also define a language with assignments and call it "functional", intepreting expressions as pure functions operating on an environment?

I mean, every imperative language can be implemented with the State monad, and that doesn't make it functional (I think).

Perhaps my question makes no sense, and is just wordplay. I'd really like to know what you think.

OOPSLA 08

I went over the OOPSLA'08 program, and these two items caught my eye:
(1) Constrained Types for Object-Oriented Languages
(2) Whiteoak: Introducing Structural Typing into Java

Looking at the abstracts of these papers (and also other abstracts from the program) brought up a thought that's been wrapping around my mind for sometime: The border between programming paradigms not as clear as it used to be.

Personally, I think this is a good thing. For example, I believe that closures are very useful in OO. My only problem with this line of thought is that I also believe in the beauty of minimalism. A language that borrows constructs from several paradigms will (usually) not be minimal. A conundrum?

On the (perceived) equivalence of static and dynamically typed reflective programming languages

Hi. I'm new here.

I've dug up some old topics on the issue of the dynamic/static-typing cold-war/debate, and considering this to be a predominantly pro-static, all-determinism and pro-PF message-board, I would lay down this question as a test of either my misunderstanding, or as a fair argument for a particular point which I think hasn't been mentioned.

One claim that's been in many topics (especially on this forum) and recent papers on modern type theory (even though I have no idea about its origins) is the possibility to construct a 'Universal' type to capture the notion of run-time typing:

data Univ = Inte Int | Str String | ...

This has been used to justify the claim that, since such a hack can be used to bypass the type-checker, statically typed languages can directly express all programs in dynamically typed ones, but such a statement isn't true in the reverse.

One argument that has been thrown against this is that, currently, this isn't very convenient (especially in SML, Haskell and any other widely used language with type-inference). One would be forced to work with explicit type-constructors, functions would have to be 'lifted' (lift (+) :: (Int -> Int) -> (Univ -> Univ)) in order to operate on data of this sort, and would have to be 'flattened' again (Univ -> Int) to be of any use in order to interact with the outside program.
One rebuttal has been made is that the blame lies /not/ with type-systems in general, but how they are currently used and implemented.
And so I attempt to debunk this claim, by stating that the perceived shortcomings of latent typings lie not with the concept as a whole, but with how (the majority of) current languages (Ruby, Python, PHP) go about it. I should mention now that I am most familiar with Scheme (and Lisp in general) and intend to use this to put forward my arguments.

Static typing is essentially a method by which a program can be mechanically checked to guarantee that when two functions (f and g) are composed (f o g)( x ): x belongs to the domain of g; the codomain of g is the domain of f; and as such all functions and/or operators are consistent in this fashion. I know very well that static typing has a much greater potential than that (as evidenced in the possibilities of dependent types, GADTs, type/module hierarchies and so on). This checking is performed during program compilation (in other words, prior to the program actually being run) and does NOT add any capability or structure to the code, and has no effect upon the execution of the algorithm.

Many modern (mostly dynamically typed) functional languages are implementing a form of compile-time metaprogramming, and allow direct access to manipulate or query the source code of the surrounding program. My question is, isn't static type checking already possible to implement through that, and therefore a dynamically-typed programming language with metaprogramming features (like Lisp) is MORE expressive in the criteria of compile-time validation. PLT Scheme programmers will be aware of this if they've ever read up on or used MrSpider and/or MrFlow.

Of course, statically-typed languages with such features would be capable of doing the same. But I'd like to digress for a moment to say that the pain of Template Haskell, F# and integrating features like macros on them is plain hell.
Anyway, to deny the above the above statement (not about the criticism of Template Haskell which is sure to start a flame-war) is plain hypocritical for advocates of static-typing and the argument about its superiority previously mentioned. A programming language with features allowing compile-time reflection and processing would easily be capable of isolating a few-modules, marking them 'typed' and sweeping them with the Hindley–Milner magic.

Of course, this would all be quite impractical. Implementing / extending a type-system is a difficult task (even though so far I'm cool with the current and most popular soft-typing attempts) but the same could be set for the Universal type constructor and all the baggage that comes with it. Getting the two worlds to talk to each other is a pain.

Static typing is a limited form of compile-time sweeping. Q.E.D?

Once again, the playing field is level, and the choice between the two is almost entirely about preference.

Syntactic/Semantic Control in MDA Framework

Hi at all,
I'm an italian student and I'm working on a thesis about semantic verification of xml models in MDA (Model Driven Architecture) context.
MDA is an OMG standard based on visual programming languages and automatic generation of code.
In particoular i'm working on a framework that allows programmers to define SOA three tiers web applications.
The programmer can define frontend and backend of these applications in terms of workflows (i.e. graphs).
The problem is that the syntax of these visual programming languages (the graphs for frontend and backend) is underconstrained, so a programmer can define senseless combinations of states.
There are at least two types of errors:

1) Two (type of) states are connected with a transition, but this transition is semanticaly senseless

2) Two (type of) states are connected with a transition, but a pre/post-condition involving other states doesn't hold. For example a transition between two (type of) states is admitted if and only if there is a transition from the fomer/latter state to another state.

The first type of constraints is easy to impose: a simple table could be added to the framework so these type of senseless cuold be checked on-the-fly.

The second type of constraints involve more complex reasoning, and i think there are basically two types of solutions:

a) To check the models (graphs) defined by the programmers, using techniques inherited from Model Checking (formal verification). In this case the control is a post-development control.

b) To define a precise syntax and semantic using graph grammars. I'm quite ignorant in the domain of graph grammars, so i don't know if these instuments are intended for this purpose.

I'm writing to you 'cause i think the problem about syntax and semantic of visual programming languages is undertheorized.
The first solution i proposed has some problems: model checking is intended to check concurrent system, and not to check the problem i described. On the other and, logic, and CTL logic in particoular, is general enough to represent every type of constraint. Still, there are some computational complexity problems (i.e. state explosion).
The second solution is only a vague idea: i don't know graph grammars...
I would like some opinions, references, suggestions or something else.
I know this post is quite general, but there are too much questions that i will describe later, on demand, in order to avoid to write a too long post.
Best regards,

Alberto

DSL or dialects used inside compilers

Hello All,

I am interested in languages used inside compilers. Of course, for front-ends, there are lot of parser code generators (like ANTLR, bison, menhir, ...) and some more sophisticated ones (e.g. attribute grammar based).

Also, functional languages are not only used for their own compilers (eg ocaml being coded in ocaml) but also in other source code related tools like Frama-C (a C static analyzer framework coded in Ocaml).

And code generation also uses specialized formalism (e.g. GCC machine description) and all the BURG like tools.

And even GCC has a middle end lisp dialect (my MELT branch) designed for middle end transforamtion and static analysis.

But there have surely been many other dialects or DSL used inside compilers. Any hints?

Regards.

Inspiring Papers

In the interest of discovering some further reading material,
I have created a quick survey open to all LtU'ers..

Please name:

1) One of your favourite papers of all time
2) A recent paper you consider ground-breaking in some way
3) A lesser-known paper that you feel ought to be more widely read

Any PL topics welcome!

FringeDC Formal Meeting Oct 11th 6PM- Writing a compiler for a functional programming language

www.lisperati.com/fringedc.html

FringeDC is a group for people interested in fringe and functional programming languages (Lisp, Haskell, Erlang, Prolog, etc) in the DC area.

This Saturday Andrew Harris will discuss the geeky internals of his EmbeddedML project, which aims to bring functional programming to the world of microcontrollers. It's a lightweight system that generates generic C code, allowing it to support many low resource devices.

This meeting will be presented in conjunction with HacDC, the one-and-only workshop for microcontroller geekery in DC. After the presentation, we'll go out for some beer to discuss all the latest programming topics of the day. Everyone is welcome to join us!

Date: Oct 11th 6PM
Address: HacDC headquarters- 1525 Newton St NW, Washington DC 20010 USA
(Near corner of 16th and Newton NW)
The closest MetroRail station is Columbia Heights (Green Line). You can check online to see the next train arriving there. The S1-2-4, H1, and H2-3-4 buses go right by our location.
Approach on the 16th St side of the building. Look for the red doors. We are on the third floor. Follow the signs to our space after signing in with the guard.

http://maps.google.com/maps/ms?ie=UTF8&hl=en&msa=0&msid=112368426664365520724.00044a72684e313eb7ebd&ll=38.932307,-77.03521&spn=0.008813,0.007253&z=17&iwloc=00044a727d23d707d87b9

-Conrad Barski, M.D.

XML feed