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.
312
questions
5
votes
4answers
162 views
Is there difference between a function in mathematics to a function in computer science?
I never learned a lot of mathematics (generally only arithmetic) and never learned computer science in a formal frame.
I emphasize that I don't mean to ask about a "function" in programming (...
5
votes
0answers
164 views
Normalization-by-evaluation for untyped lambda calculus which results in 𝛽𝜂-normal form
Usual NbE algorithms for untyped lambda calculus, which use (P)HOAS to embed terms to a host language constructs, results in a beta-normal form of a terms.
Is there algorithms to (efficiently) exploit ...
0
votes
0answers
74 views
Can we think of a non-symmetric product type in Haskell?
Meta note: I asked this question here a while ago. It got an answer:
type a /\!! b = (a, ((b -> Void) -> Void))
Unfortunately, I do not reckon it to be ...
1
vote
1answer
51 views
For every imperative function, is there a functional counterpart with identical performance or even instructions?
Currently, I haven't learned about a functional language that can achieve the same performance as C/C++. And I have learned that some languages that favor functional programming to imperative ...
1
vote
0answers
51 views
What is the category theory interpretation of higher order abstract syntax?
Suppose you have a simple sort of lambda calculus abstract syntax tree. The fine details don't really matter.
...
-1
votes
1answer
40 views
Repeating functions in functional programming?
Functional programming is said to be superior in many ways to imperitive programming. But I am struggling to find a simple functional way of writing:
...
1
vote
0answers
15 views
N-dimensional generalization of map and reduce?
Is there any conceptual generalization of higher-order functions like map and reduce but for N-dimensional objects (e.g. arrays or tensors)?
For mapping, I guess it would be a point-wise ...
4
votes
3answers
115 views
Can lists be defined in a special way so that they contain things of different type?
In https://www.seas.harvard.edu/courses/cs152/2019sp/lectures/lec18-monads.pdf it is written that
A type $\tau$ list is the type of lists with elements of type $\tau$
Why must a list contain ...
1
vote
1answer
97 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, \, ...
3
votes
1answer
251 views
The meaning and relevance of the locution ''no terminating implementation'' in type theory
In the context of a discussion of Haskell https://stackoverflow.com/questions/62509788/the-intuition-behind-the-definition-of-the-co-reader-monad, I was told that
There is no terminating ...
1
vote
2answers
77 views
Lambda Calculus Conversion
How can I take a Haskell data type or function (eg fold, list, String, zip) and convert or translate it to a lambda calculus abstraction?
Example:
If sum computes a sum of all elements in a list, and
:...
2
votes
1answer
76 views
A monad is just a monoid in the category of endofunctors, what's the enlightenment?
Pardon the word play. I'm a little confused about the implication of the claim and hence the question.
Background: I ventured into Category Theory to understand the theoretical underpinnings of ...
3
votes
0answers
57 views
What's the meaning of linguistics?
In the programming language theory world, there are two important terminologies, i.e syntax, and semantics.
I can understand these two terminologies:
syntax is about sentence's structure (e.g. a valid ...
3
votes
1answer
104 views
Functional Programming and Category Theory
I'm a math Ph.D. having done research in Algebraic Geometry and Algebraic Topology in grad school for my thesis and I've studied a fair amount of category theory in the process (e.g. having worked ...
1
vote
0answers
55 views
Is there a known way to make an efficient, compact, and fully persistent stack or queue?
In the world of mutable/ephemeral data structures and imperative programming languages, one of the classic ways to implement a stack or queue is to use array doubling: use mutation to fill up or empty ...
2
votes
1answer
149 views
Organizing a “speedback”
Speedback is the merging of speed-dating with feedback: a 2 min. 1-on-1 talk with all members of a group of people.
I'm in a team and I want to plan the ideal speedback setup: all team members have ...
2
votes
3answers
89 views
Uncurrying and Polymorphism
How do we uncurry functions when they are polymorphic? For example, is it possible to uncurry the following types? If so what is the uncurried type?
$\forall X. X \rightarrow int \rightarrow X$ ?
$...
3
votes
1answer
24 views
Pattern matching on function application
Suppose we have a function f :: a -> b and a function g :: b -> a such that f . g = id....
4
votes
2answers
89 views
Why is the second operation of a Monad called bind?
I understand how monadic computation works, I am just wondering where does the name come from. I cannot relate the thing that the bind operator actually does (i.e. ...
2
votes
0answers
32 views
Compiling an impure language into a pure stack-based language
For a personal learning and fun project, I build an abstract virtual machine based on a stack. The instructions are simple and act on the top of the stack only. There are also stack operators such as <...
2
votes
0answers
18 views
Reducing Kleene's predecessor for Church numerals
I am trying to "reinvent" Kleene's predecessor myself. The following code snippet should be self-explanatory. The idea is to make a 2-tuple and count up from zero, i.e. ...
0
votes
1answer
31 views
What kind of Grammar could this be
I am trying to sort Grammar into the Chomsky Hierarchy and I can do so for most of my examples but I am stumped by the following one:
bX -> abY
which Type of ...
0
votes
1answer
54 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:
...
-2
votes
1answer
72 views
Lambda Expression Reduction
I am unable to solve the following lambda expression using both normal order (Call-by-name) and applicative order (Call-by-value) reduction. I keep getting different answers for both. This is the ...
0
votes
1answer
62 views
generic way to convert imperative if-then-else statements into functional style?
In this question, I asked about a reference for translating imperative code to functional code. I want to ask a more specific question here.
How, in general, do we translate into functional style, a ...
1
vote
2answers
68 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 ...
0
votes
1answer
24 views
Converting a function with single parameter to a function with multiple parameters
I have been solving some algorithm questions recently and a pattern I have observed in some problems is as follows:
Given a string or a list, do an aggregation operation on each of its elements. Here ...
3
votes
2answers
142 views
When is cumulative type universes useful?
AFAIK, a hierarchy of type universe(Type^0: Type^1: Type^2: ...) was introduced to avoid inconsistency caused by Type: Type.
...
1
vote
0answers
26 views
What is the maths name for a set which contains the Domain and Codomain of a function? [closed]
Im interested in this so that I can name a type parameter in a program I'm writing.
There is function that that has three parameters.
D, Domain
C, Codomain
X, where D is a subset of X and C is a ...
1
vote
0answers
40 views
Relationship between left identity and associativity
In an effort to better-grok monads I have reviewed many "Everything you need to know about Monads" tutorials out in the wild, but I feel like my understanding is still coming up a bit short.
While ...
0
votes
2answers
169 views
Does the callback concept of programming have any basis in computer science?
Although I seriously code with computer languages in general since 2010 and as an amateur programmer with programming languages in particular since 2015 (primarily Bash and JavaScript imperative ...
9
votes
1answer
133 views
Semantics for de Bruijn levels
There is an exceptionally simple way to embed simply typed lambda calculus with de Bruijn indices in a functional host language (discussed by Carette, Kiselyov & Shan, and by Kiselyov). The ...
-1
votes
1answer
107 views
Applying FP/Categorical terminology to non-FP languages
In my continuing effort to finally wrap my brain around advanced FP/categorical concepts, I've been reading dozens of articles and tutorials; what I have concluded is that:
1) Category Theory and ...
0
votes
2answers
39 views
If declarative programming is possible at the instruction/action level?
I am considering what the possibilities are with declarative programming. I have a firm understanding of how to use declarative programming in practice, but, short of having examples, I don't know if ...
1
vote
0answers
83 views
Predecessor function with recursive types
I am defining the type Nat of natural numbers a recursive sum type:
$$ Nat = \mu X. Unit \oplus X$$
Now, I have defined zero ...
2
votes
0answers
58 views
Simulating extensible sums with dependent types?
ML-style languages have a concept of "extensible" or "open" sum types, where variants can be declared at any point, and there's not a fixed number of constructors for the type. They're usually used to ...
5
votes
0answers
48 views
Rules for consistency with mutual inductive families?
I'm trying to use a proof assistant to define a type and a relation that are mutually dependent on each other:
...
0
votes
0answers
72 views
Is this proof of the map fusion law correct?
I am reading Functional Programming in Scala, where I have been asked to prove the map fusion law. Since Scala is what I am familiar with, I am using as my notation a kind of pseudo-Scala.
Here is ...
5
votes
1answer
336 views
Why does higher-order abstract syntax need an inverse to define catamorphisms?
In the introduction to the colorfully-named Boxes Go Bananas: Encoding Higher-Order Abstract Syntax with Parametric Polymorphism, Washburn and Weirich describe a problem in traditional formulations of ...
2
votes
1answer
65 views
How does the function to curry and uncurrying another function work?
The following is the code to curry or uncurry a function in Haskell:
...
5
votes
1answer
301 views
How to write a coterminating, effectful program?
[Using Idris for code examples and terminology, but the question is not about Idris per se]
In a post titled A Neighborhood of Infinity, @sigfpe argues that "the kind of open-ended loop we see in ...
2
votes
1answer
46 views
Can most programs (except the IO part) be re-written as a sequence of matrix operations?
I got this idea recently. If we do not consider the data IO part of software, imagine the data is in the memory and we need to come out with some decision (which product to recommend to a user, how to ...
0
votes
0answers
40 views
What is the point-free version of f(x,y)?
What is the point-free version of
f(x, y)
? Is it just f or some kind of function composition, since when curried there is an implicit function which is made ...
2
votes
2answers
54 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
0answers
68 views
Integer-array indexing (e.g. numpy.take) as function composition: where can I find more resources?
For context, one of Numpy's features is that an an array of integers can be passed as an index to an array, and this selects values at all of the specified positions, in any order with possible ...
0
votes
1answer
30 views
What is the relation between the formal definition of strictness and its intuitive notion
I am currently reading Functional Programming in Scala and have encountered a statement in the book I cannot quite make sense of.
On page 67, we are told the formal definition of strictness:
"If the ...
2
votes
1answer
82 views
Like transitive reduction, but removing vertices rather than edges?
Suppose I have a directed graph $G = (V, E)$ (or, which is the same, a relation on the set $V$ as defined by the adjacency matrix) that may contain three vertices $x, y, z$, such that $xy, xz, yz \in ...
1
vote
2answers
109 views
Can we always transform a set of lines to a function?
If I have n lines in a programming language like Python (globally or inside a function):
...
-2
votes
1answer
33 views
2
votes
1answer
62 views
Are the definitions of constructs in terms of lambda terms issues in implementation/design or uses of functional languages?
In Lambda Calculus, natural numbers, boolean values, list processing functions, recursion, if function are defined in terms of lambda terms. For example, natural numbers are defined as Church numerals,...
