Skip to main content
Dan Doel's user avatar
Dan Doel's user avatar
Dan Doel's user avatar
Dan Doel
  • Member for 5 years, 9 months
  • Last seen this week
  • Boston, MA, USA
15 votes
Accepted

Monad in Haskell programming vs. Monad in category theory

13 votes
Accepted

What does canonicity property mean in Type Theory?

8 votes

Curry-Howard isomorphism and non-constructive logic

7 votes
Accepted

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

7 votes
Accepted

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

6 votes
Accepted

Are Bad churches inhabited?

6 votes

What are the implications of Homotopy Type Theory?

5 votes

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

5 votes

How exactly do we define parametric polymorphism?

5 votes
Accepted

Stablishing termination of the construction of infinite stream with ranking functions

5 votes
Accepted

Relationship between Higher Kinded Polymorphism, type inference, and Currying

5 votes

Can a total programming language be Turing-complete?

4 votes
Accepted

Example of Dependent Types?

4 votes
Accepted

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

4 votes
Accepted

Why use the Y combinator for recursion?

4 votes
Accepted

Proving transitivity in an intuitionistic type theory without the K rule

4 votes
Accepted

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

4 votes

liskov substitution principle seems to have two conventional meanings

4 votes
Accepted

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

4 votes
Accepted

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

4 votes
Accepted

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

4 votes

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

4 votes

Are "logarithm types" a thing?

4 votes
Accepted

Greatest fixpoint of the type of lists

3 votes

What is an uninhabited type?

3 votes

When is cumulative type universes useful?

3 votes

Generalization of Functors to other datatypes?

3 votes

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

3 votes
Accepted

Differences between Church and Scott encoding

3 votes
Accepted

Proving intuitionistic tautologies in Agda