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.
331
questions
-3
votes
0answers
26 views
In Scala, converting CSV into map using first line values as keys and columns values as arrays [closed]
I have this format data in CSV :
A,B,C,D
1,2,3,4
5,6,7,8
9,10,11,12
And I need to convert it to map of below format, using lambda expression (no loops)
...
0
votes
0answers
29 views
Haskell Map with multiple arguments [closed]
I am an absolute beginner and in my introductory class to Haskell we were talking about map and its uses. As an example problem to try out, we were asked to write a function which merges two lists. ...
3
votes
1answer
100 views
Is mutual inductive type definition essential in coq core language?
I'm studying Coq's core language and I found that mutual inductive type definition is in it.
https://coq.inria.fr/refman/language/core/inductive.html#theory-of-inductive-definitions
Before I read the ...
3
votes
2answers
76 views
Plain-language example of how a functional style makes parallel programming easier
I read a few "function >> imperative/OOP" articles because I heard there was a move in imperative OOP languages toward a functional style of coding, especially encouraging pure ...
0
votes
2answers
17 views
What is name of type “ Function->Value->Bool = if (Bool) Function (Value) ” in Category theory?
I am very new to functional programming so sorry if the question is stupid.
Having this function
...
0
votes
0answers
15 views
Is there a uniform way of giving for any mathematical formula a hypercomputer that computes it?
Some mathematical formulas directly suggest an algorithm for computing it (even if sometimes an inefficient one).
For example, if we recursively define $\sum_{i=1}^nx_i=x_n+\sum_{i=1}^{n-1}x_i$, then ...
5
votes
2answers
193 views
Regarding Backus' Commentary on von Neumann-style Programming
in John Backus' 1978 FP paper "Can Programming Be Liberated from the von Neumann Style" he says
To help assemble the overall result from single words [von Neumann ie.
conventional mutation-...
2
votes
1answer
75 views
Meaning of Free (Arbitrary Abstract Algebra Term)
I'm currently learning abstract algebra and the word free appears (free monoid, free vector space) throughout different literatures. Is there a general (and simple) definition of the word (and ...
2
votes
1answer
61 views
Curry–Howard correspondence and functional programming “reliability”
The first time I heard about functional programming, someone told me "it's more reliable to code in a functional style because your type system is like a proof of correctness".
I recently ...
10
votes
1answer
1k views
What is the name of this type of program optimization where two loops operating over common data are combined into a single loop?
On an imperative programming language, let us consider the following program:
...
1
vote
0answers
24 views
Should I use Dr. Racket for learning Scheme?
I've been fiddling with software development for a couple of years and in trying to get into the gist of things I came across SICP, which uses Scheme.
Basically what I want to do at this stage is to ...
0
votes
0answers
33 views
Can a lambda expression be beta-equal to beta-normal forms?
Given a Lambda Expression Term T can it be beta-equal to two different Lambda Terms T1 and T2, both T1 and T2 are in beta-normal form?
2
votes
1answer
52 views
Computation equivalence of functional and procedural programming
I'm really interested in the idea of functional programming, it seems like a very modular way of doings things. I've seen some suggestion that functional programming is just as powerful as procedural ...
2
votes
1answer
57 views
Show that term cons works by showing all beta reductions
I'm new to functional programming.
So the terms cons appends an element to the front of the list. Where cons ≜ λx:λl:λc:λn: c x (l c n).
How should I go about proving that cons works correctly using ...
1
vote
0answers
105 views
Constraint based analysis: understanding the program $[[ \text{fn} \ x => [x]^1]^2 [ \text{fn} \ y => [y]^3]^4]^5$
I am currently studying the textbook Principles of Program Analysis by Flemming Nielson, Hanne R. Nielson, and Chris Hankin. Chapter 1.4 Constraint Based Analysis says the following:
1.4 Constraint ...
2
votes
0answers
63 views
The word “algebra” in category theory
I am currently learning category theory and a saying that I see a lot is that X is the algebra of something (e.g. Monoid is an algebra of something). Can someone explain to me what that means? Thanks!
2
votes
1answer
54 views
Is well-founded recursion enough for practical total functional programming?
Total functional programming is a paradigm of non-Turing-complete programming languages where any program that type checks is proven to halt.
Well-founded recursion is a recursive definition of a ...
3
votes
1answer
115 views
How to prove that the Church encoding, forall r. (F r -> r) -> r, gives an initial algebra of the functor F?
The well-known Church encoding of natural numbers can be generalized to use an arbitrary (covariant) functor F. The result is the type, call it ...
3
votes
1answer
68 views
Loop optimization of non-tail recursion
When researching how to optimize recursion into loops, I came upon (on Wikipedia) a general rule about this: Whenever a function is in form:
...
4
votes
2answers
148 views
What are the implications of Homotopy Type Theory?
I've recently come across the topic of homotopy type theory and I'm interested to learn more. I have a very limited background in type theory.
Can anyone tell me, in functional programming terms or ...
6
votes
4answers
184 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
176 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
87 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
65 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
57 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
73 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
18 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
130 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
117 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
255 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
87 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
187 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
64 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
145 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
59 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
155 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
97 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
25 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
119 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
37 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
24 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
65 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
81 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
70 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
79 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
25 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
176 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
28 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
45 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 ...
