Skip to main content
Share Your Experience: Take the 2024 Developer Survey
65 votes
Accepted

Is Lambda Calculus purely syntactic?

Ironically, the title is on point but not in the way you seem to mean it which is "is the lambda calculus just a notational convention" which is not accurate. Lambda terms are not functions1. They ...
Derek Elkins left SE's user avatar
34 votes

How is algorithm complexity modeled for functional languages?

If you assume that the $\lambda$-calculus is a good model of functional programming languages, then one may think: the $\lambda$-calculus has a seemingly simple notion of time-complexity: just count ...
Martin Berger's user avatar
32 votes
Accepted

Why do functional languages disallow reassignment of local variables?

In a pure functional programming language, there is no real notion of time at all. So, saying that a variable x has value a at one point and then b later simply ...
leftaroundabout's user avatar
31 votes
Accepted

What are some interesting/important Programming Language Concepts I could teach myself in the coming semester?

Very good explanations of programming paradigms and the programming concepts from which those paradigms are built are found in Peter van Roy's works. Especially in the book Concepts, Techniques, and ...
Jörg W Mittag's user avatar
23 votes

How is algorithm complexity modeled for functional languages?

Algorithm complexity is designed to be independent of lower level details. No, not really. We always count elementary operations in some machine model: Steps for Turing machines. Basic operations on ...
Raphael's user avatar
  • 72.5k
18 votes
Accepted

What is the name of this type of program optimization where two loops operating over common data are combined into a single loop?

It's called "loop fusion". It's often more efficient, in the sense of doing more work per loop iteration and sometimes (as you say) other advantages. On the other hand, the fused loop in ...
Pseudonym's user avatar
  • 22.2k
17 votes
Accepted

Strictness in both arguments but not in each individually

That's a very good question! It turns out the answer is both yes and no. A classic example of a function we'd like to write is Plotkin's parallel or. We know from basic boolean logic that both ...
Gilles 'SO- stop being evil''s user avatar
16 votes
Accepted

“Left identity” of Monad laws in Haskell is wrong

You should be more precise. When you say that f(x), f a and m >>= f are "the same", ...
Andrej Bauer's user avatar
  • 30.8k
13 votes
Accepted

Is the IO monad technically incorrect?

This is a suggested "interpretation" of the IO monad. If you want to take this "interpretation" seriously, then you need to take "RealWorld" seriously. It's ...
Derek Elkins left SE's user avatar
12 votes

What is the Curry-Howard analogue for linear logics?

Linear logic corresponds to a type system for a process calculus (a variant of the internal π-calculus), where: proofs correspond to processes; propositions correspond to session types (communication ...
fmontesi's user avatar
  • 171
12 votes

Dependent types vs refinement types

A refinement type is a type together with a decidable predicate: $$ \{x:T ~|~ p(x)\} $$ where $x$ is a variable name, $T$ is a type, and $p(x)$ is a decidable predicate over $x$. A dependent pair ...
drcicero's user avatar
  • 121
12 votes
Accepted

How to make a language homoiconic

You can make any language homoiconic. Essentially you do this by 'mirroring' the language (meaning for any language constructor you add a corresponding representation of that constructor as data, ...
Martin Berger's user avatar
12 votes
Accepted

λ -calculus : What is the most efficient in memory representation of functions?

The thing is, there's really not much leeway in terms of function encoding. Here are the main options: Term rewriting: you store functions as their abstract syntax trees (or some encoding thereof. ...
Joey Eremondi's user avatar
11 votes
Accepted

Why is `map insertionsort` not to equal to`map mergesort`?

It has to do with the axiom of extensionality, i.e. whether you accept it for functions or not. The statement of this axiom with regard to functions is $$\forall f,g:A \to B,\ ((\forall x:A ,\ f\ x = ...
Anton Trunov's user avatar
  • 3,479
11 votes
Accepted

Are the words "expression" and "term" interchangeable in programming language theory?

The two words expression and term have largely the same sets of possible meaning, but in a specific presentation, they may not be synonyms. In rewriting theory, a term is something that conforms to a ...
Gilles 'SO- stop being evil''s user avatar
11 votes

Why do functional languages disallow reassignment of local variables?

I can only share my perspective. The way I think of it is that mainstream functional languages typically combine two themes: (1) support for higher-order functions, and (2) a preference for pure ...
D.W.'s user avatar
  • 161k
10 votes

Total functional programming language without an static type checker

The question is, how do you eliminate terms that run forever: In particular, things like $(\lambda x \ldotp x\ x)(\lambda x \ldotp x\ x)$ and the Y combinator must NOT be in your language, since they ...
Joey Eremondi's user avatar
10 votes
Accepted

Can literals in functional languages be thought of as functions from the empty type?

Let's start in a total language like Agda. Then, as gallais states, this only makes sense if by "empty type" you mean the unit type, i.e. the 0-ary tuple, which has exactly one value. The empty type ...
Derek Elkins left SE's user avatar
10 votes
Accepted

A monad is just a monoid in the category of endofunctors, what's the enlightenment?

This answer may not be exactly what you are looking for. That is, I think perhaps the importance of this characterisation is being overemphasised here. The quote a monad in X is just a monoid in the ...
varkor's user avatar
  • 661
10 votes

What are some interesting/important Programming Language Concepts I could teach myself in the coming semester?

Check out the book Types and Programming Languages (TAPL) by Benjamin Pierce. This is an excellent introduction to the fundamental concepts of the field of programming languages.
Caleb Stanford's user avatar
10 votes

What exactly is the relation between Haskell and category theory?

Category theory is an abstract branch of mathematics and you do not need to learn it before you start writing Haskell code. Similarly, you do not need to learn Haskell before you start learning ...
axr's user avatar
  • 296
9 votes

How do Functional Reactive Programming and the Actor model relate to each other?

I wanna point out how they are different from a practical point of view: 1) actors send messages to other actors, this message passing is described explicitly and imperatively. For example: ...
jhegedus's user avatar
  • 255
9 votes

Why are the laws of an applicative functor defined the way they are?

As described in the original idioms paper, Applicative (called Idiom there) corresponds to a strong lax monoidal functor. This ...
Derek Elkins left SE's user avatar
9 votes
Accepted

How is the definition of monads in category theory equivalent to the definition in functional programming?

The Haskell monads are known as Kleisli triples in mathematics. I am guessing you're coming from the Haskell land, so let me just put down the translations between the two formulations in Haskell (I ...
Andrej Bauer's user avatar
  • 30.8k
9 votes

Why do functional languages disallow reassignment of local variables?

If we want to be very precise with our words, we should say that in functional programming you don't assign a value to a variable, because assignment is a thing that you "do", and if you are ...
kaya3's user avatar
  • 520
9 votes
Accepted

Does it make sense to call GAP a "procedural" language?

Yes, GAP as a programming language is a procedural language. "The simplest test to apply is that a language is procedural if it has assignable (mutable) variables", Michael Kay pointed out. ...
John L.'s user avatar
  • 39k
8 votes
Accepted

Why is Church-Rosser so important for basing programming languages on lamdba-calculus?

Think of it as a sanity check. CR cones from the days when we were just figuring out what programming languages were. The Lambda calculus was new, and its basic properties were unknown. CR says that ...
Joey Eremondi's user avatar
8 votes
Accepted

Is there a paradigm for composing "incremental update" functions in a pure dataflow style?

This field has been invented many times, and goes under many names, such as: Online algorithms. Streaming algorithms, stream queries, continuous queries. Dynamic data structures. Self-adjusting ...
Martin Berger's user avatar
8 votes
Accepted

Safe way to explicitly define new types instead of using Algebraic data types for my functional language

You're on the right track: people have come up with the same way to do this. The general concept is known as abstract types. With the Church encoding, the type of a pair of elements of types $a$ and $...
Gilles 'SO- stop being evil''s user avatar
8 votes

Is there a point to an all-encompassing programming language?

You can make a language that does all these things. The problem is that it won't be able to do all these things well, because they're contradictory. For example, database manipulation is fundamentally ...
Gilles 'SO- stop being evil''s user avatar

Only top scored, non community-wiki answers of a minimum length are eligible