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.
-1
votes
0answers
8 views
Simple HTML code and integrating CSS, Python, and JavaScript with the existing HTML code [closed]
Tonight I started programming a makeshift webpage thats not really a webpage. I downloaded Notepad++, opened it and started writing HTML code. I am making a table of information that has (at the ...
5
votes
3answers
66 views
How exactly do we define parametric polymorphism?
My naive distinction between parametric polymorphism and ad-hoc polymorphism, is that:
In parametric polymorphism, the type is given as a variable: (pseudocode)
Function f: <.Type T> T $\to$...
1
vote
0answers
22 views
Generalization of Functors to other datatypes?
Functors in category theory, and also in its application to functional programming, can be seen as a kind of "structured" functions: Given two sets $A,B$, rather than just having a function $f:A\to B$,...
5
votes
0answers
50 views
Difference between “functional programming languages” and “lambda calculus based languages”?
In "Can programming be liberated from the Von Neumann Style?", John Backus states:
The main reason
FP systems are considerably simpler than either conventional languages or lambda-calculus-based ...
2
votes
0answers
29 views
How can one flip a stream using corecursion
Following is the definition of codata stream:
codata Stream where
hd : Stream −> A
tl : Stream −> Stream
For simplicity I assume I have just a ...
1
vote
0answers
39 views
Reasons for why x - 1 and x -1 gives different result in some languages [closed]
I assume the reason space makes a difference in F# is due to reserving a certain function, when minus is in front of a number without space, however what are the reasons for this? I can't seem to find ...
9
votes
0answers
139 views
How would a CPU designed purely for functional programming be different?
CPU's are to an extent designed with in mind the software that people will write for it, implicitly or explicitly.
It seems to me that if you look at the design of instruction set architectures, ...
1
vote
0answers
24 views
Intuition for “run” function of monads
I'm learning about monads, I understood why they are useful, I understood in general what bind, join, return do.
I also looked at basic usage examples for the basic reader / writer / state / list / ...
3
votes
1answer
47 views
What are different ways to provide a semantics to a language?
Suppose you have 1. a grammar for terms of a language; 2. type-assignment rules, 3. a set of reduction rules. You want to prove that your language is adequate for mathematical reasoning. If I ...
1
vote
1answer
33 views
Tailrecursive definition for a function
In an exam I took we were asked to provide a tailrecursive definition of a recursive function. I failed miserably and the provided solution makes absolutely no sense to me. If anyone could explain ...
0
votes
2answers
27 views
Beta reduction order in Lambda calulus
Will it be wrong to use g for reducing (λx.λy.x) first in step (2) instead of using to reduce λg?
Is there a rule against it?
4
votes
1answer
65 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 ...
1
vote
0answers
28 views
Can you use CPS to simulate state in a stateless programming language?
In a language supporting CPS, but no built in global state, we can represent a state based computation using a function. We call this function a state function. Assume the function takes three ...
2
votes
2answers
36 views
When are you supposed to eta-reduce?
Wikipedia lists the following algorithm for normalizing a lambda calculus term $t$:
If $t$ is not in head normal form, beta reduce the beta redex in the head position to get $t'$. Then normalize $t'$ ...
0
votes
0answers
24 views
Composition of compostion as a functor
"Composition of Composition" (i.e., (.) . (.)) in Haskell), has type ...
0
votes
1answer
102 views
First-order vs Higher-order Programs
Can someone explain the difference between first-order programs and higher-order programs in the context of programming languages?
My understanding so far is that Functional Languages (most) use ...
0
votes
2answers
62 views
Multiple inputs in lambda calculus (Confusing example)
In a programming class I take, we briefly (very briefly) touched lambda calculus. I think I have a pretty good grasp of the basics now, but one example given I just don't understand. Am I missing ...
1
vote
1answer
281 views
Is Pattern Matching as expressive as Case Expression in Haskell?
Nomenclature
The term expressive in the question shall bear the same meaning as in the following sentence:
A Turing Machine is as expressive as Lambda Calculus.
Introduction
While learning ...
0
votes
1answer
76 views
join is the heart of the monad because it encompasses everything a monad can do that a functor cannot. Is this true? [closed]
There is a controversy about Monad implementation in S.O .
The original question is,
What's so special about Monads in Kleisli category?
Is there any counterexample that Functors cannot do what ...
2
votes
2answers
82 views
How does one show $(\lambda x . (\lambda y.x))yx \equiv_{\beta} y$ in lambda calculus?
I wanted to show:
$$ (\lambda x . (\lambda y.x))yx \equiv_{\beta} y $$
the definition of beta equivalence is on page 17 of these notes.
I did a few attempts but got different things like $x$. I ...
2
votes
1answer
51 views
How do we show $\lambda x . x (\lambda y .y) \equiv_{\alpha} \lambda y.y (\lambda x . x)$ in lambda calculus?
How do we show $$\lambda x . x (\lambda y .y) \equiv_{\alpha} \lambda y.y (\lambda x . x)$$?
I was going through the slides here and it asked to do the above but by page 16 of the slides we have not ...
-1
votes
1answer
243 views
2
votes
4answers
99 views
How does one formally show that two lambda functions are $\alpha$ equivalent?
I was going through the following slides and I wanted to show the following:
$$ \lambda x. x \equiv_{\alpha} \lambda y . y$$
formally. They define a an $\alpha$-conversion on page 15 as follows:
$$ ...
2
votes
0answers
32 views
What is the difference between ADTs and ASDLs?
ASDL stands for Abstract Syntax Description Language (ASDL), whereby ADT stands for Algebraic data type.
By looking at Python.asdl it appears to me to be the same thingy, just with different names, ...
5
votes
1answer
262 views
About the relationship between non-termination and inconsistency?
I've been trying to get into Agda and I noticed that it doesn't have recursion, which implies that it isn't Turing-Complete.
From what I could understand, if Agda had recursion, it would make itself ...
0
votes
1answer
67 views
Solving equations without side effects
Consider the example of solving for $x$ where $Ax=b$. This is not in general function, there can be more than one solution. So if you make such a solver in a functional style...does this count as a ...
1
vote
0answers
18 views
How does the browser
I wondering how the browser's JS runtime implements these methods. I looked on the web and could not find any documentation.
How does something like the V8 runtime actually work to implement these ...
4
votes
0answers
45 views
Inferring ranking functions in a general code graph with partial information
Let me define the notion of call graph:
A program consists on a set of functions $f,g,h,\ldots$ where each
function $n$ is as a mapping $n: D^l \to D^m$. Here $D$ is the
datatype representing ...
1
vote
0answers
20 views
Nested Function stuck on iteration update
I want to solve the Sparse Extended Information Filter Slam described by Dr. Sebestian Thrun in Probabilistic Robotics.I stuck in some nested function.
The algorithm is described in page 309 in this ...
1
vote
1answer
56 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 ...
1
vote
1answer
56 views
Stablishing termination of the construction of infinite stream with ranking functions
I'm working with Turing's paradigm to prove termination of programs by annotating functions with ranking functions and I encounter the following example:
...
2
votes
1answer
337 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
90 views
Proving parametricity for Gallina functions
I have the following definitions
Definition nat'' {X : Type} := (X -> X) -> X -> X.
Definition nat' := forall (X : Type), @nat'' X.
And when I wanted to ...
20
votes
0answers
485 views
Can a calculus have incremental copying and closed scopes?
A few days ago, I proposed the Abstract Calculus, a minimal untyped language that is very similar to the Lambda Calculus, except for the main difference that substitutions are ...
5
votes
1answer
126 views
Best way to translate while loops to functions for software verification
I have a verification engine where while loops are translated into functional code, like this:
...
2
votes
2answers
94 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
113 views
pure function in C
There does not seem to be a canonical definition of "pure function", but the widespread language-agnostic understanding seems to be a function that
has no side effects
produces a value that is ...
-1
votes
2answers
50 views
Defining an HTML Template as an Algebraic Type
Wondering if/how you could define a highly nested structure as a Dependent Type (or an Algebraic or Parameterized type). Specifically, an HTML template. Not that they work like this (HTML templates ...
1
vote
2answers
135 views
functional vs state-based
As mentioned in Lambda Calculus - Computerphile,
Alonzo Church's method is functional where a function as a blackbox,
takes an input, processes, and produces an output, and Turing machines
...
4
votes
0answers
144 views
Why most purely functional red-black trees are left-leaning?
Is there any particular reason for picking a left-leaning red-black tree over a regular red-black tree when trying to do a purely functional implementation?
I've not researched very deeply into this ...
0
votes
1answer
121 views
Are there any known implementations of a functional Heap's Algorithm?
TL;DR: Is an implementation of the Heap's Algorithm adhering to the principals of functional programming possible, and are any implementations of it known? And by "adhering to the principals of ...
2
votes
0answers
56 views
Term for weak head normal forms that cannot be reduced in any environment
In my understanding, a lambda expression is a normal form (NF) when it has no redexes. For instance, $\lambda x.x$ is a NF, but $(\lambda x.x)y$ is not. A lambda expression is a weak head normal form (...
-2
votes
1answer
43 views
Erlang- Creating a function which only adds/subtracts positive integers
I want to create a function which allows me to input a list, and then add all of the positive numbers from the list together, leaving any that are negative.
([3,1,-1])
For example only 3 and 1 would ...
2
votes
0answers
210 views
How would a priority queue be implemented in a functional programming language?
How would a priority queue be coded efficiently in a functional programming language? I'm new to functional programming, but I'm having difficulty understanding how a data structure that seems to ...
-2
votes
2answers
102 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?
1
vote
1answer
50 views
Is there a combinator that introduces brackets to a combinatory logic expression using just B?
Suppose I have the expression $abcdef$ and I want a combinator $X$ that does this:
$Xabcdef=a(bcd)(ef)$.
Is it possible to express $X$ using just the $B$ combinator, defined by
$Babc=a(bc)$?
Is ...
0
votes
1answer
78 views
Can we define the Functor Category in Haskell (or any other language with a more expressive type system)?
Here I am talking about the Functor category, which is defined as a category whose objects are functors and morphisms are natural transformations.
For reference: https://ncatlab.org/nlab/show/functor+...
3
votes
2answers
69 views
Can we define a program by means of a walk of a graph induced by the category of types?
After reading about Category Theory at https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ I was wondering whether we can represent any program by means of a walk of a ...
3
votes
3answers
159 views
Is it possible to make a language that can build upon itself perfectly?
First of all, note that I'll have to explain my thoughts in a layman's terms.
There are so many high-level programming languages out there that compete with each other. This means we have to build ...
1
vote
2answers
63 views
What mathematical terminology exists for “embellished trees”?
I'm looking for some pointers on proper mathematical (FP?, category-theory?) terminology.
My apologies if the below is somewhat imprecise; I suppose the precision is precisely what I'm looking for in ...
