## User login## Navigation |
## LtU Forum## Eliminating left recursionDoes 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 upHi, 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 - Papers like "Generative Programming and Active Libraries" which usually just - There's a thesis, "Active Libraries and Universal Languages", which as far as Two implementations that work well: - I think Haskell libraries that use GHC's rewrite rules are "active libraries" - The stream fusion library described in POPL'17 paper "Stream Fusion, to These are pretty much all I can think of as examples. I'm looking for recent ## 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-cDear 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:
Then psyche-c will give you back these declarations: 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 By pronesto at 2016-11-07 23:52 | LtU Forum | login or register to post comments | other blogs | 1395 reads
## How to name the inverse functions of constructorsI 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.
It has the constructor From a nonempty list we can extract the head and the tail with the following functions.
The 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 ( 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. ## Best value for overloading?There exist various approaches to overloading, including: * type classes of various kinds 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 ## List of POPL 2017 papers with crowd-sourced preprint linkshttps://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 F, 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 _{2}F? Here are the things that I can think of (in fact, they also apply to unrestricted System _{2}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 By Alex Shpilkin at 2016-10-23 00:23 | LtU Forum | login or register to post comments | other blogs | 1417 reads
## 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? |
## Browse archives## Active forum topics |

## Recent comments

35 min 15 sec ago

8 hours 54 min ago

9 hours 41 min ago

18 hours 17 min ago

1 day 1 hour ago

1 day 10 hours ago

1 day 12 hours ago

1 day 16 hours ago

1 day 19 hours ago

2 days 13 hours ago