46

In their basic form, type classes are somewhat similar to object interfaces. However, in many respects, they are much more general. Dispatch is on types, not values. No value is required to perform it. For example, it is possible to do dispatch on the result type of function, as with Haskell's Read class: class Read a where readsPrec :: Int -> String -...


40

A type $C$ has a logarithm to base $X$ of $P$ exactly when $C \cong P\to X$. That is, $C$ can be seen as a container of $X$ elements in positions given by $P$. Indeed, it's a matter of asking to what power $P$ we must raise $X$ to obtain $C$. It makes sense to work with $\mathop{log}F$ where $F$ is a functor, whenever the logarithm exists, meaning $\mathop{...


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


28

Software Foundations by Benjamin C. Pierce would be a good place to start. It would be a make a good precursor to his Types and Programming Languages. There is also Simon Thompson's Type Theory and Functional Programming and Girard's Proofs and Types.


25

As it happens, I'm writing a paper about this now. IMO, a good way to think about futures or promises is in terms of the Curry-Howard correspondence for temporal logic. Basically, the idea behind futures is that it is a data structure representing a computation that is in progress, and upon which you can synchronize. In terms of temporal logic, this is the ...


23

Yes, it is. Here's how you do it: You can compile basically any program you like to circuits. See for instance the work of Dan Ghica and his collaborators on the Geometry of Synthesis, which shows how to compile programs into circuits. Dan R. Ghica. Geometry of Synthesis: A structured approach to VLSI design Dan R. Ghica, Alex Smith. Geometry of Synthesis ...


23

I think the overall goal of PL theory is to lower the cost of large-scale programming by way of improving programming languages and the techincal ecosystem wherein languages are used. Here are some high-level, somewhat vague descriptions of PL research areas that have received sustained attention, and will probably continue to do so for a while. Most ...


22

There are several senses of "expressiveness" that you might want for a type system. What mathematical functions can you express in a particular type system. For example, in the simply typed lambda calculus, not all computable functions can be expressed. The same is true of System $F$, but strictly more functions can be expressed. This is not very ...


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


21

Algebraic data types let you define types recursively. Concretely, suppose we have the datatype $$ \mathsf{data\;list = Nil \;\;|\;\; Cons\;of\;\mathbb{N} \times list} $$ What this means is that $\mathsf{list}$ is the smallest set generated by the $\mathsf{Nil}$ and $\mathsf{Cons}$ operators. We can formalize this by defining the operator $F(X)$ $$ ...


21

The short answer is no. The long answer is that such languages are invented on a regular basis, but if they see any significant degree of use, for good semantic reasons they never remain in this mode for very long. The basic problem is that it is very difficult to build programs compositionally using state machines. The modular construction of programs ...


20

A recent developpement on this topic: U. dal Lago and B. Accatoli proved that the length of the leftmost-outermost reduction (LOr) of a $\lambda$-term is an invariant (time) cost model for $\lambda$-calculus. They show that Turing machines (with cost=time) and $\lambda$-terms (with cost=length of the LOr) can simulate each other with a polynomial overhead ...


20

I have an answer to this question which is possibly novel. In fact, I am still thinking through it for the last 6 months or so, and it hasn't been written about in papers yet. The general thesis is that relational reasoning principles like "logical relations", "simulations", and even "invariants" are manifestations of data abstraction or information hiding....


20

Two times no. First, most HPLs are not context free. While they usually have syntax based on a CFG, they also have what people call static semantics (which is also often included in the term syntax). This can include names and types which have to check out for a correct program. For instance, class A { String a = "a"; int b = a + d; } is a ...


20

Parsing perl is un-decidable. http://www.jeffreykegler.com/Home/perl-and-undecidability/perl-and-undecidability-files/TPR3.pdf?attredirects=0 http://www.perlmonks.org/?node_id=663393


20

What you want exists, and is an enormous area of research: it's the entire theory of programming languages. Loosely speaking, you can view computation in two ways. You can think of machines, or you can think of languages. A machine is basically some kind of finite control augmented with some (possibly unbounded) memory. This is why introductory TOC ...


19

Consider algebraic datatypes such as: data List a = Nil | Cons a (List a) The return types of each constructor in a datatype are all the same: Nil and Cons both return List a. If we allow the constructors to return different types, we have a GADT: data Empty -- this is an empty data declaration; Empty has no constructors data NonEmpty data NullableList a ...


19

About a decade ago, Ene and Muntean showed that broadcasting has no reasonable compositional encoding into the $\pi$-calculus [1]. The essence of their separation between point-to-point communication and message passing is easy to understand: point-to-point is "too asynchronous". That means that in a broadcasting system, a broadcasting sender can send to $n$ ...


18

Q1: There are many notions of program equivalence (trace equivalence, contextual equivalence, observational equivalence, bisimilarity) which may or may not take into account things such as time, resource usage, nondeterminism, termination. A lot of work has been done on finding usable notions of program equivalence. For example: Operationally-Based Theories ...


18

Benjamin Werner has proved the mutual interpretability of ZFC with countably many inaccessibles and the Calculus of Inductive Constructions, in his paper Sets in Types, Types in Sets. This means, roughly, that any function which can be shown to be total in ZFC with countably many inaccessibles can be defined in Coq. So unless you are a set theorist ...


18

[I haven't thought deeply about the issues of object-oriented type systems, but I will say what I know to get the discussion going.] We say that $A$ is a subtype of $B$ if all $A$-typed values can be used in every context where $B$-typed values are expected. Or, to put another way, $A$-typed values can "masquerade" as $B$-typed values. If such ...


18

"Meaning" is used in a broader way than denotation is. The original dichotomy, inherited from logic and philosophy, is between "sense" and "denotation" (which philosophers call "reference"). This distinction can be illustrated by Frege's original example. He noted that phrases "the morning star" and "the evening star" referred to the same object --- the ...


18

Roughly speaking, there are two main strategies for safe manual memory management. The first approach is to use some substructural logic like linear logic to control resource usage. This idea has floated around basically since linear logic's inception, and basically works on the observation that by banning the structural rule of contraction, every variable ...


17

First, you should know that, in general, there is not consensus about these terms and their definitions depend on the system in which one is working.Since you asked about intuitionist type theory, I'll quote Pfenning: A judgment is something we may know, that is, an object of knowledge. A judgment is evident if we in fact know it. Propositions on the ...


16

I am happy with Adrej's answer, but I would like to drill down further. To start with, denotational semantics wants to say something like "the meaning of this notation is that". A real semanticist would want to imagine that the meanings are what exist in our mind and the notations are just a way of expressing those meanings. The requirement that ...


16

I would divide the books on programming language semantics into two classes: those that focus on modelling programming language concepts and those that focus on the foundational aspects of semantics. There is no reason a book can't do both. But, usually, there is only so much you can put into a book, and the authors also have their own predispositions ...


16

If you only think of Booleans as 0 and 1, then it is natural to include them as subtypes of natural numbers and integers. But as soon as you start applying operations to them, then things start to fall apart. Consider what happens when you define the + operation on Booleans. You have two choices: Make + the same as OR, so 1+1=1. But then you have the ...


16

Perhaps I can try giving a less metaphysical answer. There is a language, a logical language, that we are studying. In this language, there are things called "propositions" which are supposed to be things that are true or false. There is a meta-language, which is also a logical language, in which we are trying to explain which things in the base language ...


16

"Resumable exceptions" are indeed a well-known idea in some programming language circles. In particular, Common Lisp has had resumable exceptions for a long time (so they are really not confined to research language; Common Lisp could be considered "mainstream", it has been widely available and relatively widely used for a long time). For a discussion of ...


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


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