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
2
votes
1answer
63 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 ...
2
votes
2answers
91 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
1k 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
113 views

Lambda Calculus Prove Equality Excessive (Haskell-oriented)

I'm on a lambda calculus with parametric polymorphism a la Hindley-Milner Haskell-oriented course and I'm currently facing this exercise which I got stuck on. Prove that $(\forall m\downarrow, n\...
2
votes
1answer
370 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: ...
2
votes
2answers
588 views

Haskell monad bind operator type

In Haskell, the Monads type class has the bind operator, which is represented by the symbol >>= The type of such operator is: ...
2
votes
3answers
592 views

Expressing semantics of an array as a function

An assignment questions asks the following: Consider an array 'var a : array[1..10] of real'. Express the semantics of this array as a function, defining the domain and codomain (you might ...
2
votes
2answers
174 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 ...
2
votes
1answer
83 views

How is this lamda function beeing executed in an example for the Y combinator

I have spent a few hours now trying to understand how the Y Combinator is working and how it allows us to construct recursive functions with higher order functions. I have been going through this ...
2
votes
2answers
107 views

General term for map/fmap

The general term for folds is a catamorphism. The general term for unfold is an Anamorphism. Is there an equivalent term for map? I know that a map is a type of fold however restriction is ...
2
votes
2answers
226 views

Proving monad laws for flatMap and unit, given laws for compose and unit

I'll use scala notation but hopefully things will make sense in general (I'm trying to prove that you can define a monad using either [flatMap (aka bind) and unit] or [compose and unit]) The book ...
2
votes
2answers
97 views

Functional programming with branches that have no order?

I was wondering if there is any programming style in which the outcome does not depend on the order of statements or groups of statements such as guards. Vaguely, I imagine this would leave room for ...
2
votes
1answer
497 views

Can we prove mathematical induction statements in Lisp?

My previous question Can we prove that $1 + 2 + \dots + n = \frac{n(n+1)}{2}$ using a computer program? has a problem that it tries to cover too much ground. Here is a related question motivated by ...
2
votes
2answers
302 views

Lazy lists with call-by-value reduction strategy

I am currently writing lists with lazy semantics in the pure lambda-calculus with call-by-value reduction strategy. I tried to construct pleasant to use and relatively efficient "lazy" functions on ...
2
votes
1answer
147 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
1answer
144 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 &...
2
votes
1answer
1k views

Call by need compared to pass by function

SML uses pass‑by‑value, Haskell uses call‑by‑need. Unless I'm wrong (the purpose of this question), one can do call‑by‑need with SML, passing a function instead of a value; a function to be later ...
2
votes
1answer
116 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 ...
2
votes
2answers
52 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
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,...
2
votes
2answers
103 views

Is purely functional programming in some situations less efficient than imperative programming?

I am used to implementing algorithms in imperative languages. Many of the algorithms I have implemented use hash maps, hash sets, mutable arrays, heaps, doubly linked lists, etc. I understand that ...
2
votes
1answer
112 views

Can we implement every algorithm using only immutable variables?

Can we implement every algorithm using only immutable variables such that their space and time complexity is the same as using mutable variables?
2
votes
2answers
1k views

Lambda Calculus Type Inference

I'm currently trying to learn how to infer most general types on lambda calculus, and due to the lack of information on the subject I could find on Google I'm forced to attempt what I think is logical ...
2
votes
2answers
92 views

Occurrences notation in “Compiling Pattern Matching to Good Decision Trees”

From Compiling Pattern Matching to Good Decision Trees (Luc Maranget, Proceedings of ML '08, pp. 35–46. ACM, 2008.) We also consider the usual occurrences. Occurrences are sequences ...
2
votes
2answers
301 views

Second order function formalization

I need to work on a optimizer for a language whose operator are second order functions. They are the well known ones filter, map, reduce, fold, foreach etc. etc. I need to formalize as much as ...
2
votes
1answer
340 views

Functional Programming and Parallelism

I have an option to learn a new language for parallel computing. As a parallel programmer what are the reasons one might want to invest time to learn functional programming for parallel computing?
2
votes
1answer
348 views

What is the name of this combinator?

I've recently started casually reading into combinatorial logic, and I noticed that a higher-order function that I regularly use is a combinator. This combinator is actually pretty useful (you can use ...
2
votes
1answer
47 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: ...
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 ...
2
votes
2answers
99 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}^...
2
votes
1answer
185 views

How is the following ML Curry expression evaluated

This question is not homework but it's related to material in a general course I take about programming languages, so I don't know whats the site policy about this In ML the following expression: <...
2
votes
1answer
66 views

Which would be the most purely functional equivalent to generators?

Some programming languages, apart from functions, have generators (eg. Python's yield). Although generators are introduced in this Python's tutorial on functional programming, I don't think that they ...
2
votes
1answer
117 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 ...
2
votes
2answers
88 views

Does proofs are programs apply to any functional program?

Does Curry howard correspondence, apply to all Functional Program, e.g. in Haskell. i.e. Is it possible to write Equivalent Haskell programs, to COQ proofs?
2
votes
1answer
57 views

Formally proving properties of fold function

Recall the fold function for lists: $fold(f,z,[x,xs]) = fold(f,f(z,x),xs)$ $fold(f,z,[]) = z$ I want to formally proof that if $f$ is associative, commutative and idempotent (meaning $f(x,y) = f(x,...
2
votes
1answer
74 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 ...
2
votes
1answer
669 views

Why are both caller-save registers and callee save registers needed?

I am having a difficult time understanding callee and caller-save registers. I get that caller-save registers are those which are needed after function call and hence caller saves them in caller ...
2
votes
1answer
156 views

Is function application actually a memory manipulation algorithm?

I thought about how in lambda calculus (and many implementations of functional programming languages) function (lambda) application and lambda itself, as a construct, are "primitive things", usually ...
2
votes
0answers
52 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 ...
2
votes
0answers
30 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
16 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. ...
2
votes
0answers
52 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 ...
2
votes
0answers
59 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 ...
2
votes
0answers
36 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 ...
2
votes
0answers
40 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, ...
2
votes
0answers
119 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
0answers
423 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
0answers
32 views

numeric stability of map reduce operations

I am building a small library for computing information retrieval metrics for classifiers (precision, recall, f1, accuracy, whatever). Typically each metric is built by calculating a single value for ...
2
votes
0answers
59 views

Functional Core Language representation of tuples

I am writing a compiler for a simple subset of standard ML (just for fun) and I am stuck on how to represent the core language (I should mention that I write it in Haskell probably). Basically what I ...
2
votes
0answers
51 views

Structural induction in non-local program transformation

Assume a functional language and a specialization operation (pulling out sub-expressions): let f x y = (h 23 x) + (g 42 y) becomes ...

1 2 3
4
5
7