Tag Info

Accepted

• 2,471
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
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
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

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

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

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