# Tag Info

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

You should be more precise. When you say that f(x), f a and m >>= f are "the same", ...
• 31k
Accepted

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 ...
• 2,737
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 ...
• 12.1k

### 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 ...
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 ...
• 22.6k

### 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 ...
• 296
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 ...
• 29.9k

### 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: ...
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 ...
• 29.9k
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 ...
• 2,202
Accepted

• 14.6k
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 ...
• 14.6k
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....
• 190
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 ...
• 31k
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 ...
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 ...
• 29.9k

• 163k
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$ ...
• 12.1k
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 ...
• 8,252
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-...
• 280

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

### 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 ...
• 14.6k
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". (...
• 276
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 ...
• 14.6k
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 ...
• 360