21 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 ...
Neel Krishnaswami's user avatar
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 ...
Andrej Bauer's user avatar
  • 28.8k
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 ($\...
Damiano Mazza's user avatar
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 ...
Neel Krishnaswami's user avatar
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 ...
Chris Okasaki's user avatar
9 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/...
Mike Rainey's user avatar
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, ...
Damiano Mazza's user avatar
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: ...
Neel Krishnaswami's user avatar
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 ...
Damiano Mazza's user avatar
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, ...
Neel Krishnaswami's user avatar
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. ...
Neel Krishnaswami's user avatar
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 ...
Andrej Bauer's user avatar
  • 28.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: ...
András Kovács's user avatar
7 votes
Accepted

Composition with recursion in functions between types

(I'm going to try to write an answer for functional programmers, with Haskell-like code.) First, you should know that using higher-order functions, recursive definitions can be turned into fixed-point ...
Lê Thành Dũng Nguyễn's user avatar
6 votes

When a type is a value?

I will offer a semantic perspective. The relationship between values and general computations may be expressed in terms of an adjunction between two categories: \begin{align*} F &: \mathcal{V} \to ...
Andrej Bauer's user avatar
  • 28.8k
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 ...
Damiano Mazza's user avatar
5 votes
Accepted

Stream fusion in total functional language

If all you have are are plain inductive and coinductive types, fusion is impossible, for the reason you point out. However, it is possible if your type system supports sized types. These types let ...
Neel Krishnaswami's user avatar
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-...
Rodolphe Lepigre's user avatar
5 votes

What logic correponds via Curry-Howard to a Monad?

I'll add this in addition to Neel Krishnaswami's answer. The article he refers to A Judgemental Reconstruction of Modal Logic cites the article by Satoshi Kobayashi Monad As Modality which I had come ...
Henry Story's user avatar
5 votes

What category are Tagless Final Algebras final In?

Final Algebra semantics was introduced by Mitch Wand in his paper "Final Algebra Semantics and Data Type Extensions", see this freely available tech report: https://www.cs.indiana.edu/ftp/techreports/...
Max New's user avatar
  • 1,675
5 votes
Accepted

Is there a high level (functional) language compiling to Mixed Integer Linear Programming problems?

Here are the systems/languages I know of for representing these kinds of problems at a higher level of abstraction: The Z3 solver has higher-level constructs for words (fixed-length bit-strings), ...
D.W.'s user avatar
  • 12k
4 votes
Accepted

Is the topsort from "Structuring Depth-First Search Algorithms" guaranteed to be (reverse) stable?

Stripping the Haskell encryption from your question (and ignoring why you are using dff instead of dfs to get a search that respects a given order), you appear to be asking about the stability of the ...
David Eppstein's user avatar
4 votes

Fixed set of type constructors to simulate all intensional inductive families?

I am not 100% sure this is what you want, but assuming you are looking for a type theory with a closed set of type constructors, which can model inductive families, then what you want are indexed ...
Neel Krishnaswami's user avatar
4 votes

Encapsulation of OOP and referential transparency of functional programming

It is true that encapsulation in OO is typically used to hide private mutable state. However, this is a property of traditional OOP, which was an evolution of procedural programming. It is not a ...
Andreas Rossberg's user avatar
3 votes

When a type is a value?

In rewriting theory, there are a number of useful definitions of what counts as a value. Here is one which seems quite useful: A term $t$ in normal form is a value if it is not neutral. A term $t$ is ...
cody's user avatar
  • 13.8k
3 votes

When a type is a value?

My impression is that most researchers in dependent type theory speak of normal forms instead of values to avoid ambiguity. There are many ways to precisely define evaluation: beta normal form, eta-...
user833970's user avatar
3 votes

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

Sounds like you are asking for a functional queue. The standard implementation of that is: ...
Andreas Rossberg's user avatar
3 votes

Is it possible to unambiguously read back λ terms from interaction nets without node types?

So, yes, turns out it is possible, as can be seen on the decode function of my abstract algorithm implementation here. Basically, Lambda and Apply nodes are given ...
MaiaVictor's user avatar
  • 3,137
3 votes

Is there a purely functional vector with O(1) access to the front and back but O(log n) concatenation?

You can achieve the exact characteristics you're looking for with Finger Trees. The most basic finger tree is defined in terms of 2-3 tree nodes: ...
Glenn Tang's user avatar
3 votes

A few questions about ISWIM

I was around when ISWIM was being formulated, including an implementation project on the Univac 1107 in the mid 1960s. It never struck me that there were no anonymous functions. But functions were ...
orcmid's user avatar
  • 161

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