Functional programming is a programming paradigm which primarily uses functions as means for building abstractions and expressing computations that comprise a computer program.

learn more… | top users | synonyms

0
votes
1answer
50 views

Can we prove mathematical induction statements in Lisp?

My previous question Can we prove that $1 + 2 + \dots + n = \frac{n(n+1)}{2}$ using a computer program? has a problem that it tries to cover too much ground. Here is a related question motivated by ...
2
votes
2answers
92 views

Can we prove that $1 + 2 + \dots + n = \frac{n(n+1)}{2}$ using a computer program?

Chapter 7 of The Haskell Road to Logic Math and Programming discusses induction and recursion. Haskell is strongly typed and we can define the natural numbers ...
3
votes
2answers
20 views

Is there a formal term for functions that have static state across executions?

Two examples, one in PHP: function adder($i){ static $a = 0; $a += $i; return $a; } A similar effect can be achieved with closures in javascript: ...
4
votes
0answers
82 views

Does this data structure already exist, and is there a better alternative?

Consider a polymorphic Haskell function type, like the type for .: (a -> b) -> (b -> c) -> a -> c This type ...
4
votes
3answers
50 views

Is there any meaning behind the classification of “λ-terms” in classes such as “church number” and “church list”?

λ-calculus terms can be informally/intuitively categorized, such as: (λ f x . (f (f (f x))))) is a church natural (3) ...
0
votes
1answer
72 views

Why are functional programs considered slower than procedural counterparts asymptotically, if the opposite appears true?

I've read and been told way too many times that functional algorithms and data structures have an obligatory O(log(N)) slowdown in respect to their procedural ...
6
votes
2answers
134 views

Eliminate non-local references from closure

For a code similarity detection framework I need to eliminate references to non-local variables, for example having the following closure: ...
7
votes
1answer
78 views

Are combinatory logic terms always larger?

So there is an algorithm to convert lambda calculus terms to combinatory logic using SK combinators. It produces things that explode in size. I would like to know more about this explosion in size. I ...
6
votes
0answers
17 views

Is there any type system which can assign a type to any halting lambda calculus term? [duplicate]

Some lambda terms, such as the church number 3: (f x -> (f (f (f x)))), are easily typeable on the simply typed lambda calculus. Others, such as ...
2
votes
1answer
85 views

Do functional algorithms require more memory than imperative algorithms? [closed]

Let's suppose we are counting words in string. We split it so what we have is an array of strings. I'll use Python as an example. The imperative approach would as follows: ...
1
vote
1answer
97 views

Intuition behind F-algebra

I looked at here for getting an intuition about F-algebra, but I am still left with some questions. Suppose I have a group signature as $\Sigma= (* : X \times X \rightarrow X, \thicksim: X ...
2
votes
2answers
30 views

Occurrences notation in “Compiling Pattern Matching to Good Decision Trees”

From Compiling Pattern Matching to Good Decision Trees (Luc Maranget, Proceedings of ML '08, pp. 35–46. ACM, 2008.) We also consider the usual occurrences. Occurrences are ...
1
vote
2answers
51 views

Curry Howard correspondence and Church-Turing thesis

Curry-Howard correspondence states the equivalence between logic/deduction and types/programs. The Church-Turing thesis states the equivalence of some models of computation. Specifically, all ...
0
votes
0answers
18 views

Proxy for lazy evaluation?

Can lazy evaluation be substituted in an eagerly evaluated language by the following setup?... Higher-order functions. Generalized left associativity. Infinite structures like ...
2
votes
1answer
27 views

What additional expressivity does polyvariance give in pushdown CFA?

I'm reading through Pushdown Control-Flow Analysis of Higher-Order Programs, which presents a synthesis of the Abstracting Abstract Machines technique and pushdown automata to get static analysis ...
2
votes
1answer
42 views

What is the difference between the Mogensen-Scott and the Boehm-Berarducci encoding for ADTs on the Lambda Calculus?

On the Lambda Calculus, there are several different ways to represent a list. For example, one can encode it as its right fold: ...
2
votes
1answer
52 views

Guessing the structure of a finger tree from the number of elements

I'm writing a data structure library, and I want to write an efficient algorithm for adding many elements to a finger tree (from an iterable sequence). I'm going to do this by constructing a finger ...
0
votes
1answer
49 views

Suggestions for Short Examples Contrasting Functional Programming Languages [closed]

A fellow student and I are writing a paper on functional programming for a programming languages course, part of which will be comparing and contrasting Lisp (Scheme), ML (SML), and Haskell. We'll be ...
1
vote
1answer
86 views

Difference between normal-order and applicative-order evaluation

The language I'm learning is Scheme and I'm working on an exercise that gives this: ...
1
vote
1answer
40 views

Definition of opposite category

From page 29 of The algebra of programming : For any category C the opposite category $C^{op}$ is defined to have the same objects and arrows as C, but the source and target operators are ...
0
votes
1answer
24 views

Something wrong with this definition of factorial with structural recursion? [closed]

In The Algebra of Programming page 5, the authors defined structural recursion foldn (c, h) over natural numbers: ...
3
votes
2answers
70 views

Formal Verification of Functional Programs

So I've been interested in learning more about formal verification, and I've seen a lot of interesting things like ACSL and JML which are based on the concept of Hoare triples. My question is, that ...
5
votes
4answers
84 views

Reviews of work in the field of partial evaluation (post 1993)

I'm looking for relatively new reviews of research work on partial evaluation. The most recent work I've found is "Tutorial notes on partial evaluation" by Charles Consel and Olivier Danvy (1993). The ...
3
votes
3answers
464 views

Does immutability in functional programming really exist?

Although I work as a programmer in my daily life and use all the trendy languages (Python, Java, C, etc) I still have no clear view of what functional programming is. From what I've read, one property ...
4
votes
1answer
54 views

Using SMT solvers to generate random solutions to given predicate

I am interested in generating random solutions to predicates. I only need SMT for integers with the following predicates/functions <, >, <=, >=, ==, !=, +, * The algorithm I want should produce ...
1
vote
1answer
45 views

Substitution-based Operational Semantics of algebraic datatypes

Assume, I want to define the operational semantics for some subset of ML. ...
2
votes
2answers
58 views

Second order function formalization

I need to work on a optimizer for a language whose operator are second order functions. They are the well known ones filter, map, reduce, fold, foreach etc. etc. I need to formalize as much as ...
1
vote
2answers
67 views

Is it possible to write an HTML compiler with no mutable state?

That's probably a vague question but allow me to try and give an example: My compiler does transformations on HTML (from HTML to HTML). It scans a flattened DOM tree, and relies on lookbehinds (on ...
-2
votes
1answer
104 views

Logic and Functional programming [closed]

I have a subject Introduction to logic and functional programming but the course is not provided in detail. This is the provided course. Introduction to declarative programming paradigms. The ...
1
vote
0answers
43 views

How to get from factorial to a y-combinator?

In one of his conference talks Jim Weirich derives the applicative form of the y-combinator by refactoring a partial definition of factorial. The starting point in his talk is different than what ...
0
votes
0answers
28 views

Are if statements avoidable is we define a program according to explicit state transitions? [duplicate]

This question occurred to me some time ago when I was thinking about whether or not if statements are fundamental in computation. Consider a program that manages a ...
4
votes
1answer
134 views

How is IO a monad?

I am learning the Haskell programming language. From what I am reading, Input/Ouput (IO) raises challenges for Haskell's purity, since by definition we are interacting with the outside world. From ...
5
votes
2answers
120 views

Which fixpoint is Haskell list type?

Let's say that lists are defined as List a = Nil | Cons a (List a) Then, in Haskell is List x the greatest or least fixpoint? ...
1
vote
0answers
23 views

How to reduce this with all 4 of normal applicative by-name by-value?

Given mult = \x -> \y -> x*y I am trying to reduce (mult (1+2)) (2+3) with each of the strategies: normal-order ...
1
vote
0answers
27 views

Algorithm for the function “drop” in a binary random-access list

In the book Purely Functional Data Structures by Okasaki, exercise 9.1 asks: Write a function drop of type ...
15
votes
2answers
496 views

Is computation expression the same as monad?

I'm still learning functional programming (with f#) and I recently started reading about computation expressions. I still don't fully understand the concept and one thing that keeps me unsure when ...
5
votes
0answers
50 views

Bounded existential polymorphism

In Pierce's "Types and Programing Languages" he, at the very end, presents the most powerful system in the book: $F^{\omega}_{<:}$. He, however, does not explain how bounded existential ...
1
vote
2answers
78 views

Call‑by‑name will succeeds where call‑by‑value may fails: some example cases?

I've landed to SML pages, comparing call‑by‑name and call‑by‑value, asserting the former always succeed while the latter may fails. As this seems counter intuitive to me, I feel at least an example ...
2
votes
1answer
136 views

Call by need compared to pass by function

SML uses pass‑by‑value, Haskell uses call‑by‑need. Unless I'm wrong (the purpose of this question), one can do call‑by‑need with SML, passing a function instead of a value; a function to be later ...
1
vote
2answers
161 views

Haskell monad bind operator type

In Haskell, the Monads type class has the bind operator, which is represented by the symbol >>= The type of such operator is: ...
3
votes
1answer
26 views

Lower complexity bounds without mutation

Lower complexity bounds tend to be a very hard problem in general. Despite this, I was wondering if there are any theoretical results that relate lower complexity bounds for some class of problems in ...
6
votes
2answers
811 views

Array-like immutable (persistent) data structure implementation with fast indexing, append, prepend, iteration

I'm looking for a persistent data structure similar to array (but immutable), allowing for fast indexing, append, prepend, and iteration (good locality) operations. Clojure provides persistent ...
2
votes
0answers
44 views

Defunctionalization and known arity function calls by pointer

Defunctionalization is nice for higher order functions where it is completely necessary to avoid runtime support, but in some cases it's favourable to use function pointers instead (since they don't ...
3
votes
0answers
112 views

Is there any programming system that enables reversible computations?

Better explained with examples, I need a programming system with the following characteristics: ...
2
votes
0answers
20 views

How does supercompilers relate to macro tree transducers?

Supercompilers can be used as a generalisation of deforestation of a functional program. Macro Tree Transducers composition can be used to the same effect, using a completely different approach. What ...
4
votes
1answer
161 views

Why are dependently typed languages such as Agda used for proofs, if supercompilers for simpler typed languages can do the same?

Proof assistants such as Agda can be used to assert properties about programs, such as "the double of a number is even". Interestingly, supercompilers can be used for the same purpose, creating ...
7
votes
2answers
182 views

Is there a canonical definition of “pure” function?

StackOverflow pointed me here, so the question might be a bit in a layman's terms. Wikipedia defines pure functions as In computer programming, a function may be described as a pure function if ...
4
votes
1answer
42 views

Is dependency analysis required in order to type a program?

I have seen stated in various places that in order to allow an "increase in polymorphism," functional dependency analysis should be performed, and type inference should be used for every declaration ...
-1
votes
2answers
155 views

Mathematical function vs Computer program

In mathematics , an $n$-ary relation is subset of cross product on $n$ sets took under consideration. Let us take $A_1,A_2,A_3 \cdots A_n$ be the n sets. Then relation $R \subseteq A_1\times ...
5
votes
1answer
57 views

What progress has been made on persistent catenable deques in the last decade?

I'm interested in persistent catenable deques: deques that can be concatenated. Kaplan and Tarjan came up with the first such data structure in 1995; Okasaki came up with a simpler, amortized version ...