48
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)\rightarrow X$) are exactly the definable functions ($\mathbb{N}\rightarrow\mathbb{N}$) in second order Heyting Arithmetic $\mathrm{HA}_2$. Note that this is the same ...
19
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 ...
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 ...
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 ...
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.
11
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 fixpoints in a cartesian closed category. Theoretical Computer Science, 73:101–112, 1990.
However, I and (most of the other people I've met) learned about it ...
11
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 typing system is so powerful that you can embed Turing-complete programming languages in the typing system, see here. This is not the only reason for Haskell's power,...
9
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 essential part is that you can have open lambda terms. For example the term for the constant function (the K-combinator) $\lambda x . \lambda y . x$ can be ...
8
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 transformer categorically". The first is a Stackoverflow question about this and the second is your question.
8
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 written as recursive functions with multiple equations that pattern match on the function arguments. So programming and/or proving in Agda is a good way to learn ...
8
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 work section in that paper contains some pointers, such as Xu, Peyton-Jones, and Claessen's static contract checking for Haskell, and Sonnex, Drossopoulou, and ...
7
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 interface, but Jaskelioff's Monatron is an alternative.
One of the earlier technical reports by Moggi, an abstract view of programming languages, discusses ...
7
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 that $f(g(v)) = v$ for every value $v : T$ and $g(f(u)) = u$ for every value $u : U$.
Let us fix a type $A$. We can then write your equations without the ...
6
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 technicalities to account for:
First, actual Haskell does not actually form a category in the sense that we would hope -- the seq operator breaks a lot of the ...
6
First, let us be explicit about how seq distinguishes $\bot$ from $\lambda x . \bot$:
bottom :: a
bottom = bottom
eta :: a -> b
eta x = bottom
-- This terminates
fortytwo = seq eta 42
-- This does not terminate
infinity = seq bottom 42
It is therefore an experimental fact that in Haskell $\bot$ and $\lambda x . \bot$ are operationally distinguishable....
5
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, let's pick $P(X)$ to be $X(\bot)$ is isomorphic to 1 where $\bot$ is the empty data type. Clearly, $P$ is preserved by isomorphisms. Now
$T_1(\bot) \cong 1 + \...
5
The paper with a rather suggestive title "Algebras, Coalgebras, Monads and Comonads" (2001)
by Neil Ghani, Christoph Lüth, Federico De Marchi, John Power addresses this topic.
4
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 topological sorting algorithm that performs a depth first search and reverses a postorder traversal of the depth-first spanning forest. However, there is a more ...
3
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 "bible" of constructive mathematics.
Varieties of constructive mathematics by D. Bridges and F. Richman considers several varieties of constructive ...
3
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 z a b where z :: * -> * -> *. The unification will yield that (without further context) z a a is the most general type for both giving substitution {b↦a}. On the other hand, z a a cannot be matched to z a b, as they are simply ...
2
Note that the specification for seq which you quote is not its definition.
To quote the Haskell report "The function seq is defined by the equations: [and then the equations you give]".
The suggested argument seems to be that seq would be uncomputable if seq (\x -> ⊥) b = ⊥.
Such behaviour would violate the specification of seq.
Importantly, since ...
2
Proving that λ x. Ω ≠ Ω in is one of the goals Abramsky sets for his lazy lambda calculus theory (page 2 of his paper, already cited by Uday Reddy), because they are both in weak head normal form. As of definition 2.7, he discusses explicitly that eta-reduction λ x. M x → M is not generally valid, but it is possible if M terminates in every environment. ...
2
I am not sure if the Haskell report defines the semantics rigorously enough to settle the question about what $\lambda x.\, \bot$ should mean. However, it is common experience in Haskell as well as all other lazy functional languages, that, if you ask them to evaluate a term that represents $\lambda x.\, \bot$, the evaluation terminates. The "As a ...
2
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. On the other end of the spectrum is the Homotopy Type Theory Book, which is very theoretical about constructive math, but doesn't include programming per se (...
2
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 assume that ZFC is consistent. By the Löwenheim-Skolem Theorem Downwards (as a corollary to the Completeness Theorem for First-Order Predicate Logic) there is a ...
2
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 foundation of mathematics, and as a language to formalize math in, specifically with a view towards algebraic topology (& related fields). However, not much ...
1
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 implementation of app but the only one I could come up with (where you use the input stream function once and then discard it) doesn't satisfy the 2nd and 3rd ArrowApply laws.
What definition of app did ...
1
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 a dynamic checks at runtime.
Only top voted, non community-wiki answers of a minimum length are eligible
