63

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


39

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


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


24

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


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

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


20

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


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.


17

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


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


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


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

Well, that of course depends on what sort of program you are trying to design. If you are designing an accounting program for your aunt's chocolate shop, I very much doubt category theory will be of much use. But there are of course situations in which category theory is enormously useful in design of programs (by which I also mean data structures, ...


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


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

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

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

Yatima2975 seems to have covered your first two questions, I'll try to cover the third. To do this I'll treat an unrealistically simple case, but I'm sure you'll be able to imagine something more realistic. Imagine you want to compute the depth of the full binary tree of order $n$. The type of (unlabeled) binary trees is (in Haskell syntax): type Tree = ...


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


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

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

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 procedures for certain properties of functional programs. The ability to specify program properties usually takes place within a logic. Dependent types are a ...


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