# Tag Info

64

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 are pieces of syntax, i.e. collections of symbols on a page. We have rules for manipulating these collections of symbols, most significantly beta reduction. You ...

40

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 refinement type systems generally, is restricted to decidable fragments so that verification (and inference) is completely automatic, meaning one does not require ...

34

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 the number of $\beta$-reduction steps $(\lambda x.M)N \rightarrow M[N/x]$. But is this a good complexity measure? To answer this question, we should clarify ...

31

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 doesn't make any sense – it's like asking a character in a painting why she always stares in the same direction. The advantage of having no time is that you never† need to worry about the order in ...

31

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 Models of Computer Programming by Peter Van Roy and Seif Haridi. (Unfortunately, the companion wiki does not seem to exist any more.) CTM (as it is colloquially ...

27

The main theorem regarding this issue is due to a British mathematician from the end of the 16th century, called William Shakespeare. His best known paper on the subject is entitled "Romeo and Juliet" was published in 1597, though the research work was conducted a few years earlier, inspired but such precursors as Arthur Brooke and William Painter. His main ...

25

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. Grammar Term   ::=   (Elim)   |   *   |   (Var:Term)→Term   |   λVar↦Term Elim   ::=   ...

24

Positive result: persistence does not cost too much. One can show that every data structure can be made fully persistent with at most a $O(\lg n)$ slowdown. Proof: You can take an array and make it persistent using standard data structures (e.g., a balanced binary tree; see the end of this answer for a bit more detail). This incurs a $O(\lg n)$ slowdown: ...

23

Refinement types are simply usual types with predicates. That is, given that $T$ is a usual type and $P$ is some predicate on $T$ $$\{v:T \mid P(v)\}$$ is a refinement type. $T$ in this case is called a base type. AFAIK, in Liquid Haskell, they also allow some dependend function types, that is types $\{x:T_1 \to T_2 \mid P\}$ [1]. Notice that fully ...

23

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 very useful answer :-). Computation expressions are a language feature that gives you a syntax which can be used for programming with computations (or data types) ...

23

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 your topic: Hal Abelson's, Jerry Sussman's and Julie Sussman's Structure and Interpretation of Computer Programs (MIT Press, 1984; ISBN 0-262-01077-1), aka the ...

23

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 RAMs. You were probably thinking of the whole $\Omega$/$\Theta$/$O$-business. While it's true that you can abstract away some implementation details with ...

18

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 are the list of arguments in the calling list, at the point in the source code where a function is called (ie used).

18

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 your example may also put more pressure on the CPU's cache prefetch system. So do test it before declaring it more efficient.

16

Dependent types are types which depend on values in any way. A classic example is "the type of vectors of length n", where n is a value. Refinement types, as you say in the question, consist of all values of a given type which satisfy a given predicate. E.g. the type of positive numbers. These concepts aren't particularly related (that I know of). Of course, ...

16

There are four main approaches, though these only scratch the surface of what is available: via lambdas and records: the idea is to encode objects, classes and methods in terms of more traditional constructs. Benjamin Pierce's work from the mid 90s is representative of this approach. Abadi and Cardelli's object calculi (see Abadi and Cardelli's book A ...

14

You should be more precise. When you say that f(x), f a and m >>= f are "the same", that does not make sense as written. f(x) and f a cannot be the same, they do not even use the same variables. Did you mean to compare f(u), f u and u >>= f? It is true that f(u) and f u are the same thing, but u >>= f is not. If f has type a -> m b (...

13

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 runtime, see Chris Okasaki's book referenced below or my answer here. Of course, as an variant, each leaf of such a tree could itself contain an immutable array ...

13

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, I'll sketch an elementary one, only. We will use a Coq-like notation. We start by defining a predicate requiring that f: nat -> nat acts as a permutation ...

13

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 sets using the usual set theoretic product, it's a legitimate, and non-trivial question whether there is some weaker notion of product that would work, while ...

12

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 a Metaclass? The documents present the structure of instance and inheritance relations between objects. Such a structure can be considered the highest ...

12

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 irrelevant whether action world gets speculatively evaluated or not, action doesn't have any side-effects, its effects, if any, are handled by returning a new state of the universe where those effects ...

11

Quick note, I allow parametric polymorphism (System F) in this system so that S, K and I can work over all types. Notice that without pattern matching, we can't write an if no matter what we do. We have absolutely no operations on booleans. There is no way to distinguish True from False. Instead try true : a -> a -> a true = \t -> \f -> t ...

11

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 = g\ x) \Leftrightarrow f = g).$$ Informally it means that if two functions are equal point-wise, then we consider them equal. Syntactically merge-sort and ...

11

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, think AST). You also need to add a couple of additional operations like quoting and unquoting. That's more or less it. Lisp had that early on because of its easy ...

11

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 certain syntax, and for which a notion of computation (rewriting) is defined. In programming language theory, term can mean specifically one of the two aspects....

11

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. When you call a function, you manually traverse the syntax tree to replace its parameters with the argument. This is easy, but terribly inefficient in terms of ...

10

I would like to venture an opinion that is different from those of @babou and @YuvalFilmus: It is vital for pure $\lambda$-calculus to have anonymous functions. The problem with having only named functions is that you need to know in advance how many names you will need. But in the pure $\lambda$-calculus you have no a priori bound on the number of ...

10

Referential transparency is an operational notion: it describes what happens when you evaluate a same piece of code (typically a function) several times, namely, the return value is the same. In particular, the evaluation context can generally be ignored when considering the operational semantics of a referentially transparent language. Equational reasoning ...

10

If we peel off the syntactic sugar on the front and the code generation on the back and compare what happens in between when converting source to running code for imperative languages, such as C or Java with functional languages such as ML or OCaml we will generally find the following differences in what, why, and how. Mutable vs. immutable With functional ...

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