Skip to main content
Petr's user avatar
Petr's user avatar
Petr's user avatar
Petr
  • Member for 11 years, 10 months
  • Last seen more than a month ago
48 votes
2 answers
6k views

Explaining Applicative functor in categorical terms - monoidal functors

22 votes
3 answers
3k views

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

19 votes
2 answers
1k views

A mathematical (categorical) description of type classes

18 votes
2 answers
793 views

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

16 votes
2 answers
465 views

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

12 votes
2 answers
773 views

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

11 votes
4 answers
1k views

Explaining monad transformers in categorical terms

10 votes
1 answer
482 views

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

10 votes
1 answer
612 views

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

8 votes
1 answer
498 views

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

6 votes
1 answer
340 views

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

3 votes
1 answer
300 views

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

3 votes
2 answers
299 views

Languages that lack contraction, weakening or exchange