117

In a previous answer in the Theoretical Computer Science site, I said that category theory is the "foundation" for type theory. Here, I would like to say something stronger. Category theory is type theory. Conversely, type theory is category theory. Let me expand on these points. Category theory is type theory In any typed formal language, and even in ...


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


34

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

I'm going to try and keep it short and sweet. There is an informal correspondence between Haskell programs and certain classes of categories, which can be made more formal with some work. This correspondence is known as the Curry-Howard-Lambek correspondence and relates: Haskell types with objects of the category Terms of type $A\rightarrow B$ with ...


29

Echoing @AJed advice, I recommend to turn your statement I want to learn category theory so I can become better at Haskell. on its head: learn Haskell, building on your programming intuition. Once you are an FP guru, it might be easier to pick up category theory (if you still care). Category theory is simple for somebody with broad mathematical education ...


26

Neither actors nor FRP are about streaming. Actors don't even support external configuration of an output stream. FRP is strongly characterized by its modeling signals and events on a linear timeline, which enables FRP behaviors to compose in a deterministic manner. Actors are strongly characterized by processing messages in non-deterministic order, and ...


24

Since Prolog = Syntactic Unification + Backward chaining + REPL All three parts can be found in Artificial intelligence: structures and strategies for complex problem solving by George F. Luger. In the fourth edition of the book all three parts are implemented in LISP in Section 15.8, Logic Programming in LISP. He also puts the same code in his other books, ...


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


24

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


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


22

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


22

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


22

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


19

First, some remarks. Using only the core typed lambda calculus it's not possible to obtain 'a -> 'b because the typing system is in correspondence (via the Curry Howard isomorphism) to intuitionistic logics, and the corresponding formula A → B is not a tautology. Other extensions such as tuples and matchings/conditionals still preserve some logic ...


19

When you work with immutable data objects, functions have the property that every time you call them with the same inputs, they produce the same outputs. This makes it easier to conceptualize computations and get them right. It also makes them easier to test. That is just a start. Since mathematics has long worked with functions, there are plenty of ...


18

The skeleton is let f x = BODY. In BODY you must use x only in generic ways (for example, don't send it to a function that expects integers), and you must return a value of any other type. But how can the latter part be true? The only way to satisfy the statement "for all types 'b, the returned value is a value of type 'b" is to make sure the function does ...


17

You are asking for an application outside of computer science and logic. That is easily found, for example in algebraic topology it is convenient to have a cartesian closed category of spaces, see convenient category of topological spaces on nLab. The formal language corresponding to cartesian closed categories is precisely the $\lambda$-calculus. Let me ...


15

"Dummy" as "unused" In general (not in Fortran) a dummy argument is an argument that will not be used by the body of the function. For example, in the following function, z is a dummy argument but x and y are not. int f(int x, int y, int z) { return (x + y); } They can be used for several reasons: depending on another argument or some configuration, ...


15

The lambda calculus is fundamental in logic, category theory, type theory, formal verification, ... Basically, anything to do with programming language semantics and formal logic. It is such a fundamental formalism that people working in these fields do not even question the benefit of it. I think that it is extremely useful for understanding functional ...


15

A Standard ML structure is akin to an algebra. Its signature describes an entire class of algebras of similar shape. A Standard ML functor is a map from a class of algebras to another class of algebras. An analogy is, for instance, with the functors $F : {\bf Mon} \to {\bf Grp}$, which adds an inverse operation to monoids, or $F : {\bf Ab} \to {\bf Rng}$ ...


15

The issue with higher-order functions is simple enough to state. A type-constructor like $T(X) = [X \to X]$ is not a functor. It should have been. A polymorphic function like ${\it twice}_X : T(X) \to T(X) = \lambda f.\, f \circ f$ is not a natural transformation. It should have been. If you read Eilenberg and MacLane's original category theory paper,...


15

It is easier to correctly work with persistent data structures than it is to work with mutable data structures. This, I would say, is the main advantage. Of course, theoretically speaking, anything we do with persistent data structures we can also do with mutable ones, and vice versa. In many cases persitent data structures incure extra costs, usually ...


15

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


15

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


15

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


14

In this answer, I'll stick to a core ML fragment of the language, with just lambda-calculus and polymorphic let following Hindley-Milner. The full OCaml language has additional features such as row polymorphism (which if I recall correctly doesn't change the theoretical complexity, but with which real programs tend to have larger types) and a module system (...


14

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


14

Categories form a (large) category whose objects are the (small) categories and whose morphisms are functors between small categories. In this sense functors in category theory are "higher size morphisms". ML functors are not functors in the categorical sense of the word. But they are "higher size functions" in a type-theoretic sense. Think of concrete ...


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


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