38

The extent to which this is possible is actually a major open question in the theory of the lambda calculus. Here's a quick summary of what's known: The simply-typed lambda calculus with unit, products, and function space does have a simple canonical forms property. Two terms are equal if and only if they have the same beta-normal, eta-long form. Computing ...


35

There are actually two uses of the word "strength" in play here. A strong endofunctor $F : C \to C$ over a monoidal category $(C, \otimes, I)$ is one which comes with a natural transformation $\sigma : A \otimes F(B) \to F(A \otimes B)$, satisfying some coherence conditions with respect to the associator which I will gloss over. This condition is sometimes ...


26

Here are a few things to keep in mind: Although we generally think we know what we mean by set-theoretic intersection and union, there have been several different takes on what exactly intersection and union types are. So, it's worth pinning this down before you embark on an implementation. One element which I think is awfully important for understanding ...


22

I can think of a few possible answers coming from linear logic. The simplest one is the affine lambda-calculus: consider only lambda-terms in which every variable appears at most once. This condition is preserved by reduction and it is immediate to see that the size of affine terms strictly decreases with each reduction step. Therefore, the untyped affine ...


18

How do type classes fit in this model? The short answer is: they don't. Whenever you introduce coercions, type classes, or other mechanisms for ad-hoc polymorphism into a language, the main design issue you face is coherence. Basically, you need to ensure that typeclass resolution is deterministic, so that a well-typed program has a single ...


17

It's common to say that $f$ and $g$ commute with respect to composition (where the property is known as commutativity). See, e.g., http://en.wikipedia.org/wiki/Function_composition.


16

What are the limitations of total functional programming? It is not Turing-complete, but still supports a large subset of the possible programs. Are there important constructs that you could write in a Turing-complete language, but not in a total functional language? Assuming your functional language $L$ lets you encode arithmetic operations, there is one ...


16

It depends on the total functional language. This answer sounds like a cop-out, but nothing more specific can be said. After all, consider whatever important decidable program that you're interested in. Write a program in your favorite Turing-complete language to solve it. Since the problem is decidable, your program will halt on all inputs. (Arguably, a ...


16

All of the following comments are premised on the choice of a standard implementation strategy using closures to represent function values and a call-by-value evaluation order: For the pure lambda calculus, garbage collection is not necessary. This is because it is not possible to form cycles in the heap: every newly-allocated value can only contain ...


16

You may wish to look at cost semantics for functional languages. These are various computational complexity measures for functional languages that do not pass through any kind of Turing machine, RAM machine, etc. A good place to start looking is this Lambda the Ultimate post, which has some good further references. Section 7.4 of Bob Harper's Practical ...


15

You might want to check out Liquid Haskell, which allow working with type refinements rather than dependent types. Type refinements can be seen as a restricted logical language that allow you to express Hoare-style properties of the inhabitants of various datatypes. Another possible candidate is the $F^*$ language, which offers similar constructs. There ...


14

The formulas are formulas of Abadi-Plotkin logic, which they describe in their paper A Logic for Parametric Polymorphism. The semantics of System F that Abadi and Plotkin used to interpret their logic can be found in Bainbridge, Freyd, Scedrov, Scott's paper Functorial Polymorphism.


14

At the request of Andrej and PhD, I am turning my comment into an answer, with apologies for self-advertising. I recently wrote a paper in which I look at how to prove the Cook-Levin theorem ($\mathsf{NP}$-completeness of SAT) using a functional language (a variant of the λ-calculus) instead of Turing machines. A summary: the key notion is that of affine ...


13

A zipper, in general, is a data structure with a hole in it. Zippers are used for traversing/manipulating data structures, and the hole corresponds to the current focus of the traversal. Typically there is also an element of the data structure under consideration, so that one has a (list) zipper and a list or a (tree) zipper and a tree. The zipper allows the ...


13

As I said in my comment, the answer in general is no. The important point to understand (I say this for Viclib, who seems to be learning about these things) is that having a programming language/set of machines in which all programs/computations terminate by no means implies that function equality (i.e., whether two programs/machines compute the same ...


13

Honda and Yoshida's A Compositional Program Logic for Polymorphic Higher-Order Functions (probably) pioneered Hoare logics for purely functional languages. This work is based on Hennessy-Milner logic and Milner's encoding of functions into processes, as described here: From Process Logic to Program Logic The work by Régis-Gianas et al mentioned in ...


12

Is it possible to make a "smart" trampoline function that takes two forms of a function, a trampolined version and a non-trampolined version, and chooses (or predicts) the most efficient strategy?* Yes, it's possible to do things like this, but if you control the compiler, it's usually faster and easier to do something else. The main exception is when you ...


12

You can think of $\lambda$-abstraction as an operator $\Lambda$ which takes a function from terms to terms into a term: $$\Lambda : (\mathsf{Term} \to \mathsf{Term}) \to \mathsf{Term}.$$ The type of $\Lambda$ is higher-order because it maps functions to objects, so it is a functional of rank 2. This is where the name comes from. For example, if $\mathsf{id}$...


12

The original paper by Church and Rosser, "Some Properties of Conversion," describes something that may be an example of what you're looking for. If you use the strict lambda calculus, where in every occurrence of $\lambda x.M$ you have that $x$ appears free in $M$, then without a type system the following property holds (it's Theorem 2 in Church and Rosser'...


11

Here is a proof that this is not a research question. It can be solved by a machine: Welcome to Djinn version 2011-07-23. Type :h to get help. Djinn> f ? (a, Either b c) -> Either (a,b) (a,c) f :: (a, Either b c) -> Either (a, b) (a, c) f (a, b) = case b of Left c -> Left (a, c) Right d -> Right (a, d)


11

A semantics of a program is a model of its behavior which, like any scientific model, ignores aspects that you don't want to study. An extremely detailed model of the execution of a program would model the physical behavior of the computer that executes it, including the execution time, power consumption, electromagnetic radiation, etc. Such aspects are ...


11

See also Yann Régis-Gianas PhD thesis work with François Pottier: A Hoare Logic for Call-by-Value Functional Programs (MPC'08). This work was extended to cover the usual ML side-effects by Johannes Kanig and Jean-Cristophe Filliatre in 2009: Who: A Verifier for Effectful Higher-order Programs.


10

Here's a fun one, by Neil Jones and Nina Bohr: Call-by-value Termination in the Untyped $\lambda$-calculus It shows how to apply the size-change analysis (a type of control flow analysis that detects infinite loops) on untyped $\lambda$-terms. This is quite nice in practice, but of course is restricted to $\lambda$-terms without defined constants (though ...


10

You're quite right that the "queue = two lists" approaches don't give you the running time you want when you have the ability to re-use earlier versions. To get O(1) running time (amortized or worst case), you need a way to reverse the rear list and append it to the front list incrementally. Instead of doing the reverse&append all at once, taking O(N) ...


10

The two papers to look at it are Benton, Bierman and de Paiva's Computational Types from a Logical Perspective, which directly gives a proof theory for Moggi's computational lambda-calculus; and Rowan Davies and Frank Pfenning's A Judgmental Reconstruction of Modal Logic, which gives a constructive proof theory for S4 modal logic with box and diamond, and ...


9

Speaking only to the relationship between FRP and SAC: My froc library (see http://jaked.github.com/froc) implements a form of FRP directly on top of SAC; froc behaviors are exactly SAC changeables, and froc events are SAC changeables which take on "instantaneous" values (i.e. for only one SAC update cycle). More details on how this works at http://...


9

I essentially agree with Dave's comment: these are lots of different things (and I only feel remotely competent to talk about three of them). However, from the perspective of a consumer of functional programming research, the three things I know something about probably feel related, because they all are ways of making functional programs deal with inputs ...


9

One of the very first applications of category theory to a subject outside of algebraic geometry was to parsing! The keywords you want to guide your search are "Lambek calculus" and "categorial grammar". In modern terms, Joachim Lambek invented noncommutative linear logic in order to model sentence structure. The basic idea is that you can give basic parts ...


9

I think that the type system you want is elementary affine logic with fixpoints. A distinctive feature (actually, the distinctive feature) of light logics, including elementary linear/affine logic, is that types do not ensure termination: unlike usual logical system, cut-elimination follows from a structural property of proofs (namely, stratification), the ...


9

For question 1, the answer is no, and is no for almost any type discipline (except certain intersection types): the fact that a term is (strongly or weakly) normalizable does not imply in general that it is typable. Typability implies termination, not the other way around. The specific case of of $\lambda EA$, however, brings up another issue which may be ...


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