user avatar
user avatar
user avatar
Petr
  • Member for 10 years
  • Last seen more than 3 years ago
47 votes
2 answers
6k views

Explaining Applicative functor in categorical terms - monoidal functors

20 votes
3 answers
2k views

Is there a concept of something like co-applicative functors sitting between comonads and functors?

18 votes
2 answers
744 views

Is it possible to decide $\beta$-equivalence within System F (or another normalizing typed λ-calculus)?

16 votes
1 answer
387 views

How to show that a type in a system with dependent types is not inhabited (i.e. formula not provable)?

15 votes
1 answer
1k views

A mathematical (categorical) description of type classes

12 votes
2 answers
725 views

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

10 votes
1 answer
476 views

What are possible implementations of Haskell's type classes and what are their (dis)advantages?

9 votes
1 answer
504 views

A simple proof that decidability of typability in System F ($\lambda 2$) implies decidability of type checking?

9 votes
4 answers
1k views

Explaining monad transformers in categorical terms

6 votes
1 answer
377 views

What is the formal definitions of the reduction related to the "call/cc" (call with the current continuation) operator?

6 votes
1 answer
307 views

In what sense are coroutines dual to (sub)routines?

3 votes
2 answers
262 views

Languages that lack contraction, weakening or exchange

3 votes
1 answer
274 views

What are the morphisms of Adj(C,T) - the category whose objects are the adjunctions of a given monad?