26

Here are a few things to keep in mind: Although we generally think we know what we mean by set-theoretic intersection and union, there have been several different takes on what exactly intersection and union types are. So, it's worth pinning this down before you embark on an implementation. One element which I think is awfully important for understanding ...


22

I can think of a few possible answers coming from linear logic. The simplest one is the affine lambda-calculus: consider only lambda-terms in which every variable appears at most once. This condition is preserved by reduction and it is immediate to see that the size of affine terms strictly decreases with each reduction step. Therefore, the untyped affine ...


19

All of the following comments are premised on the choice of a standard implementation strategy using closures to represent function values and a call-by-value evaluation order: For the pure lambda calculus, garbage collection is not necessary. This is because it is not possible to form cycles in the heap: every newly-allocated value can only contain ...


17

It's common to say that $f$ and $g$ commute with respect to composition (where the property is known as commutativity). See, e.g., http://en.wikipedia.org/wiki/Function_composition.


16

What are the limitations of total functional programming? It is not Turing-complete, but still supports a large subset of the possible programs. Are there important constructs that you could write in a Turing-complete language, but not in a total functional language? Assuming your functional language $L$ lets you encode arithmetic operations, there is one ...


16

It depends on the total functional language. This answer sounds like a cop-out, but nothing more specific can be said. After all, consider whatever important decidable program that you're interested in. Write a program in your favorite Turing-complete language to solve it. Since the problem is decidable, your program will halt on all inputs. (Arguably, a ...


16

You may wish to look at cost semantics for functional languages. These are various computational complexity measures for functional languages that do not pass through any kind of Turing machine, RAM machine, etc. A good place to start looking is this Lambda the Ultimate post, which has some good further references. Section 7.4 of Bob Harper's Practical ...


15

You might want to check out Liquid Haskell, which allow working with type refinements rather than dependent types. Type refinements can be seen as a restricted logical language that allow you to express Hoare-style properties of the inhabitants of various datatypes. Another possible candidate is the $F^*$ language, which offers similar constructs. There ...


14

A zipper, in general, is a data structure with a hole in it. Zippers are used for traversing/manipulating data structures, and the hole corresponds to the current focus of the traversal. Typically there is also an element of the data structure under consideration, so that one has a (list) zipper and a list or a (tree) zipper and a tree. The zipper allows the ...


14

The formulas are formulas of Abadi-Plotkin logic, which they describe in their paper A Logic for Parametric Polymorphism. The semantics of System F that Abadi and Plotkin used to interpret their logic can be found in Bainbridge, Freyd, Scedrov, Scott's paper Functorial Polymorphism.


14

At the request of Andrej and PhD, I am turning my comment into an answer, with apologies for self-advertising. I recently wrote a paper in which I look at how to prove the Cook-Levin theorem ($\mathsf{NP}$-completeness of SAT) using a functional language (a variant of the λ-calculus) instead of Turing machines. A summary: the key notion is that of affine ...


13

You can think of $\lambda$-abstraction as an operator $\Lambda$ which takes a function from terms to terms into a term: $$\Lambda : (\mathsf{Term} \to \mathsf{Term}) \to \mathsf{Term}.$$ The type of $\Lambda$ is higher-order because it maps functions to objects, so it is a functional of rank 2. This is where the name comes from. For example, if $\mathsf{id}$...


13

As I said in my comment, the answer in general is no. The important point to understand (I say this for Viclib, who seems to be learning about these things) is that having a programming language/set of machines in which all programs/computations terminate by no means implies that function equality (i.e., whether two programs/machines compute the same ...


13

Honda and Yoshida's A Compositional Program Logic for Polymorphic Higher-Order Functions (probably) pioneered Hoare logics for purely functional languages. This work is based on Hennessy-Milner logic and Milner's encoding of functions into processes, as described here: From Process Logic to Program Logic The work by Régis-Gianas et al mentioned in ...


12

Is it possible to make a "smart" trampoline function that takes two forms of a function, a trampolined version and a non-trampolined version, and chooses (or predicts) the most efficient strategy?* Yes, it's possible to do things like this, but if you control the compiler, it's usually faster and easier to do something else. The main exception is when you ...


12

The original paper by Church and Rosser, "Some Properties of Conversion," describes something that may be an example of what you're looking for. If you use the strict lambda calculus, where in every occurrence of $\lambda x.M$ you have that $x$ appears free in $M$, then without a type system the following property holds (it's Theorem 2 in Church and Rosser'...


11

A semantics of a program is a model of its behavior which, like any scientific model, ignores aspects that you don't want to study. An extremely detailed model of the execution of a program would model the physical behavior of the computer that executes it, including the execution time, power consumption, electromagnetic radiation, etc. Such aspects are ...


11

See also Yann Régis-Gianas PhD thesis work with François Pottier: A Hoare Logic for Call-by-Value Functional Programs (MPC'08). This work was extended to cover the usual ML side-effects by Johannes Kanig and Jean-Cristophe Filliatre in 2009: Who: A Verifier for Effectful Higher-order Programs.


10

Here's a fun one, by Neil Jones and Nina Bohr: Call-by-value Termination in the Untyped $\lambda$-calculus It shows how to apply the size-change analysis (a type of control flow analysis that detects infinite loops) on untyped $\lambda$-terms. This is quite nice in practice, but of course is restricted to $\lambda$-terms without defined constants (though ...


10

You're quite right that the "queue = two lists" approaches don't give you the running time you want when you have the ability to re-use earlier versions. To get O(1) running time (amortized or worst case), you need a way to reverse the rear list and append it to the front list incrementally. Instead of doing the reverse&append all at once, taking O(N) ...


10

The two papers to look at it are Benton, Bierman and de Paiva's Computational Types from a Logical Perspective, which directly gives a proof theory for Moggi's computational lambda-calculus; and Rowan Davies and Frank Pfenning's A Judgmental Reconstruction of Modal Logic, which gives a constructive proof theory for S4 modal logic with box and diamond, and ...


9

MonadPlusDist $\rightarrow$ Alternative is true. Corollary: Alternative $\rightarrow$ MonadPlusCatch is false (because as Petr Pudlák pointed out, [] is a counterexample - it doesn't satisfy MonadPlusCatch but does satisfy MonadPlusDist, hence Applicative) Assumed: MonadPlusDist Laws -- (mplus,mzero) is a monoid mzero >>= k = mzero` ...


9

One of the very first applications of category theory to a subject outside of algebraic geometry was to parsing! The keywords you want to guide your search are "Lambek calculus" and "categorial grammar". In modern terms, Joachim Lambek invented noncommutative linear logic in order to model sentence structure. The basic idea is that you can give basic parts ...


9

It's not entirely clear what do you mean by a functional programming language without closures. Can you give an example? Functional programming languages are usually based on lambda calculus, whose essential part is that you can have open lambda terms. For example the term for the constant function (the K-combinator) $\lambda x . \lambda y . x$ can be ...


9

I think that the type system you want is elementary affine logic with fixpoints. A distinctive feature (actually, the distinctive feature) of light logics, including elementary linear/affine logic, is that types do not ensure termination: unlike usual logical system, cut-elimination follows from a structural property of proofs (namely, stratification), the ...


9

For question 1, the answer is no, and is no for almost any type discipline (except certain intersection types): the fact that a term is (strongly or weakly) normalizable does not imply in general that it is typable. Typability implies termination, not the other way around. The specific case of of $\lambda EA$, however, brings up another issue which may be ...


9

I think you are looking for a typed variant of anti-unification. Anti-unification can be described as follows. First, suppose that we have a grammar of terms as follows: t ::= () | (t, t) | C t | X Here, () and (t, t) denote units and pairs, C t is a term with a leading constructor, and X is a term variable, which could be substituted for any term. The ...


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

According to Oleksandr Manzuk, they are "translation of a monad along an adjunction", see "Calculating Monad Transformers with Category Theory". By the way, that's the third hit on Google for "monad transformer categorically". The first is a Stackoverflow question about this and the second is your question.


8

There is a paper in this year's ICFP, refinement types for Haskell. The paper deals with termination checking rather than full Hoare logic, but hopefully that's a start in this direction. The related work section in that paper contains some pointers, such as Xu, Peyton-Jones, and Claessen's static contract checking for Haskell, and Sonnex, Drossopoulou, and ...


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