Skip to content

Instantly share code, notes, and snippets.

@mbbx6spp
Last active August 1, 2020 16:13
Show Gist options
  • Save mbbx6spp/e18a5a9e54fd6ce40633b15ea303b1bd to your computer and use it in GitHub Desktop.
Save mbbx6spp/e18a5a9e54fd6ce40633b15ea303b1bd to your computer and use it in GitHub Desktop.
Propositions *AS* Types: The Cheatsheet (with Fancy Nancy)
module Logic
-- Connective is a fancy word for operator.
namespace Connectives
-- Truth: Also known as the "unit" type, (there is only one truth in value,
-- literally).
-- Scala: type Truth = Unit
-- Haskell: type Truth = ()
Truth : Type
Truth = ()
-- Falsity: Also known as the "bottom" type; uninhabitable; no values exist
-- for this type.
-- Scala: type Falsity = Null
-- Haskell: type Falsity = Void -- not your imperative programmer's void!
Falsity : Type
Falsity = Void
-- Conjunction: Fancy word for logical AND. That's it. Now sound fancy at
-- the bar tonight!
-- Scala: type Conjunction[A, B] = (A, B)
-- Haskell: type Conjunction a b = (a, b)
Conjunction : Type -> Type -> Type
Conjunction = Pair
-- Disjunction: Fancy word for logical OR. That's it. Go tweet about it and
-- be all philosophical.
-- // Just kidding, it's more like Scalaz's \/ type called, 'disjunction'.
-- Scala: type Disjunction[A, B] = Either[A, B]
-- Haskell: type Disjunction a b = Either a b
Disjunction : Type -> Type -> Type
Disjunction = Either
-- Implication: Fancy word for "if we know A holds, then B holds."
-- Scala: type Implication[A, B] = A => B
-- Haskell: type Implication a b = (a -> b)
Implication : (a : Type) -> (b : Type) -> Type
Implication a b = a -> b
-- Negation: Fancy word for logical NOT.
-- Scala: type Negation[A] = A => Nothing
-- Haskell: type Negation a = a -> Void
Negation : (a : Type) -> Type
Negation a = a -> Void
-- Quantifier is just a fancy word for "describing how many"
namespace Quantifiers
-- universal quantification is a fancy term for "for all ..." prefix when
-- talking maths-y. In Idris, a function type serves as a universal
-- quantifier, and as such higher order functions allow the programmer to
-- nest universal quantification inside a larger proposition.
-- existential quantification is a fancy term for:
-- "there exists A such that B".
-- In Idris, this is represented as a dependent pair, which has special
-- syntax.
-- Below is the Archimedean property of the natural numbers, namely:
-- Given n in naturals, there exists an m in the naturals such that m > n.
archimedean : (n : Nat) -> (m : Nat ** LTE n m)
archimedean n = ?exerciseForReader -- ;)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment