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)\...
- 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 ...
- 31.7k
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 ...
- 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 ...
- 10.3k
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 ...
- 31.7k
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 ...
- 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 ...
- 10.3k
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 ...
- 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 ...
- 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 ...
- 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 ...
- 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 ...
- 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 ...
- 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 ...
- 31.7k
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, ...
- 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 ...
- 50.3k
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 &...
- 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 ...
- 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....
- 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 ...
- 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 ...
- 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 ...
- 26
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 ...
- 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 ...
- 1,887
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 ...
- 111
Only top scored, non community-wiki answers of a minimum length are eligible