20 votes

Why do functional programming languages require garbage collection?

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 ...
16 votes
Accepted

(How) Could we discover/analyze NP problems in the absence of the Turing model of computation?

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 ...
  • 26.8k
15 votes

Are there any annotated formal verification systems for pure functional programming languages?

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 ...
  • 13.3k
14 votes

(How) Could we discover/analyze NP problems in the absence of the Turing model of computation?

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 ($\...
13 votes
Accepted

Are there any annotated formal verification systems for pure functional programming languages?

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 ...
13 votes
Accepted

What logic correponds via Curry-Howard to a Monad?

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 ...
11 votes

Are there any annotated formal verification systems for pure functional programming languages?

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 ...
  • 1,910
11 votes

Purely(ish) functional data structure with fast append and forward iteration

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 ...
9 votes
Accepted

Category theory and parsers --- references wanted

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 ...
9 votes
Accepted

What type system fits the subclass of λ-terms that can be reduced optimally?

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, ...
9 votes

How to implement a functional programming language efficiently?

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 ...
  • 2,481
9 votes
Accepted

Explaining monad transformers in categorical terms

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 ...
  • 26.8k
9 votes
Accepted

Can you assign a type to any term of the λEA-calculus?

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 ...
9 votes
Accepted

Type for "ways values can be different"

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: ...
8 votes

Are there any annotated formal verification systems for pure functional programming languages?

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 ...
  • 2,637
8 votes

Can programming help one understand constructive mathematics?

Agda is a dependently typed programming language and/or proof assistant for Martin-Löf type theory. Programming in Agda feels very much like programming in Haskell. For example, inductive proofs are ...
  • 231
8 votes

Programming language supporting infinitary rewriting of regular term graphs?

Yes, Prolog. The specification of unification in the Prolog standard omits the occurs check, and as a result when this spec is properly implemented variables range over rational trees. Additionally, ...
7 votes

Is there a pair of different lambda terms in the normal form that behave identically when applied to any input?

The result you are looking for is Böhm's theorem. The equivalence described by "behaves the same way on all inputs" is the same as the equivalence given by normal forms, but only if you treat eta-...
7 votes

Explaining monad transformers in categorical terms

Augmenting Andrej's answer: There is still no widespread agreement on the appropriate interface monad transformers should support in the functional programming context. Haskell's MTL is the de-facto ...
  • 2,637
7 votes

What's new in purely functional data structures since Okasaki?

Following up on the 2012 paper linked above, the work on RRB vectors has since been extended and published in ICFP'15. RRB vector: a practical general purpose immutable sequence http://dl.acm.org/...
7 votes
Accepted

Can all structurally recursive functions be written without explicit recursion using a catamorphism/fold?

Your function is completely structurally recursive on n, so it is pretty much just a change of notation to make it a catamorphism on the natural numbers. ...
7 votes

Can Non-termination be considered an algebraic effect?

Non-termination can be considered an algebraic effect up to a point. It's an exception that cannot be handled. More precisely, we may introduce a nullary operation (constant) $\bot$ which signifies ...
  • 26.8k
7 votes
Accepted

Structural equality of Pi Types with heterogeneous equality?

I am not aware that J or K exists for heterogeneous equality. It does not need an elimination principle, because it can be simply defined as a sigma type: ...
6 votes

Category theory, computational complexity, and combinatorics connections?

Joyal's Combinatorial Species, Sedgwick/Falojet's "admissible constructions" of Analytic Combinatorics, and Yorgey's Haskell Species are all good. Power Series Power Serious by McIlroy of UNIX diff ...
6 votes
Accepted

How do you encode Lamping's abstract algorithm using interaction combinators?

I am not aware of any implementation of Lamping's algorithm directly in the interaction combinators. I do know that the presence of integer labels is a necessary feature of Lamping's algorithm, even ...
6 votes

Phonology and lambda calculus

This is just a long comment (too many words to fit in a comment box). Gérard Huet is, among other things, an expert in $\lambda$-calculus who worked worked a lot on the computational processing of ...
5 votes
Accepted

Typechecking liveness properties of coprograms

To expand on pedagand's answer: productivity is the term used for the computational dual (in some precise sense) of termination. Formally, a program f : CoData is ...
  • 13.3k
5 votes

Category theory and parsers --- references wanted

It would appear that (context free) parsing a la Parsec is naturally expressed in terms of the Applicative type class. In turn, this class is described well by so-called strong lax monoidal functors, ...
  • 13.3k
5 votes
Accepted

Can we design our own `if` clause in Normal Order evaluation

To answer your question we need some machinery and concepts from the theory of programming languages, so that we can actually make your question well posed, and then answer it. You are asking whether ...
  • 26.8k
5 votes

What makes a language (and its type-system) capable of proving theorems about its own terms?

[Self-advertising follows, but I think that this is relevant.] There are several possible approaches to this questions. One of the ways (that I explored during my PhD thesis in the context of an ML-...

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