User Petr

48 votes

2 answers

6k views

Explaining Applicative functor in categorical terms - monoidal functors

asked Aug 27, 2012 at 7:57

22 votes

3 answers

3k views

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

asked Jan 27, 2013 at 9:26

19 votes

2 answers

1k views

A mathematical (categorical) description of type classes

asked Sep 6, 2012 at 15:58

18 votes

2 answers

821 views

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

asked Oct 31, 2012 at 17:23

16 votes

2 answers

481 views

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

asked Oct 27, 2012 at 8:54

12 votes

2 answers

780 views

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

asked Oct 31, 2012 at 8:32

11 votes

4 answers

1k views

Explaining monad transformers in categorical terms

asked Sep 17, 2014 at 8:37

10 votes

1 answer

486 views

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

asked Sep 6, 2012 at 15:15

10 votes

1 answer

629 views

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

asked Nov 18, 2012 at 16:56

8 votes

1 answer

528 views

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

asked Aug 14, 2015 at 14:10

6 votes

1 answer

344 views

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

asked Nov 12, 2012 at 17:44

3 votes

1 answer

301 views

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

asked Apr 3, 2015 at 12:14

3 votes

2 answers

303 views

Languages that lack contraction, weakening or exchange

asked Aug 5, 2017 at 17:39

Stack Exchange Network

13 Questions

Explaining Applicative functor in categorical terms - monoidal functors

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

A mathematical (categorical) description of type classes

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

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

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

Explaining monad transformers in categorical terms

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

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

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

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

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

Languages that lack contraction, weakening or exchange