The tag has no wiki summary.

learn more… | top users | synonyms

0
votes
0answers
33 views

Does the Y Combinator Contradict the Haskell-Howard Correspondence? [migrated]

The Y combinator has the type $(a \rightarrow a) \rightarrow a$. By the Haskell-Howard Correspondence, because the type $(a \rightarrow a) \rightarrow a$ is inhabited, it must correspond to a true ...
3
votes
2answers
121 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 ...
23
votes
5answers
944 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 ...
5
votes
2answers
135 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 ...
3
votes
0answers
139 views

Generalizing Haskell: could we replace Hask with Cat?

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 ...
5
votes
1answer
99 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 ...
3
votes
2answers
128 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)$ ...
12
votes
4answers
276 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 ...
3
votes
1answer
200 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 ...
4
votes
0answers
158 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 ...
7
votes
2answers
215 views

What are the relations between Alternative, MonadPlus(LeftCatch) and MonadPlus(LeftDistributive)?

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