User Dan Doel

15 votes

Accepted

Monad in Haskell programming vs. Monad in category theory

answered Nov 2, 2020 at 1:55

13 votes

Accepted

What does canonicity property mean in Type Theory?

answered Aug 22, 2019 at 1:53

7 votes

Accepted

How to prove that the Church encoding, forall r. (F r -> r) -> r, gives an initial algebra of the functor F?

answered Nov 4, 2020 at 4:51

7 votes

Accepted

Flawed argument in the proof of function extensionality in cubical type theory?

answered Sep 8, 2018 at 23:55

7 votes

Curry-Howard isomorphism and non-constructive logic

answered Sep 17 at 23:31

6 votes

Accepted

Are Bad churches inhabited?

answered Oct 13, 2018 at 0:29

6 votes

What are the implications of Homotopy Type Theory?

answered Nov 6, 2020 at 4:29

5 votes

What is the difference between $ \alpha \to \alpha $ vs $ \forall \alpha. \alpha \to \alpha$?

answered Oct 26, 2019 at 16:26

5 votes

How exactly do we define parametric polymorphism?

answered Mar 3, 2019 at 16:51

5 votes

Accepted

Stablishing termination of the construction of infinite stream with ranking functions

answered Sep 11, 2018 at 23:43

5 votes

Accepted

Relationship between Higher Kinded Polymorphism, type inference, and Currying

answered Sep 1, 2018 at 18:43

5 votes

Can a total programming language be Turing-complete?

answered Jun 15, 2022 at 1:34

4 votes

Accepted

Example of Dependent Types?

answered Sep 14, 2020 at 17:59

4 votes

Accepted

What's the difference between Row Polymorphism and Structural Typing?

answered Sep 20, 2020 at 0:03

4 votes

Accepted

Why use the Y combinator for recursion?

answered Feb 24, 2022 at 23:06

4 votes

Accepted

Proving transitivity in an intuitionistic type theory without the K rule

answered May 23, 2022 at 2:16

4 votes

Accepted

How to determine whether a dependent type that doesn't fit the monad instance is categorically a monad

answered Sep 27, 2018 at 5:06

4 votes

liskov substitution principle seems to have two conventional meanings

answered Sep 13, 2018 at 22:13

4 votes

Accepted

Multi-prompt delimited continuations in terms of single-prompt delimited continuations

answered May 7, 2019 at 3:26

4 votes

Accepted

In Agda's GADT, are "parameterized" and "indexed" different semantically?

answered Oct 13, 2018 at 0:48

4 votes

Accepted

Does co-inductive and co-recursive types also have their recursors?

answered Oct 20, 2018 at 15:37

4 votes

What is the adjunct of the evaluation morphism in a closed monodical category?

answered Oct 27, 2019 at 1:38

4 votes

Are "logarithm types" a thing?

answered Dec 1, 2019 at 16:52

4 votes

Accepted

Greatest fixpoint of the type of lists

answered Dec 22, 2020 at 17:18

3 votes

What is an uninhabited type?

answered Jan 11, 2021 at 19:50

3 votes

When is cumulative type universes useful?

answered Feb 9, 2020 at 4:55

3 votes

Generalization of Functors to other datatypes?

answered Apr 6, 2019 at 19:19

3 votes

When do we need U(n+2) to solve a problem that can be formulated in U(n)?

answered Sep 1, 2018 at 13:43

3 votes

Accepted

Differences between Church and Scott encoding

answered Sep 6, 2018 at 12:36

3 votes

Accepted

Proving intuitionistic tautologies in Agda

answered May 19, 2021 at 20:31

Stack Exchange Network

62 Answers

Monad in Haskell programming vs. Monad in category theory

What does canonicity property mean in Type Theory?

How to prove that the Church encoding, forall r. (F r -> r) -> r, gives an initial algebra of the functor F?

Flawed argument in the proof of function extensionality in cubical type theory?

Curry-Howard isomorphism and non-constructive logic

Are Bad churches inhabited?

What are the implications of Homotopy Type Theory?

What is the difference between $ \alpha \to \alpha $ vs $ \forall \alpha. \alpha \to \alpha$?

How exactly do we define parametric polymorphism?

Stablishing termination of the construction of infinite stream with ranking functions

Relationship between Higher Kinded Polymorphism, type inference, and Currying

Can a total programming language be Turing-complete?

Example of Dependent Types?

What's the difference between Row Polymorphism and Structural Typing?

Why use the Y combinator for recursion?

Proving transitivity in an intuitionistic type theory without the K rule

How to determine whether a dependent type that doesn't fit the monad instance is categorically a monad

liskov substitution principle seems to have two conventional meanings

Multi-prompt delimited continuations in terms of single-prompt delimited continuations

In Agda's GADT, are "parameterized" and "indexed" different semantically?

Does co-inductive and co-recursive types also have their recursors?

What is the adjunct of the evaluation morphism in a closed monodical category?

Are "logarithm types" a thing?

Greatest fixpoint of the type of lists

What is an uninhabited type?

When is cumulative type universes useful?

Generalization of Functors to other datatypes?

When do we need U(n+2) to solve a problem that can be formulated in U(n)?

Differences between Church and Scott encoding

Proving intuitionistic tautologies in Agda