Haskell (Proof by Curry-Howard Isomorphism)
A mathematical proof that 2 + 2 = 5 in Haskell. The proof is based on the Curry-Howard Isomorphism, where mathematical propositions are expressed as types in a programming language (here 2 + 2 == 5) and mathematical proofs of a proposition P are expressed as terms of type P (here undefined). The proof exploits diverging functions in Haskell to get the paradoxical Qed. The definition of data a == b ... defines propositional equality : the type that is inhibited (iwith Refl) if and only if a and b are judgmentally equal — i.e. data a == and b .. simplify to the same expression.) The definition is equivalent to the definition of :~:.
{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, GADTs #-}
import GHC.TypeLits
proof :: 2 + 2 == 4
proof = Refl
paradox :: 2 + 2 == 5
paradox = undefined
data a == b where
Refl :: a == a
infix 4 ==
Haskell (Proof by Curry-Howard Isomorphism)
A mathematical proof that 2 + 2 = 5 in Haskell. The proof is based on the Curry-Howard Isomorphism, where mathematical propositions are expressed as types in a programming language (here 2 + 2 == 5) and mathematical proofs of a proposition P are expressed as terms of type P (here undefined). The proof exploits diverging functions in Haskell to get the paradoxical Qed. The definition of propositional equality (i.e. data a == b ...) is equivalent to the definition of :~:.
{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, GADTs #-}
import GHC.TypeLits
proof :: 2 + 2 == 4
proof = Refl
paradox :: 2 + 2 == 5
paradox = undefined
data a == b where
Refl :: a == a
infix 4 ==
Haskell (Proof by Curry-Howard Isomorphism)
A mathematical proof that 2 + 2 = 5 in Haskell. The proof is based on the Curry-Howard Isomorphism, where mathematical propositions are expressed as types in a programming language (here 2 + 2 == 5) and mathematical proofs of a proposition P are expressed as terms of type P (here undefined). The proof exploits diverging functions in Haskell to get the paradoxical Qed. data a == b ... defines propositional equality : the type that is inhibited (with Refl) if and only if a and b are judgmentally equal — i.e. a and b simplify to the same expression. The definition is equivalent to the definition of :~:.
{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, GADTs #-}
import GHC.TypeLits
proof :: 2 + 2 == 4
proof = Refl
paradox :: 2 + 2 == 5
paradox = undefined
data a == b where
Refl :: a == a
infix 4 ==
Haskell (Proof by Curry-Howard Isomorphism)
A mathematical proof that 2 + 2 = 5 in Haskell. The proof is based on the Curry-Howard Isomorphism, where mathematical propositions are expressed as types in a programming language (here 2 + 2 == 5) and mathematical proofs of a proposition P are expressed as terms of type P (here undefined). The proof exploits diverging functions in Haskell to get the paradoxical Qed. The definition of propositional equality (i.e. data a == b ...) is equivalent to the definition of :~: .
{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, GADTs #-}
import GHC.TypeLits
proof :: 2 + 2 == 4
proof = Refl
paradox :: 2 + 2 == 5
paradox = undefined
data a == b where
Refl :: a == a
infix 4 ==
Haskell (Proof by Curry-Howard Isomorphism)
A mathematical proof that 2 + 2 = 5 in Haskell. The proof is based on the Curry-Howard Isomorphism, where mathematical propositions are expressed as types in a programming language (here 2 + 2 == 5) and mathematical proofs of a proposition P are expressed as terms of type P (here undefined). The proof exploits diverging functions in Haskell to get the paradoxical Qed.
{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, GADTs #-}
import GHC.TypeLits
proof :: 2 + 2 == 4
proof = Refl
paradox :: 2 + 2 == 5
paradox = undefined
data a == b where
Refl :: a == a
infix 4 ==
Haskell (Proof by Curry-Howard Isomorphism)
A mathematical proof that 2 + 2 = 5 in Haskell. The proof is based on the Curry-Howard Isomorphism, where mathematical propositions are expressed as types in a programming language (here 2 + 2 == 5) and mathematical proofs of a proposition P are expressed as terms of type P (here undefined). The proof exploits diverging functions in Haskell to get the paradoxical Qed. The definition of propositional equality (i.e. data a == b ...) is equivalent to the definition of :~: .
{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, GADTs #-}
import GHC.TypeLits
proof :: 2 + 2 == 4
proof = Refl
paradox :: 2 + 2 == 5
paradox = undefined
data a == b where
Refl :: a == a
infix 4 ==
Haskell (Proof by Curry-Howard Isomorphism)
A mathematical proof that 2 + 2 = 5 in Haskell. The proof is based on the Curry-Howard Isomorphism, where mathematical propositions are expressed as types in a programming language (here 2 + 2 == 5) and mathematical proofs of a proposition P are expressed as terms of type P (here undefined). The proof exploits diverging functions in Haskell to get the paradoxical Qed.
{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, GADTs #-}
import GHC.TypeLits
import Data.Type.Equality
proof :: 2 + 2 == 4
proof = Refl
paradox :: 2 + 2 == 5
paradox = undefined
data a == b where
Refl :: a == a
infix 4 ==
Haskell (Proof by Curry-Howard Isomorphism)
A mathematical proof that 2 + 2 = 5 in Haskell. The proof is based on the Curry-Howard Isomorphism, where mathematical propositions are expressed as types in a programming language (here 2 + 2 == 5) and mathematical proofs of a proposition P are expressed as terms of type P (here undefined). The proof exploits diverging functions in Haskell to get the paradoxical Qed.
{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, GADTs #-}
import GHC.TypeLits
import Data.Type.Equality
proof :: 2 + 2 == 4
proof = Refl
paradox :: 2 + 2 == 5
paradox = undefined
data a == b where
Refl :: a == a
infix 4 ==
Haskell (Proof by Curry-Howard Isomorphism)
A mathematical proof that 2 + 2 = 5 in Haskell. The proof is based on the Curry-Howard Isomorphism, where mathematical propositions are expressed as types in a programming language (here 2 + 2 == 5) and mathematical proofs of a proposition P are expressed as terms of type P (here undefined). The proof exploits diverging functions in Haskell to get the paradoxical Qed.
{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, GADTs #-}
import GHC.TypeLits
proof :: 2 + 2 == 4
proof = Refl
paradox :: 2 + 2 == 5
paradox = undefined
data a == b where
Refl :: a == a
infix 4 ==