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.
38
questions
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 ...
- 6,171
137
votes
7
answers
39k
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 ...
dan
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 ...
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, ...
- 5,071
75
votes
4
answers
16k
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 ...
- 29.5k
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?
- 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,...
- 255
10
votes
2
answers
495
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 ...
- 203
9
votes
2
answers
868
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 ...
- 4,047
8
votes
3
answers
456
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 ...
5
votes
2
answers
394
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 ...
- 3,760
3
votes
1
answer
582
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 ...
- 339
2
votes
1
answer
388
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:
...
- 199
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 ...
- 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 ...
- 663
27
votes
3
answers
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 ...
- 5,071
23
votes
4
answers
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 ...
- 1,769
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 ...
- 303
17
votes
3
answers
774
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, ...
- 1,480
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 ...
- 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 ...
- 2,907
7
votes
1
answer
358
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:
...
- 235
6
votes
1
answer
313
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 ...
- 191
6
votes
1
answer
589
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 ...
- 475
6
votes
1
answer
512
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 ...
- 8,268
6
votes
2
answers
339
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
...
- 1,911
5
votes
2
answers
486
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 ...
- 4,047
2
votes
1
answer
166
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 &...
- 435
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
...
- 611
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.\...
- 33
2
votes
1
answer
213
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, \, ...
- 194
1
vote
2
answers
147
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 ...
- 3,492
1
vote
1
answer
148
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 ...
- 315
0
votes
0
answers
38
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 ...
- 29
0
votes
1
answer
123
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 ...
- 339
0
votes
1
answer
141
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 ...
- 173
0
votes
1
answer
118
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:
...
- 137
-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?
