Questions tagged [functional-programming]

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

Filter by
Sorted by
Tagged with
19
votes
1answer
2k views

What classes of data structures can be made persistent?

Persistent data structures are immutable data structures. Operations on them return a new "copy" of the data structure, but altered by the operation; the old data structure remains unchanged though. ...
123
votes
7answers
30k views

Is Category Theory useful for learning functional programming?

I'm learning Haskell and I'm fascinated by the language. However I have no serious math or CS background. But I am an experienced software programmer. I want to learn category theory so I can become ...
19
votes
3answers
2k views

ML function of type 'a -> 'b

Our professor asked us to think of a function in OCaml that has the type 'a -> 'b i.e. a function of one argument that could be anything, and that can return ...
22
votes
2answers
1k views

What is meant by Category theory doesn't yet know how to deal with higher-order functions?

In reading Uday Reddy's answer to What is the relation between functors in SML and Category theory? Uday states Category theory doesn't yet know how to deal with higher-order functions. Some day, ...
13
votes
2answers
1k views

Is there a theory/abstraction behind OOP?

Functional programming has the very elegant Lambda Calculus and its variants as a backup theory. Is there such a thing for OOP? What is an abstraction for the object oriented model?
11
votes
2answers
3k 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 Vector,...
8
votes
2answers
572 views

What is the Curry-Howard analogue for linear logics?

As defined by Wikipedia, (The Curry-Howard correspondence) is a generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the ...
8
votes
3answers
375 views

ML functions from polymorphic lists to polymorphic lists

I'm learning programming in ML (OCaml), and earlier I asked about ML functions of type 'a -> 'b. Now I've been experimenting a bit with functions of type ...
8
votes
2answers
381 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 ...
3
votes
1answer
429 views

Does a Haskell program count as an inductive proof?

Is the following statement from [1] true? "Since recursion is the main computational technique, a terminating pure Haskell program counts as an inductive proof of a theorem." My intuition is that ...
5
votes
2answers
250 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 ...
2
votes
1answer
361 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: ...
60
votes
3answers
10k views

Dependent types vs refinement types

Could somebody explain the difference between dependent types and refinement types? As I understand it, a refinement type contains all values of a type fulfilling a predicate. Is there a feature of ...
30
votes
2answers
8k views

How do Functional Reactive Programming and the Actor model relate to each other?

FRP is about streaming events and behaviours through pure functions. The Actor model - at least, as implemented in Akka - is about streaming immutable messages (which can be considered to be discrete ...
38
votes
3answers
4k views

How is algorithm complexity modeled for functional languages?

Algorithm complexity is designed to be independent of lower level details but it is based on an imperative model, e.g. array access and modifying a node in a tree take O(1) time. This is not the case ...
16
votes
3answers
579 views

Studying Programming Language Theory

I have recently become extremely interested in understanding and proving aspects of (functional) programming languages. However as I dive deeper in, things like $\lambda$ calculus, category theory, ...
25
votes
3answers
3k views

What is the relation between functors in SML and Category theory?

Along the same thinking as this statement by Andrej Bauer in this answer The Haskell community has developed a number of techniques inspired by category theory, of which monads are best known but ...
19
votes
4answers
966 views

Why is it important for functions to be anonymous in lambda calculus?

I was watching the lecture by Jim Weirich, titled 'Adventures in Functional Programming'. In this lecture, he introduces the concept of Y-combinators, which essentially finds the fixed point for ...
22
votes
4answers
4k views

Why do we use persistent data structures in functional programming?

Functional programming employs persistent data structures and immutable objects. My question is why is it crucial to have such data structures here? I want to understand at a low level what would ...
8
votes
2answers
1k views

Isn't Functional Programming just Imperative Programming in disguise?

A YouTube video I was watching explained the differences between Imperative and Functional programming by demonstrating how the numbers from 1 to ...
6
votes
1answer
240 views

How is the definition of monads in category theory equivalent to the definition in functional programming?

In Haskell, Monad is a class of type constructors which act on types that have the following functions implemented: ...
5
votes
2answers
414 views

What terms type systems exclude?

I understand type systems like the simply typed lambda calculus, system F and the calculus of constructions include a different subset of all lambda terms. But what, precisely, are the terms each of ...
6
votes
2answers
292 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 ...
5
votes
1answer
383 views

Non-termination of types in Martin-Löf's Type:Type?

In the pre-history of dependent type theory, Per Martin Löf introduced a calculus that is in some sense the simplest dependent type theory and the most general form of impredicative polymorphism. It ...
5
votes
1answer
379 views

Lazy concatenative functional language

Can the idea of concatenative programming languages be extended to call-by-need evaluation strategy? I see some problems that I will explain with few examples. I will use a prefix instead of a ...
2
votes
1answer
139 views

Why do we distinguish between term abstraction and type abstraction in System F?

In System F, we distinguish between types and terms. Types are defined by the following BNF: \begin{align} A, B ::=&~\alpha && \text{(type variable)} \\ &|~A \rightarrow B &...
2
votes
1answer
1k views

Reducing lambda expression to normal form

Can someone explain the steps to reduce $$ (\lambda n. \lambda m. \lambda f. \lambda x.\ n\ (m\ f)\ x)\ (\lambda f. \lambda x.\ f\ (f\ x))\ (\lambda f. \lambda x.\ f\ x) $$ to $\lambda y. \lambda z.\...
2
votes
2answers
49 views

Using function composition to turn a function into point free one

In Tacit Programming page on wikipedia, it is stated that the point free version of p x y z = f (g x y) z is p = ((.) f) . g ...
2
votes
2answers
99 views

Inference of a measure for a decreasing chain

Given integers $v_0,\dots,v_{n-1} \in \mathbb{N}$, I want to find an integer $t>0$, a map $f:\mathbb{N} \times \{0,1,\dots,n-1\} \to \mathbb{N}^t$, and a well-founded order $>_t$ on $\mathbb{N}^...
1
vote
1answer
79 views

how to deduce a function subtype rule from a given function type definition

This question relates to liskov substitution principle seems to have two conventional meanings but is really a different question, so I'm posing it as a new question. I'm doing a bit of research into ...
0
votes
1answer
87 views

Could the execution of a Haskell program be considered as a proof using equational reasoning

Could the execution of a Haskell program be considered as a proof in equational reasoning. This follows on from my earlier question on Haskell and inductive proof. Currently I am stuck between morally ...
0
votes
1answer
106 views

Proving equality between foldl recursive and iterative fold

Hi I have two definitions of fold. I will call them foldl which is recursive and fold$_{itr}$ which is iterative. I am looking for an algebraic proof that the two definitions are equal ideally ...