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
21 votes
1 answer
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 ...
Realz Slaw's user avatar
  • 6,191
137 votes
7 answers
40k 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 ...
user avatar
19 votes
3 answers
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 ...
Gilles 'SO- stop being evil''s user avatar
22 votes
2 answers
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, ...
Guy Coder's user avatar
  • 5,091
13 votes
2 answers
2k 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?
Viclib's user avatar
  • 441
11 votes
2 answers
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,...
Tvaroh's user avatar
  • 255
10 votes
2 answers
514 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 ...
Andrey Shchekin's user avatar
9 votes
2 answers
965 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 ...
MaiaVictor's user avatar
  • 4,127
8 votes
3 answers
472 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 ...
Gilles 'SO- stop being evil''s user avatar
5 votes
2 answers
457 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 ...
Jake's user avatar
  • 3,800
3 votes
1 answer
587 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 ...
Patrick Browne's user avatar
2 votes
1 answer
393 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: ...
blue-dino's user avatar
  • 199
76 votes
4 answers
17k 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 ...
Joey Eremondi's user avatar
38 votes
3 answers
5k 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 ...
wsaleem's user avatar
  • 581
32 votes
2 answers
10k 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 ...
Robin Green's user avatar
27 votes
3 answers
4k 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 ...
Guy Coder's user avatar
  • 5,091
23 votes
4 answers
5k 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 ...
gpuguy's user avatar
  • 1,799
20 votes
4 answers
1k 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 ...
Rohan Prabhu's user avatar
17 votes
3 answers
817 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, ...
daniel gratzer's user avatar
14 votes
1 answer
3k views

Concise example of exponential cost of ML type inference

It was brought to my attention that the cost of type inference in a functional language like OCaml can be very high. The claim is that there is a sequence of expressions such that for each expression ...
mrrusof's user avatar
  • 241
8 votes
2 answers
2k 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 ...
CodyBugstein's user avatar
  • 2,957
7 votes
1 answer
404 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: ...
Eben Kadile's user avatar
6 votes
1 answer
362 views

Why are there two not operators in lambda calculus?

From Wikipedia: $\mathrm{true} = \lambda a. \lambda b. a$ $\mathrm{false} = \lambda a. \lambda b. b$ Because true and false choose the first or second parameter they may be combined to provide logic ...
HappyFace's user avatar
  • 191
6 votes
1 answer
534 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 ...
Martin Berger's user avatar
6 votes
1 answer
638 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 ...
user3368561's user avatar
6 votes
2 answers
346 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 ...
john mangual's user avatar
  • 1,941
5 votes
2 answers
497 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 ...
MaiaVictor's user avatar
  • 4,127
2 votes
1 answer
247 views

Creating a large tuple from smaller tuples via a monad or applicative

Suppose I have a term $a :\alpha$ of the Simply-Typed Lambda Calculus (in the following, $\alpha, \beta, \gamma$ stand for arbitrary types) and I want to lift it to a term $\lambda x_{\beta}. \;(x, \, ...
user65526's user avatar
  • 194
2 votes
1 answer
171 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 &...
Aadit M Shah's user avatar
2 votes
2 answers
70 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 ...
al pal's user avatar
  • 621
2 votes
1 answer
2k 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.\...
n0unc3's user avatar
  • 33
1 vote
2 answers
170 views

resource on translating imperative programs to functional programs

I'm not asking this question for the purpose of any particular project. Rather, I'm trying to understand how to translate non-trivial programs in imperative style to functional style. By functional ...
user56834's user avatar
  • 3,702
1 vote
1 answer
152 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 ...
Jim Newton's user avatar
0 votes
0 answers
41 views

Question about machine learning

Hello everyone I am new to the site, I have a question that was in the test and did not understand the parts that are in the question. This question from a test I failed to pass, in a machine learning ...
hah's user avatar
  • 29
0 votes
1 answer
128 views

lambda calculus beta reductions: ((((lambda f (lambda x ((f x) f))) (lambda y (lambda g (g (* y y))))) 2) (lambda a a))

My question is in continuation to lambda calculus reduction: (((lambda f (lambda x (f x))) (lambda y (* y y))) 12) given the input: ...
Dhruv's user avatar
  • 137
0 votes
1 answer
130 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 ...
Patrick Browne's user avatar
0 votes
1 answer
143 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 ...
Abdul Rahman's user avatar
-2 votes
2 answers
2k views

Are mathematical functions used in computer science? [closed]

Well, I know the difference between functions used in math and C language. But what are those specific areas where mathematical functions are used?
Bilal Sheikh's user avatar