64
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 ...
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
...
- 8,308
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 ...
- 1,671
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 ...
- 5,830
25
votes
What is a brief but complete explanation of a pure/dependent type system?
Let's have a go. I'll not bother about Girard's paradox, because it distracts from the central ideas. I will need to introduce some presentational machinery about judgments and derivations and such.
...
- 546
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 ...
- 72k
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 ...
- 21.6k
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", ...
- 30k
16
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 ...
13
votes
Accepted
No Naive Set Theoretic Models of Polymorphic Lambda Calculus?
The standard reference you are looking for is indeed Reynold's Polymorphism is not Set Theoretic. While it is quite obvious that you cannot form, e.g. the product $\Pi_{S\in\mathrm{Set}}S$ over all ...
- 8,114
13
votes
Accepted
Proving a sorting operation in type system
Yes, it is possible to express a precise type for a sorting routine, such that any function having that type must indeed sort the input list.
While there might be a more advanced and elegant solution,...
- 14.4k
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 ...
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 ...
- 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 ...
- 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, ...
- 8,308
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. ...
- 29.7k
11
votes
Accepted
Can a functional language be homoiconic?
The definition implies not only that programs are represented by a "primitive" datatype, but presumably also that it is possible to inspect the elements of this type, i.e., one can actually get at the ...
- 30k
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 = ...
- 3,469
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 ...
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.♦
- 156k
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 ...
- 29.7k
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 ...
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 ...
- 591
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.
- 6,958
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 ...
- 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:
...
- 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 ...
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 ...
- 30k
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 ...
- 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. ...
- 38.6k
Only top scored, non community-wiki answers of a minimum length are eligible