Hot answers tagged

50 votes
Accepted

What functions can System F not compute?

System $F$ is quite expressive. As proved by Girard here, the functions of type $\mathbb{N}\rightarrow\mathbb{N}$ (where $\mathbb{N}$ is defined to be $\forall X.\ X\rightarrow (X\rightarrow X)\...
user avatar
  • 13.2k
20 votes

Why do functional programming languages require garbage collection?

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 ...
user avatar
15 votes

Are there any annotated formal verification systems for pure functional programming languages?

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 ...
user avatar
  • 13.2k
13 votes
Accepted

Are there any annotated formal verification systems for pure functional programming languages?

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 ...
user avatar
12 votes
Accepted

A bicartesian closed category of strict complete partial orders (Hask)

Yes, it's impossible to have a nondegenerate CCC with general recursion and categorical coproducts. The standard reference for this is: H. Huwig and A. Poigne. A note on inconsistencies caused by ...
user avatar
11 votes

Are there any annotated formal verification systems for pure functional programming languages?

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 ...
user avatar
  • 1,910
11 votes

What functions can System F not compute?

It is somewhat misleading to say that Haskell's typing system is "the hinley-milner type system". Haskell's types are much more powerful, including, among others, higher-kinded types. Indeed the ...
user avatar
9 votes

How to implement a functional programming language efficiently?

It's not entirely clear what do you mean by a functional programming language without closures. Can you give an example? Functional programming languages are usually based on lambda calculus, whose ...
user avatar
  • 2,471
9 votes
Accepted

Explaining monad transformers in categorical terms

According to Oleksandr Manzuk, they are "translation of a monad along an adjunction", see "Calculating Monad Transformers with Category Theory". By the way, that's the third hit on Google for "monad ...
user avatar
  • 26.7k
8 votes

Are there any annotated formal verification systems for pure functional programming languages?

There is a paper in this year's ICFP, refinement types for Haskell. The paper deals with termination checking rather than full Hoare logic, but hopefully that's a start in this direction. The related ...
user avatar
  • 2,637
8 votes

Can programming help one understand constructive mathematics?

Agda is a dependently typed programming language and/or proof assistant for Martin-Löf type theory. Programming in Agda feels very much like programming in Haskell. For example, inductive proofs are ...
user avatar
  • 231
7 votes

Explaining monad transformers in categorical terms

Augmenting Andrej's answer: There is still no widespread agreement on the appropriate interface monad transformers should support in the functional programming context. Haskell's MTL is the de-facto ...
user avatar
  • 2,637
7 votes
Accepted

Isomorphism between algebraic data-types

Spoiler: the types are isomorphic. First let me clarify what might be meant by "isomorphic". Say that two datatypes $S$ and $T$ are isomorphic if there are maps $f : S \to T$ and $g : T \to S$ such ...
user avatar
  • 26.7k
6 votes
Accepted

What are values relative to Hask?

At the level of precision used in the nlab page, values are global elements -- i.e., a value of type $A$ corresponds to a morphism $1 \to A$. If you want to be serious about this, there are some ...
user avatar
5 votes

Isomorphism between algebraic data-types

A useful technique is to find a property $P$ that is preserved by isomorphism, that is if $X\cong Y$ then $P(X)=P(Y)$. Then if we can show that $P(X)\neq P(Y)$ then also $X\not\cong Y$. In your case, ...
user avatar
  • 2,471
4 votes
Accepted

Is the topsort from "Structuring Depth-First Search Algorithms" guaranteed to be (reverse) stable?

Stripping the Haskell encryption from your question (and ignoring why you are using dff instead of dfs to get a search that respects a given order), you appear to be asking about the stability of the ...
user avatar
3 votes
Accepted

Uncountability in intuitionistic logic

I tried to address the questions you raise in "Five stages of accepting constructive mathematics". And here are some textbooks: Constructive analysis by D. Bridges and E. Bishop is the &...
user avatar
  • 26.7k
3 votes
Accepted

Practical implementation of Hindley–Milner with typeclasses — matching vs most general unifier

Ok, so I figured it out the next day. It's all dead simple as it came out. Let's use an example – type applications z a a and ...
user avatar
  • 211
2 votes

Can programming help one understand constructive mathematics?

Maybe take a look at the textbook Software Foundations, which uses the proof assistant Coq. I don't think the focus is really on "learning constructive math", but it does develop the programming tools....
user avatar
  • 7,090
2 votes

Uncountability in intuitionistic logic

I can't give you a (easily translatable) answer to the question regarding Haskell and the types, but the following might help you since you already mentioned ZFC: Take the axioms of ZFC and let's ...
user avatar
  • 25
2 votes

Areas of research and open problems in functional programming

The computational implications of homotopy type theory & higher type theory. Homotopy type theory was invented and developed by a group of computer scientists and mathematicians as a new ...
user avatar
  • 1,125
1 vote
Accepted

Why can't opaque optics form a category?

optics do form a category where the objects are (Type, Type). However, the Optic type is ...
user avatar
1 vote
Accepted

Are the `ArrowApply` and `Monad` typeclasses equivalent?

The problem with your counterexample is that the type you presented is not a valid instance of ArrowApply as far as I can tell. You didn't present what the ...
user avatar
  • 1,474
1 vote

Are there any annotated formal verification systems for pure functional programming languages?

Our work on soft verification of contracts is related, at OOPSLA 2012 and ICFP 2014, allows you to write contracts, which are a lot like ACSL specs, and then either statically verify them or use them ...
user avatar
1 vote

Explaining monad transformers in categorical terms

I would highly recommend the book book by Bartosz Milewski "Category Theory for Programmers" which goes into some detail about Monads from a Category Theoretic perpective. And it's also ...
user avatar

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