LtU Forum

Eliminating left recursion

Does anyone have a reference to a correct algorithm which eliminates left recursion from a grammar? The one in Wikipedia is incorrect. Lots of youtube videos and lecture notes Google finds are also incorrect. All make the same mistake, they forget that a production A = N A X is left recursive if N is nullable. Requiring the grammar to be null free would be absurd since the algorithm itself inserts epsilon productions.

I also wish to extend the requirement to an attribute grammar of the form usually used in practice, with an extra symbol kind for AST construction, etc, which cannot be eliminated and yet recognises the empty string.

BTW: I'm looking for the basic algorithm. Lost my copy of the Dragon Book ;(

Splitting witnesses up

Hi,

I have an idea for an academic paper, and am seeking help for prior art and research.

My idea is about proof witnesses, and what to do when a group of witnesses contradict each other (software bug/logical inconsistency), and repairing the proof. Without going into details on the algorithm, the metaphor is simply to split witnesses up, using a mathematical plane to draw a group of witnesses into two groups: definitely lying (the witness whose account is proven contradictory/false), and somewhat certain (witnesses with similar testimonies who have not yet been proven contradictory/false, but might once asked further questions or may be proven "good enough" given the new questions/evidence we've asked the witness about). My idea comes from witness interrogation techniques in the real world.

Since I haven't been active in PLT for several years, my knowledge of what to search for and keywords to use on ACM and IEEE search engines is pretty weak, and I could use some tips.

Thank you very much!

Any recent developments on "active libraries" that I'm missing?

I'm interested in libraries that guide compilers for optimizations, but it
seems like there isn't much literature on this topic.

- Papers like "Generative Programming and Active Libraries" which usually just
briefly talk about the idea and give the same examples like Blitz++.

- There's a thesis, "Active Libraries and Universal Languages", which as far as
I can see is a bit too light on the practical examples and implementation.

Two implementations that work well:

- I think Haskell libraries that use GHC's rewrite rules are "active libraries"
in this sense

- The stream fusion library described in POPL'17 paper "Stream Fusion, to
Completeness" is an example that's a recent work and one that works really
well (although it has problems like leaking `code` type to the user in
functional arguments).

These are pretty much all I can think of as examples. I'm looking for recent
developments and other practical examples (i.e. ones that work well and/or used
widely). Any pointers would be appreciated.

Resources for implementing higher-kinded types?

I’m working on a language and I would like to implement polymorphism over type constructors (for functor, applicative, monad, etc.) but I’m uncertain how to proceed.

Can anyone recommend tutorial-style resources or sample implementations of this? I’ve read that higher-order unification is involved, and that inference is undecidable without certain restrictions. Is that accurate? Would it be difficult to retrofit a (more or less) standard implementation of Hindley–Milner?

Seeking contributors to psyche-c

Dear guys,

I would like to announce an open-source tool that we are developing: psyche-c. It completes missing parts of C programs, so that you can have a fully compilable program. In other words, it does type inference and stub generation for missing functions. The tool has an online interface, which you can use: http://cuda.dcc.ufmg.br/psyche-c/

For instance, if you feed it with this program, taken from Sedgewick's book:


void TCdfsR(Graph G, Edge e) {
link t;
G->tc[e.v][e.w] = 1;
for (t = G->adj[e.w]; t != NULL; t = t->next) if (G->tc[e.v][t->v] == 0)
TCdfsR(G, EDGE(e.v, t->v));
}

Then psyche-c will give you back these declarations:

typedef struct link {int v;struct link* next;}* link ;
typedef struct Graph {int** tc;struct link** adj;}* Graph ;
typedef struct Edge {int v;int w;} Edge ;
struct Edge EDGE (int,int) ;

Notice that is reconstructs recursive types that are pretty complicated. We have used psyche-c to reconstruct missing code in the GNU Core Util programs and in all the Sedgewick's examples (on graphs), for instance. Psyche-c is good for code completion, as a helper to debug programs, and even to reduce compilation time. It uses a unification based type-inference engine, and has a few tricks to parse C, even when missing declarations. If you would like to contribute, the code is available at https://github.com/ltcmelo/psychec.

Regards,

Fernando

How to name the inverse functions of constructors

I am working on the design of a language (Albatross) which allows for static verification. It has a strong functional core. One of the most important types in a functional language is the inductive or algebraic type. One of the most prominent examples is a list. E.g. a list type in Albatross is declared as follows.

A: ANY
class
    LIST[A]
create
    []
    (^) (head:A, tail:LIST[A])
end

It has the constructor [] to create an empty list and the constructor ^ to construct a new list by prefixing an already constructed list (tail) with a new element (head).

From a nonempty list we can extract the head and the tail with the following functions.

head(l:LIST[A]): A
    require
         l as _ ^ _
    ensure
        -> inspect
               l
           case h ^ _ then
               h
    end

tail(l:LIST[A]): LIST[A]
    require
         l as _ ^ _
    ensure
        -> inspect
               l
           case _ ^ t then
               t
    end

The functions head and tail reverse the effect of the constructor ^. I am looking for a name on how to describe these type of functions.

The most immediate ideas are _desctructors_ or _unconstructors_ which I don't find very appealing. A better name might be _inverse constructors_ which seem to precisely describe what they are, but sound a little bit clumsy.

Does anyone have a good idea on how to name these animals?

Some background information on why I need these type of functions:

Algebraic data types are a great tool, but they are not always the appropriate tool. E.g. in order to describe natural numbers their implementation is straighforward but awfully inefficient (this is one of the big problems when you want to extract source code from Coq). There are two ways to describe natural numbers with an efficient implementation. Either as machine numbers with modulo arithmetic or as arbitrary sized numbers where the components are machine numbers.

Machine numbers are not objects of algebraic type. But they are similar. The have constructors (zero and successor) and an induction law. Furthermore they have discriminator functions (n = 0) to decide how the number has been constructed and an inverse constructor (predecessor).

As soon as a type has an induction law (which implicitely defines the constructor functions), discriminator functions and inverse constructors the compiler can treat these types like inductive types in order to define recursive functions (which are guaranteed to terminate), do pattern matching etc. The discriminator functions and inverse constructors are necessary for the compiler in order to be able to compile pattern matching expressions into executable code.

In my opinion these pseudo algebraic/inductive types will be a great tool. Therefore I need good notions and names to express properties well.

Thanks for any help.

Language Description

Best value for overloading?

There exist various approaches to overloading, including:

* type classes of various kinds
* traits
* implicits [2]
* multimethods
* other systems [1,3]

What seems to offer the best value for investment effort, expressiveness, and type safety?

For instance, multimethods are pretty flexible and uniformally allow a form of type-based and case-based overloading, but it seems quite difficult to capture accurate types with all the expressiveness we expect of ML functions, eg. first-class functions require intersection types and subtyping.

Type classes and traits seem more or less equivalent, but have problems with overlapping and named instances, a problem shared by [1] I believe. Implicits seem promising, and properly handle named and overlapping instances.

[1] A Second Look at Overloading
[2] The Implicit Calculus: A New Foundation for Generic Programming
[3] A Theory of Overloading

List of POPL 2017 papers with crowd-sourced preprint links

https://github.com/gasche/popl2017-papers/ has a list of POPL 2017 papers with crowd-sourced links to the preprints. The deadline for camera-ready version (a version provided by the researchers that takes reviewers' comment into account) is only on November 7th, so one should expect more preprints to be available after that.

Feel free to mention any paper that catches your interest. If you are very curious in a particular work that does not have an online preprint, sending an email to the authors to ask them whether they plan to have a preprint accessible online can help a lot.

Interesting use cases for universal quantifiers in rank 2?

Trevor Jim’s System P2 types the same terms as the second-rank System F2, but function arguments can only be typed as (finite) intersections of simple types. This restriction is reasonable and also seems to correspond neatly to the inner workings of a compiler which specializes polymorphic functions for every usage (such as Rust’s, IIRC). What do we lose, relative to F2? Here are the things that I can think of (in fact, they also apply to unrestricted System P, which prohibits universal quantifiers in negative positions):

  • The ST monad of Peyton Jones et al. famously uses second-rank universal quantification to prevent imperative state from leaking outside, by defining runST :: forall a. (forall s. ST s a) -> a and threading the dummy parameter s through all related imperative things — e. g., imperative variables are accessed by readSTRef :: STRef s a -> ST s a and writeSTRef :: a -> STRef s a -> ST s (). Dynamic event switching in reactive-banana is guaranteed free of time leaks using a similar mechanism. (It sort of makes sense that we lose this: it is difficult to see how a universally quantified type could be inferred for any argument. Though…)
  • Induction principles for non-regular datatypes have rank-2 types (always?). It seems to me that so do types defined using Haskell’s ExistentialQuantification extension.

Anything else?

Side note: What is then the class of all datatypes whose induction principles fit into P2? Is it interesting or any bigger than that for HM? I don’t understand what intersections could mean as eliminator arguments.

How is structural typing checked?

If a language is decided to have structural type, how are the types checked?

With a nominal type system I can just have a table with the names, and lookup it. However with structural types is necessary to encode more info so I can know how do it.

How are this info encoded? How are the check performed?

XML feed