Propositions *AS* Types: The Cheatsheet (with Fancy Nancy)

Logic.idr

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 -- ;)