The tag has no usage guidance.

18 questions
Filter by
Sorted by
Tagged with
2k views

### What functions can System F not compute?

In this wikipedia article on Turing Completeness it states that: The untyped lambda calculus is Turing complete, but many typed lambda calculi, including System F, are not. The value of typed ...
2k views

### Are there any annotated formal verification systems for pure functional programming languages?

ACSL (Ansi C Specification Language), is a specification for C code, annotated with special comments, that allows C code to be formally verified. I have not looked into it, but I imagine that the ...
2k views

### Why do functional programming languages require garbage collection?

What's stopping ghc from translating Haskell into a concatenative programming language such as combinatory logic and then simply using stack allocation for everything? According to Wikipedia, the ...
587 views

### Is eta-equivalence for functions compatiable with Haskell's seq operation?

Lemma: Assuming eta-equivalence we have that (\x -> ⊥) = ⊥ :: A -> B. Proof: ⊥ = (\x -> ⊥ x) by eta-equivalence, and <...
609 views

Following up What’s an example of a Monad which is an Alternative but not a MonadPlus?: Assume $m$ is a monad. What are the relations betweem $m$ being an Alternative, a MonadPlusCatch and a ...
744 views

### Explaining monad transformers in categorical terms

Most resource regarding categorical notions in programming describe monads, but I've never seen a categorical description of monad transformers. How could monad transformers be described in the terms ...
257 views

### A bicartesian closed category of strict complete partial orders (Hask)

It seems to be well-known that programming languages can't have sums, products and nontermination together. Q1. Is this true? Below (or in the above link I gave) is a partial argument. However, ...
781 views

### Practical implementation of Hindley–Milner with typeclasses — matching vs most general unifier

I'm trying to get a deep understanding of a (great) paper "Typing Haskell in Haskell". I'm having difficulties understanding the implementation of two methods there — the ...
236 views

N.B. I asked the same question on Stack Overflow but it was suggested that it is too theoretical for this forum. It is great that Haskell allows us to walk around in the category $Hask$. But ...
284 views

### Isomorphism between algebraic data-types

I have two types of trees in Haskell, defined as the least solution of the following equations: $T_1(A) \cong 1 + A + T_1(A) \times T_1(A)$ $T_2(A) \cong 1 + A \times T_2(A) + T_2(A) \times T_2(A)$ ...
248 views

### Can programming help one understand constructive mathematics?

I have read about the principles of constructive mathematics, for example, the principle of excluded middle is not allowed, and now I want to do some exercises to increase my understanding of the ...
111 views

### What are values relative to Hask?

According to ncatlab's page on category theory and haskell, "we can identify a subset of Haskell called Hask that is often used to identify concepts used in basic category theory. One considers ...
352 views

### Aren't Monads F-Algebra's? And then if that could be said are Comonad's F-Coalgebra's?

So considering a Monad to be a Triple (T:C -> C, η, µ) with eta and mu as the Natural transformations with appropriate signatures, isn't this in essence an F-Algebra? My thinking is that being both (...
190 views

### Type-and-effect systems, stochasticism and effect squelching: how about quicksort?

There's a feature of Haskell's type system which bugs me: you can't implement a randomized sorting algorithm without the use of randomness spilling out into all of its callers. That seems undesirable....
345 views

A distributive law between monads must satisfy laws that are usually given in terms of the units $\eta$ and multiplications $\mu$ of the two monads. Among the four laws there are: \$\mu^S T \circ S l \...
147 views

### Is the topsort from “Structuring Depth-First Search Algorithms” guaranteed to be (reverse) stable?

In "Structuring Depth-First Search Algorithms in Haskell", implemented in Data.Graph in the Haskell standard library, an algorithm for topologically sorting graphs is given: ...