Stack Overflow
Stack Overflow

Questions tagged [curry-howard]

The Curry–Howard correspondence is the direct relationship between computer programs and proofs in programming language theory and proof theory.

Curry–Howard correspondence is also known as Curry–Howard isomorphism, proofs-as-programs correspondence and formulae-as-types correspondence. It is a generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the American mathematician Haskell Curry and logician William Alvin Howard.

Source http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence

43 questions
106
votes
6 answers

What's the absurd function in Data.Void useful for?

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 the logical -- reasoning tool of \"ex falso…
Luis Casillas
  • 29,802
  • 7
  • 49
  • 102
104
votes
10 answers

What are the most interesting equivalences arising from the Curry-Howard Isomorphism?

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 there exists a precise analogue in formal logic, and…
Tom Crockett
  • 30,818
  • 8
  • 72
  • 90
61
votes
3 answers

Curry-Howard isomorphism

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 "intuitionistic proposition calculus" is a phrase…
MathematicalOrchid
  • 61,854
  • 19
  • 123
  • 220
41
votes
6 answers

Dependent Types: How is the dependent pair type analogous to a disjoint union?

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 a value of type B(x)”. Hence it's represented as a function…
Aadit M Shah
  • 72,912
  • 30
  • 168
  • 299
32
votes
4 answers

Constructing efficient monad instances on `Set` (and other containers with constraints) using the continuation monad

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 >>= without any constraints. The same problem applies to many other…
Petr
  • 62,528
  • 13
  • 153
  • 317
22
votes
3 answers

Is Curry-Howard correspondent of double negation ((a->r)->r) or ((a->⊥)->⊥)?

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 b. b. p1 :: forall r. ((a -> r) -> r) p2 :: (a -> (forall b. b))…
nushio
  • 753
  • 3
  • 12
21
votes
2 answers

Can GADTs be used to prove type inequalities in GHC?

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 -- | The type of type equality proofs, which can only be…
Luis Casillas
  • 29,802
  • 7
  • 49
  • 102
19
votes
3 answers

What else can `loeb` function be used for?

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 defined as loeb :: Functor f => f (f a -> a) -> f a loeb…
Yrogirg
  • 2,301
  • 3
  • 22
  • 33
12
votes
1 answer

What type corresponds to a xor b in type theory?

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 operator. I know that a xor b == (a ∨ b) ∧ ¬(a ∧ b)…
Enlico
  • 23,259
  • 6
  • 48
  • 102
10
votes
1 answer

What is the bottom type?

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 agree bottom is uninhabited, but I don't think this…
V. Semeria
  • 3,128
  • 1
  • 10
  • 25
10
votes
1 answer

How come that we can implement call/cc, but the classical logic (intuitionistic + call/cc) is not constructive?

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 equivalents, such as double negation elimination or…
Petr
  • 62,528
  • 13
  • 153
  • 317
9
votes
2 answers

A question about logic and the Curry-Howard correspondence

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?
Bubba88
  • 1,910
  • 20
  • 44
8
votes
3 answers

If Either can be either Left or Right but not both, then why does it correspond to OR instead of XOR in Curry-Howard correspondence?

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 and Right at the same time. Where is the truth?
Enlico
  • 23,259
  • 6
  • 48
  • 102
8
votes
1 answer

Practical examples of using Void

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 with an actual Void type. To do so, we must be sure…
Anton3
  • 577
  • 4
  • 14
8
votes
1 answer

How or is that possible to prove or falsify `forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.` in Coq?

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 : forall (t0 t1 : True), t0 = t1. Proof. intros. destruct…
TorosFanny
  • 1,702
  • 1
  • 16
  • 25
1
2 3