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 ...
user avatar
42 votes
Accepted

Dependent types vs refinement types

The main differences are along two dimensions -- in the underlying theory, and in how they can be used. Lets just focus on the latter. As a user, the "logic" of specifications in LiquidHaskell and ...
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 ...
user avatar
31 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 ...
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 ...
user avatar
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. ...
user avatar
  • 546
23 votes
Accepted

Is computation expression the same as monad?

First of all, computation expressions are a language feature, while monads are mathematical abstractions, so from this point of view, they are completely different things. But that would not be a ...
user avatar
23 votes

Difference between normal-order and applicative-order evaluation

What research have you done to answer that question? I just plugged it as it is in Google, and got as second answer (the first may be as good, I did not check) a reference to a section of a bible on ...
user avatar
  • 19.1k
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 ...
user avatar
  • 70.9k
19 votes
Accepted

What does "dummy argument" mean?

In fortran a dummy argument is what other languages refer to as a formal argument. So the dummy arguments are the list of arguments in the function (or subroutine) definition. The actual arguments ...
user avatar
  • 306
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 ...
user avatar
  • 18.9k
14 votes

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 ...
user avatar
  • 7,744
14 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", ...
user avatar
  • 28.2k
13 votes
Accepted

Array-like immutable (persistent) data structure implementation with fast indexing, append, prepend, iteration

The obvious candidate is a persistent balanced binary tree. All the operations you listed can be performed in $O(1)$ or $O(\lg n)$ time, using path copying. For more details on how to achieve this ...
user avatar
  • 141k
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,...
user avatar
  • 14.2k
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 ...
user avatar
12 votes

Is there a theory/abstraction behind OOP?

The connection between object model core and set theory is described in the following documents: Object Membership: The Core Structure of Object Technology Object Membership – Basic Structure What Is ...
user avatar
  • 237
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, ...
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 = ...
user avatar
  • 3,419
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 ...
user avatar
11 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. ...
user avatar
  • 29.1k
10 votes

Why are dependently typed languages such as Agda used for proofs, if supercompilers for simpler typed languages can do the same?

I think you're confusing two things: dependently typed languages are convenient for specifying properties and giving proofs about functional programs. The techniques you mention are possible decision ...
user avatar
  • 7,744
10 votes

Which fixpoint is Haskell list type?

It's the greatest fixed point, or the final coalgebra, depending on how you set things up. In Haskell it is impossible to define the datatype of finite lists because Haskell does not have inductive ...
user avatar
  • 28.2k
10 votes
Accepted

Does immutability in functional programming really exist?

When a program starts it has fixed data structures with fixed data This is a bit of a misconception. It has a fixed form and a fixed set of rewrite rules but these rewrite rules can explode into ...
user avatar
  • 3,728
10 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 ...
user avatar
  • 28.2k
10 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 ...
user avatar
  • 151
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 ...
user avatar
  • 29.1k
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 ...
user avatar
10 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 ...
user avatar
  • 141k
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.
user avatar
  • 5,164

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