# 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 ...
• 11.8k
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 ...
• 536

### 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,178
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,651
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,151

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

### 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 ...
• 19.1k

### 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 ...
• 70.9k
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 ...
• 306
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 ...
• 18.9k

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

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

### 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 ...
• 237
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,178
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 = ...
• 3,419
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 ...
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.1k

### 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 ...
• 7,744

### 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 ...
• 28.2k
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 ...
• 3,728
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 ...
• 28.2k

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

### 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.1k
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 ...
• 11.8k