13

This is an interesting question! As Anthony's answer suggests, one can use the usual approaches to compiling a non-dependent functional language, provided you already have an interpreter to evaluate terms for type-checking. This is the approach taken by Edwin Brady. Now this is conceptually simpler, but it does lose the speed advantages of compilation when ...


10

There is a naive algorithm for programs with bounded-size inputs: enumerate all programs in order of increasing length (or execution time, which is a bounded function of the length). If you can prove that the program is equivalent to the original, stop; otherwise keep searching. This algorithm is sound. In order for it to be complete, you need to be able to ...


10

Edwin Brady's PhD thesis outlines how to construct a compiler for a dependently typed programming language. I'm not an expert, but I'd say it's not extremely harder than implementing a System F-like compiler. Many of the principles are quite similar and some are the same (e.g. supercombinator compilation.) The thesis covers many other concerns.


9

There's a very recent survey paper available on Alias Analysis for Object-Oriented Programs. It will be published in April in the LNCS state-of-the-art volume (gratuitous advertising alert): Aliasing in Object-Oriented Programming: Types, Analysis and Verification. Lecture Notes in Computer Science, Vol. 7850. Dave Clarke, Tobias Wrigstad, James Noble (Eds....


8

JHC uses a different approach. The compiler's intermediate language is a dependently typed lambda-calculus where there is no distinction between types and values. JHC therefore can perform a case analysis on the type parameter of a function and call the correct overloaded function directly. The JHC website goes into some depth on the implementation, as ...


8

Implicit Complexity has taught us that (some) complexity classes can be classified by type systems, in the sense that there are type systems that only accept polynomial programs, for example. One more practical-minded offshoot of this research is RAML (Resource Aware ML), a functional programming language with a type system that will give you precise ...


8

I assume you are asking whether a "reasonable" system exists that can express these functions and also also decide whether any two expressible function definitions define the same function. (An unreasonable system would be, for example, the language which has only the two function definitions above in it...) Both of functions are expressible in Buss's ...


7

In the strictest sense, there is no real difference between syntax errors and semantics errors, at least as far as language theory is concerned: the only salient difference is the complexity of the automaton required to recognize that language, with, e.g. Context-free languages only requiring pushdown automata (PDA) General recursive languages requiring ...


7

The COSTA tool developed by the COSTA research group does exactly what you want. Given a program (in Java bytecode format), the tool produces a cost equation based on a cost model provided by the programmer. The cost model can involve entities such as runtime, memory usage, or billable events (such as sending text messages). The runtime equation is then ...


7

You need to identify the lattices involved in each case. Let $(\wp(S),\subseteq)$ be the lattice of all subsets of a set $S$ ordered by subset inclusion. A function $f:\wp(S) \to \wp(S)$ is monotone if for every pair of sets $x$ and $y$, if $x \subseteq y$ it also holds that $f(x) \subseteq f(y)$. The definition applies more generally to functions $f: L \...


6

One approach is described by Georgios Fourtounis and Nikolaos S. Papaspyrou. 2013. Supporting Separate Compilation in a Defunctionalizing Compiler. SLATE 2013. As @gasche mentions: A different approach at the problem would be to consider that each module can define its own "defunctionalized functions" type and dispatcher/handler. You can "link" those ...


6

The standard presentation of program transformation ideas is unsound, quite unfortunately. They usually think of program transformation as forward deduction. Using equational reasoning, you can deduce new facts from the old program, and lo and behold, it gives a better program! While the new facts are quite clearly facts, nothing guarantees that they ...


6

@xuq01's guess is (extremely surprisingly!) wrong. The CBV eta rule described in the question is sound in Standard ML: the value v is contextually equivalent to fn x => v x. There are two caveats to this. First, in specific implementations this equivalence might not be sound: in SML/NJ, you could use Unsafe.cast to detect physical equality of function ...


5

this paper by Yves Bertot, Benjamin Gr´egoire, and Xavier Leroy builds an optimizing compiler for a C-like language based purely on the Coq specification. some of this technology is apparently utilized in the CompCert C compiler. A structured approach to proving compiler optimizations based on dataflow analysis it considers the correctness of two ...


5

If you are a bit more careful about definitions, and in particular recursive definitions, then such confusion cannot arise. In your example, we must first decide whether f(x) = x + 1 is supposed to be a recursive definition or not. This cannot be discovered by looking for recursive calls in the body of the definition. Defining a function by recursion is a ...


4

Functions can be partially applied, so you can end up with a situation in which a function is called with "not enough" arguments. For example, consider the map functional: (* map : ∀α,β. (α → β) → list α → list β *) let rec map f xs = match xs with | [] -> [] | x :: xs -> (f x) :: map f xs This will take a function f as an argument, and ...


4

Adding to shaunc's answer: the first program (idealized over integers rather than "machine" integers) is a linear recurrence, and it turns out there are some very general methods for solving those: http://en.wikipedia.org/wiki/Recurrence_relation#Solving Note that this is similar to a discrete version of differential equations, so things get complicated ...


4

Read the post you are linking to. It's explained there in quite some detail. It's a consequence of the C++ spec, as Neel Krishnaswami explains. The very first sentence of the blog post says "Obviously I’m not serious". That should have been a tip-off right there. The post then goes on to say "What is really going on here..." and explains what's going on....


3

Actually, optimizing compilers do that kind of things. I am for example thinking of the work of Robert Paige at NYU. The problem is of course to identify situations where a given type of transformation may be useful. That require identifying computational structures, and knowing some of the algebraic properties of the data being manipulated. A classical ...


3

How can inherited attributes be simulated with synthesized ones: an example. The way of doing it is to postpone the evaluation of any attribute that uses directly or indirectly an inherited attribute, by abstracting it into a function that takes the inherited attribute as argument. There may be several such arguments. Here is a fragment of a simple example,...


3

I assume you're looking for ways to compute the Control Flow Graph of a given program. This graph depends (obviously) on the actual operational semantics of the language you are interested in, and so cannot be computed from the AST alone, in the sense that some knowledge of the language semantics themselves are needed. For a given language it is possible ...


3

Can I prove certain properties (that are guaranteed to hold) for a program (e.g., a subroutine is non-entrant and can never call itself) that allow to perform optimizations that are not usually possible. It is equivalent to extending the typechecker to provide some properties of a program to the optimizer. I believe Tsuyoshi Ito is right and you may be ...


2

I actually thought about the same question a while ago. Here is the train of thought I had: As you said the halting problem is an issue. To avoid this we need a language which only allows programs that always halt. On the other hand our language needs to be expressive enough to deal with most common problems(e.g. it should at least capture all of the ...


2

Consider the following lazy functional program: doArith :: Int -> Int doArith n = if n < 0 then 1 + 2 else 3 - 4 A compiler can figure out that it doesn't need to build a thunk for 1 + 2 or 3 - 4 in the if expression. This is because that an if expression is strict in the branch position, since either 1 + 2 or 3 - 4 will surely be evaluated after ...


2

This new version of the answer tries to take into account the changes in the question, and the information exchanged in the comments. This answer assumes that $S$ should be the set of variables that have a content that is used in some defined fragment of the program, rather than, at some point in the program, the variables with a content that will be ...


2

A general approach is to automatically infer loop invariants. There are techniques for inferring loop invariants that can be expressed in Presburger arithmetic, i.e., linear expressions over the integers plus quantifiers. These typically rely upon the fact that there exist decision procedures for Presburger arithmetic, e.g., the Omega method (see also the ...


2

SML compilers do perform eta-reduction (at least SML/NJ does), but I expect most functional programming language compilers do, even those for which the eta-law does not always hold. E.g. the pointer equality of OCaml doesn't have a strictly defined semantics, which means that the compiler is free to apply eta-reduction, even though it may change the program'...


2

It is hard to say. The boundary between "syntactic errors" and "static semantic errors" can be really blurred. One appropriate example would be Curry-style (extrinsic typing) and Church-style (intrinsic typing) variants of the same programming language, say System F. Failing to include type annotations in the Church-style variant of the language would be a ...


2

In Knuth Vol II Theorem E on page 494 he presents an algorithm that can evaluate a polynomial using $\frac{n}{2} + 2$ multiplications. The theoretical minimum is $\frac{n}{2}$, assuming generic polynomials. The algorithm requires factoring polynomials. There is another algorithm from Rabin & Winograd that only requires division, but runs in $\frac{n}{2} +...


2

... is not valid since we have "left recursion" (a variable that calls itself). That's not what a left recursion is. That's simply recursion. Direct left recursion is when a rule $A \to A\alpha$ exists for arbitrary $\alpha$. Indirect left recursion exists when there's a rule $A \to^* A\alpha$ for arbitrary $\alpha$. Note the star, implying possibly many ...


Only top voted, non community-wiki answers of a minimum length are eligible