17 votes
Accepted

Strictness in both arguments but not in each individually

That's a very good question! It turns out the answer is both yes and no. A classic example of a function we'd like to write is Plotkin's parallel or. We know from basic boolean logic that both ...
Gilles 'SO- stop being evil''s user avatar
16 votes
Accepted

“Left identity” of Monad laws in Haskell is wrong

You should be more precise. When you say that f(x), f a and m >>= f are "the same", ...
Andrej Bauer's user avatar
  • 30.4k
15 votes
Accepted

Monad in Haskell programming vs. Monad in category theory

A monad in Haskell is intended to be a monad on the category of types, when the category theory is done internally to the type theory. The capabilities of Haskell and similar languages are somewhat ...
Dan Doel's user avatar
  • 2,688
13 votes
Accepted

Is the IO monad technically incorrect?

This is a suggested "interpretation" of the IO monad. If you want to take this "interpretation" seriously, then you need to take "RealWorld" seriously. It's ...
Derek Elkins left SE's user avatar
13 votes

Rigorous proof that parametric polymorphism implies naturality using parametricity?

The missing part is the "identity extension lemma", which is mentioned in Reynolds' original paper but not in Wadler's. For $F : \text{Type} \to \text{Type}$, this says that if the ...
András Kovács's user avatar
11 votes
Accepted

Are there any type constructors which are *not* functors?

One obvious counterexample is a binary search tree. You cannot freely substitute the values in a binary search tree because a substitution might change the ordering (relative to ...
Pseudonym's user avatar
  • 22.1k
10 votes

What exactly is the relation between Haskell and category theory?

Category theory is an abstract branch of mathematics and you do not need to learn it before you start writing Haskell code. Similarly, you do not need to learn Haskell before you start learning ...
axr's user avatar
  • 296
8 votes
Accepted

For every imperative function, is there a functional counterpart with identical performance or even instructions?

Performance is not a property of language, it is a property of specific programs within a language. Some languages might be very fast at some things and slow at others. For example, Chez-Scheme can ...
Joey Eremondi's user avatar
7 votes

Prove foldl fusion law

Let me try to answer your question, I may be mistaken, so check it out first: Let's first state the definition of foldl: ...
Teodoro Freund's user avatar
7 votes
Accepted

Implementing mathematical theory of arithmetic in Haskell via Curry-Howard correspondence

Proofs in Haskell? Okay, first let's talk about the Curry-Howard correspondence. This says that one can view theorems as types and proofs as programs. However, it says nothing about which specific ...
Joey Eremondi's user avatar
7 votes
Accepted

Curry-Howard, void, and type checking in Haskell

I would find a different tutorial because the author of that one is fundamentally confused. They wrongly claim that $\neg a$ and $\bot\to a$ are equivalent ($a\to\bot$ would be correct), and also ...
benrg's user avatar
  • 2,112
6 votes
Accepted

How should I describe the relationships between type expressions?

The set-theoretic intuitions can make sense in the semantics, especially in the context of realizability semantics (where types are interpreted as sets of terms). In this case, the polymorphic type $\...
Rodolphe Lepigre's user avatar
6 votes
Accepted

In Hindley-Milner system, how can I prove that let id=\x.x in id id is well-typed?

If I understand you question correctly, you are wondering how the typing judgment $f : \forall \alpha. \alpha \to \alpha \vdash f\;f : \beta$ can be proved, where $\beta$ is some (yet unknown) type. ...
Rodolphe Lepigre's user avatar
6 votes
Accepted

How to model conditionals with first-class functions?

The usual encoding of booleans, due to Church, is $$ {\sf true} = \lambda x. \lambda y. x \qquad {\sf false} = \lambda x. \lambda y. y $$ Roughly, "true" is the function which takes two arguments $x,...
chi's user avatar
  • 14.6k
6 votes
Accepted

Can we define a program by means of a walk of a graph induced by the category of types?

Consider the simply-typed $\lambda$ calculus: this is one of the simplest functional languages you can define. It is very common to interpret it in a Cartesian closed category (CCC). Indeed, CCCs are ...
chi's user avatar
  • 14.6k
5 votes
Accepted

How does Bifunctor in Haskell work?

A Haskell type class defines a set of functions (sometimes called methods) that belong to the type class. In most cases, specific instances must supply specific implementations of one or more of these....
Mark Seemann's user avatar
5 votes
Accepted

Can this set of propositions be represented and proved in Haskell?

Your Haskell encoding fails to capture proofs in propositional calculus (which is what the book you referred to does). The failure is not due to your using Haskell, but because of your encoding ...
Andrej Bauer's user avatar
  • 30.4k
5 votes
Accepted

Relating a proof to a Haskell program

Your goal is to “prove” --I'm using bullets “•” for syntactic separators-- $$ ∀x \;•\;\; ∃y \;•\;\; y² ≤ x < (y+1)²$$ Proof Methods In the natural deduction style, one proves “∀ x : ℕ • P x” by ...
Musa Al-hassy's user avatar
5 votes
Accepted

Can Haskell ensure a Functor (or other typeclasses) satisfies its law?

So, while this question seems Haskell specific at first glance, I think it touches on enough aspects of modern Programming Languages theory and research that there's a good CS-general answer here. As ...
Joey Eremondi's user avatar
5 votes

Can we define a program by means of a walk of a graph induced by the category of types?

Your question sounds redundant to me. By definition of category whenever two morphisms with common object $f\colon A \rightarrow B$ and $g\colon B \rightarrow C$ exist, then their composition $g\circ ...
Apiwat Chantawibul's user avatar
4 votes

Unclear logic notation for PFX program rules

The "fraction"-style notation is an inference rule in natural deduction style. See What is this fraction-like "discrete mathematics"–style notation used for formal rules?. $v_1,\dots,v_n\...
D.W.'s user avatar
  • 159k
4 votes
Accepted

How to explain/understand brackets of applicative functor [[f u1... un]]?

In it's simplest, original form, $[\![f\ x \ y]\!]$ just means $\eta(f)\circledast x \circledast y$ where $\circledast$ is what Haskell calls <*> and $\eta$ ...
Derek Elkins left SE's user avatar
4 votes
Accepted

When does a type generalise another type?

A pretty easy way to see if $t$ generalizes $u$ if $u$ matches $t$: replace all variables in $u$ by (fresh) constants, written $u_c$, and check if $u_c$ unifies with $t$. If so, then there is a ...
cody's user avatar
  • 8,204
4 votes
Accepted

Haskell type class and initial algebra

tl;dr: we can show that they are in fact isomorphic. Defining two different instances over them does not make them different. Defining two different functions over two types does not make them non-...
Mario Román's user avatar
4 votes

In Hindley-Milner system, how can I prove that let id=\x.x in id id is well-typed?

As a starting note, the rules are syntax-directed: there's only one rule for each language construct. This means that you can construct the typing proof from the bottom up, by always using the rule ...
Gilles 'SO- stop being evil''s user avatar
4 votes

Is Pattern Matching as expressive as Case Expression in Haskell?

The expression case e of p1 -> e1 p2 -> e2 ... can be rewritten as let k p1 = e1 k p2 = e2 ... in k e ...
chi's user avatar
  • 14.6k
4 votes
Accepted

Why does higher-order abstract syntax need an inverse to define catamorphisms?

By being corecursive between the types, you indeed get a representation of a grammar, and it does have binding. But now you've sort of "baked in" the unembedding by making it "definitionally id". (...
sclv's user avatar
  • 276
3 votes
Accepted

Typing rule for binding groups

I don't know what rule Jones intended to use, but I'd guess it's something like $$ \dfrac{ \Gamma' = \Gamma,x_1:\tau_1,\ldots,x_n:\tau_n \\ \Gamma' \vdash e_1 : \tau_1 \\ \cdots \\ \Gamma' \vdash e_n ...
chi's user avatar
  • 14.6k
3 votes
Accepted

How does the function to curry and uncurrying another function work?

The meaning of curry can be easier to be seen when the type signature is written as ...
siracusa's user avatar
  • 360
3 votes

Curry Howard correspondence to Predicate Logic?

To explain why I'm uncomfortable with Newsham's and (especially) Piponi's data wrappers ... (This is going to be more question than answer, but perhaps it'll work ...
AntC's user avatar
  • 487

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