Questions tagged [functional-programming]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
592
votes
6answers
120k views

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

Since Chris Okasaki's 1998 book "Purely functional data structures", I haven't seen too many new exciting purely functional data structures appear; I can name just a few: IntMap (also invented by ...
53
votes
2answers
6k views

What are the outstanding questions in purely functional data structures?

This question is inspired by another question about what's new in PFDS since the publication of Okasaki's book in 1998. I'll start with two questions I have: Is there a purely functional set data ...
46
votes
2answers
6k views

Explaining Applicative functor in categorical terms - monoidal functors

I'd like to understand Applicative in terms of category theory. The documentation for Applicative says that it's a strong lax ...
36
votes
8answers
2k views

Higher-order algorithms

Most of the well-known algorithms are first-order, in the sense that their input and output are "plain" data. Some are second-order in a trivial way, for example sorting, hashtables or the map and ...
29
votes
1answer
1k views

Programming languages with canonical functions

Are there any (functional?) programming languages where all functions have a canonical form? That is, any two functions that return the same values for all set of input is represented in the same way, ...
27
votes
2answers
4k views

Are lambda calculus and combinatory logic the same?

I am currently reading "Lambda-Calculus and Combinators" by Hindley and Seldin. I'm not an expert, but have always taken an interest in lambda calculus because of involvement with functional ...
25
votes
5answers
2k views

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

ACSL (Ansi C Specification Language), is a specification for C code, annotated with special comments, that allows C code to be formally verified. I have not looked into it, but I imagine that the ...
22
votes
2answers
839 views

Can the cost of GC be neglected when analyzing the running time of worst-case data structures specified in a garbage-collected programming language?

I just realized that I have been assuming the answer to my question is "yes" but I don't have a good reason. I imagine that maybe there is a garbage collector that provably introduces only $O(1)$ ...
22
votes
1answer
1k views

What are the practical issues with intersection and union types?

I'm designing a simple statically typed functional programming language as a learning experience. It appears that the type system I have implemented so far could (with a little extra work) ...
19
votes
2answers
3k views

What are the limits of total functional programming?

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 ...
19
votes
3answers
3k views

Reader, Writer monads

Let $C$ be a CCC. Let $(\times)$ be a product bifunctor on $C$. As Cat is CCC, we can curry $(\times)$: $curry (\times) : C \rightarrow(C \Rightarrow C)$ $curry (\times) A = \lambda B. A \times B$ ...
18
votes
4answers
972 views

How are imperative languages more different from each other than functional languages?

I'm reading Simon Peyton Jones's The Implementation of Functional Programming Languages and there's one statement that surprised me a little bit (on page 39): To a much greater extent than is the ...
18
votes
2answers
2k views

What persistent data structure for a set of partially ordered elements?

I need to store sets of elements of type a. Type a is partially ordered, so comparing $a_1$ and $a_2$ can return smaller, greater, equal or incomparable. One problem with hashtables is that two equal ...
17
votes
2answers
3k views

Category theory, computational complexity, and combinatorics connections?

I have been trying to read “Pearls of Functional Algorithm design”, and subsequently “The Algebra of Programming”, and there is an obvious correspondence between recursively (and polynomially) defined ...
16
votes
3answers
2k views

Bootstrapping a Finger Tree Structure

After working with 2-3 finger trees for quite a bit I have been impressed by their speed in most operations. However, the one issue I have run into is the large overhead associated with the initial ...
15
votes
2answers
443 views

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

From a purely abstract math/computational reasoning point of view, (how) could one even discover or reason about problems like 3-SAT, Subset Sum, Traveling Salesman etc.,? Would we be even able to ...
15
votes
1answer
1k views

A mathematical (categorical) description of type classes

A functional language can be viewed as a category where its objects are types and morphisms functions between them. How do type classes fit in this model? I assume we should only consider those ...
15
votes
2answers
3k views

What is a zipper, and how does it relate to a tree-like structure?

I was reading a chapter in LYAH which didn't really make sense to me. I understand that zippers can arbitrarily traverse a tree-like structure, but I need some clarification on it. Also, can zippers ...
14
votes
2answers
1k views

Difference lists in functional programming

The question What's new in purely functional data structures since Okasaki?, and jbapple's epic answer, mentioned using difference lists in functional programming (as opposed to logic programming), ...
14
votes
1answer
2k views

Why do functional programming languages require garbage collection?

What's stopping ghc from translating Haskell into a concatenative programming language such as combinatory logic and then simply using stack allocation for everything? According to Wikipedia, the ...
14
votes
2answers
2k views

Purely Functional Equivalent of B-Tree?

I am exploring the idea of writing a DBMS in purely functional way. The traditional data structure used for indexing is B-Tree. I'd like to know some purely functional equivalent of B-Tree that would ...
14
votes
3answers
604 views

Associative hash mixing

Consider the lowly singly-linked list in a purely functional setting. Its praises have been sung from the mountain tops and will continue to be sung. Here I will address one among its many strengths ...
14
votes
0answers
364 views

Are there simple core languages which are consistent and expressive?

The Calculus of Constructions is a very simple core functional language with dependent types. Per curry-howard isomorphism, it could, potentially, be very useful for writing programs and proofs. It, ...
13
votes
2answers
564 views

Category theory and parsers — references wanted

Since I'm interested in parsers (mainly in parser expression grammars), I'm wondering if there's some work that gives a categorical treatment of parsing. Any reference on applications of category ...
12
votes
2answers
700 views

What are the relations between Alternative, MonadPlus(LeftCatch) and MonadPlus(LeftDistributive)?

Following up What’s an example of a Monad which is an Alternative but not a MonadPlus?: Assume $m$ is a monad. What are the relations betweem $m$ being an Alternative, a MonadPlusCatch and a ...
12
votes
2answers
612 views

Continuation passing transform of binary functions

Recall the continuation passing transform (CPS transform) which takes $A$ to $\beta A \mathrel{{:}{=}} R^{R^A}$ (where $R$ is fixed) and $f : A \to B$ to $\beta f : \beta A \to \beta B$ defined by $$\...
12
votes
2answers
656 views

Simple balanced trees with O(1) concat?

In Purely Functional Worst Case Constant Time Catenable Sorted Lists, Brodal et al. present purely functional balanced trees with O(1) concatenate and O(lg n) insert, delete, and find. The data ...
12
votes
1answer
308 views

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

I've recently attempted to implement Aaron's Cedille-Core, a minimalist programming language capable of proving mathematical theorems about its own terms. I've also proven induction for λ-encoded ...
11
votes
1answer
537 views

What exactly does “semantically observable” side-effect mean?

I have question regarding pure functions. According to the Wikipedia page one of the requisites for a pure function is : Evaluation of the result does not cause any semantically observable side ...
10
votes
2answers
1k views

How do I choose a functional dictionary data structure?

I've read a bit about the following data structures: Bagwell's Ideal Hash Tries Larson's Dynamic hash tables Red-Black trees Patricia trees ...and I'm sure there are a lot of others out there. I've ...
10
votes
3answers
474 views

Which algorithms can be expressed using a total functional language with data parallel operators?

Imagine a functional programming language whose only data types are numerical scalars and arbitrary nestings of arrays. The language lacks any means of unbounded iteration, so the following are ...
10
votes
1answer
798 views

Algorithm to determine function equality on the simply typed lambda calculus?

We know that beta-equality of simply typed lambda-terms is decidable. Given M,N:σ→τ, is it decidable whether for all X:σ, MX $≃_β$ NX?
10
votes
1answer
755 views

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

Interaction combinators have been proposed as a compile target for the λ-calculus before. That paper implements the full λ-calculus. It is also known that it is possible to optimize interaction-net ...
10
votes
1answer
516 views

What are the theoretical limits of the Stratego Programming Language?

Stratego is a programming transformation language/Rewriting DSL. Anthony Sloane has done some work doing an implementation that runs on Scala. What are the theoretical limits of Stratego as a ...
10
votes
1answer
237 views

Type systems preventing laziness-related memory leaks?

Perhaps the main source of performance problems in Haskell is when a program inadvertently builds up a thunk of unbounded depth - this causes both a memory leak and a potential stack overflow when ...
9
votes
3answers
1k views

How to make the Lambda Calculus strong normalizing without a type system?

Is there any system similar to the lambda calculus that is strong normalizing, without the need to add a type system on top of it?
9
votes
8answers
6k views

What are the simplest turing-complete systems? [closed]

Lambda Calculus is very simple. Are there even simpler turing-complete systems? Which is the simplest of them all?
9
votes
4answers
904 views

Explaining monad transformers in categorical terms

Most resource regarding categorical notions in programming describe monads, but I've never seen a categorical description of monad transformers. How could monad transformers be described in the terms ...
9
votes
3answers
630 views

Is the class of primitive recursion functionals equivalent to the class of functions which Foetus proves to terminate?

Foetus, if you have not heard of it, can be read up on here. It uses a system of 'call matrices' and 'call graphs' to find all 'recursion behaviors' of recursive calls in a function. To show that a ...
9
votes
1answer
474 views

What are possible implementations of Haskell's type classes and what are their (dis)advantages?

As far as I know, a Haskell function with type classes constraints is internally compiled to a function with additional arguments that receive dictionaries with the necessary implementations of each ...
8
votes
2answers
263 views

Resumption-based IO systems?

I've been playing around with resumptions lately, mostly from Abramsky's classic paper Retracing Some Paths in Process Algebra. They are quite slick (basically solutions to the domain equation $R = I \...
8
votes
1answer
159 views

Type for “ways values can be different”

I am looking for a concept in type theory that I am sure has probably been explored, but do not know the name behind. Let's consider a ML-like language with product and sum types and a Hindley-Milner ...
8
votes
1answer
378 views

Functional Sparse-Matrix with good performance?

While writing a Petri Net program, I was faced with a choice about data structures to represent the graph. Adjacency lists (i.e. lists enumerating the arcs into and out of individual places or ...
8
votes
0answers
418 views

Complete combinator basis for System F-omega

The S and K combinators form a complete (and Turing complete) basis when untyped. Within the Hindley-Milner type-system, and I believe within system $F$ as well, S and K can encode any well-typed ...
7
votes
3answers
1k views

What are the relationships between Functional Reactive Programming, Automatic Differentiation, Self-Adjusting Computation and Partial Evaluation?

Self-adjusting computation seems to be related to all of the other topics, but I would like to get a clearer sense of how they all relate. For example, do any of them subsume or obsolete any of the ...
7
votes
2answers
1k views

What is higher-order in higher-order abstract syntax?

I understand that using higher-order abstract syntax essentially means using host (meta) language abstraction facilities to represent binders in embedded (object) language. But, Why exactly is it ...
7
votes
2answers
815 views

Free theorems, where?

I've found this webapp which lets you generate a free theorem for a given type. The generated theorems quantify over types and relations on these types. These theorems (formulas) are theorems of which ...
7
votes
2answers
859 views

What logic correponds via Curry-Howard to a Monad?

According to Moggi's 1991 paper "Notions of computation and monads" one can represent monadic equational logic with the well known monad $(T, \eta, \mu)$ with T an functor and the two natural ...
7
votes
3answers
333 views

Can Non-termination be considered an algebraic effect?

Non-termination is sometimes considered an effect. I have been reading about algebraic effect systems (What is algebraic about algebraic effects and handlers?), and I suspect non-termination (like ...
7
votes
3answers
352 views

When a type is a value?

In functional programming and in the theoretical setting of the $\lambda$-calculus it is standard to consider a lambda abstraction $\lambda x.M$ as a value. In my understanding, the intuitive reason ...