# Tag Info

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 ...

### 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 ...
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 ...
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 ...

### 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. ...

### 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 ...
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 ...
Accepted

You should be more precise. When you say that f(x), f a and m >>= f are "the same", ...
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 ...
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 ...
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,...
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 ...

### 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 ...

### 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 ...
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, ...
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. ...
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 ...
Accepted

### Why is map insertionsort not to equal tomap 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 = ...
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 ...

### 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 ...

### 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 ...
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 ...
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 ...

### 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.

### 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 ...

### 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: ...

### 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 ...
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 ...