When I asked this question, one of the answers, now deleted, was suggesting that the type Either corresponds to XOR, rather than OR, in the Curry-Howard correspondence, because it cannot be Left an...

At the end of Category Theory 8.2, Bartosz Milewski shows some examples of the correspondence between logic, category theory, and type systems. I was wandering what corresponds to the logical xor o...

Curry's paradox (named after the same person as the present programming language) is a construction possible in a faulty logic that allows one to prove anything. I know nothing about logic, but ho...

How do I show that anything follows from a value of a type with no constructors in Scala? I would like to do a pattern match on the value and have Scala tell me that no patterns can match, but I am...

In wikipedia, the bottom type is simply defined as "the type that has no values". However, if b is this empty type, then the product type (b,b) has no values either, but seems different from b. I a...

The absurd function in Data.Void has the following signature, where Void is the logically uninhabited type exported by that package: -- | Since 'Void' values logically don't exist, this witnesses ...

Edit: By Void, I mean Haskell's Void type, i.e. empty type that cannot have values but undefined. There is an ongoing discussion on Swift Evolution whether to replace noreturn function attribute w...

If I understand Curry-Howard's isomorphism correctly, every dependent type correspond to a theorem, for which a program implementing it is a proof. That means that any mathematical problem, such as...

Which is the Curry-Howard correspondent of double negation of a; (a -> r) -> r or (a -> ⊥) -> ⊥, or both? Both types can be encoded in Haskell as follows, where ⊥ is encoded as forall...

I am trying to understand "Löb and möb: strange loops in Haskell", but right now the meaning is sleaping away from me, I just don't see why it could be useful. Just to recall function loeb is defin...

I've been studying dependent types and I understand the following: Why universal quantification is represented as a dependent function type. ∀(x:A).B(x) means “for all x of type A there is ...

I want to prove or falsify forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q. in Coq. Here is my approach. Inductive True2 : Prop := | One : True2 | Two : True2. Lemma True_has_one...

Intuitionistic logic, being constructive, is the basis for type systems in functional programming. The classical logic is not constructive, in particular the law of excluded middle A ∨ ¬A (or its e...

Set, similarly to [] has a perfectly defined monadic operations. The problem is that they require that the values satisfy Ord constraint, and so it's impossible to define return and >>= witho...

I came upon the Curry-Howard Isomorphism relatively late in my programming life, and perhaps this contributes to my being utterly fascinated by it. It implies that for every programming concept the...

So, in my ongoing attempts to half-understand Curry-Howard through small Haskell exercises, I've gotten stuck at this point: {-# LANGUAGE GADTs #-} import Data.Void type Not a = a -> Void --...

So in order to help me understand some of the more advanced Haskell/GHC features and concepts, I decided to take a working GADT-based implementation of dynamically typed data and extend it to cover...

I've searched around the Internet, and I can't find any explanations of CHI which don't rapidly degenerate into a lecture on logic theory which is drastically over my head. (These people talk as if...

Could you please explain me what is the basic connection between the fundamentals of logical programming and the phenomenon of syntactic similarity between type systems and conventional logic?