proving a lemma about least elements in posets in Haskell using singletons

a-poset-lemma.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wall #-}

import Data.Kind (Type)
import Data.Singletons
import Data.Singletons.Prelude
import Data.Singletons.TH

-- Define some singletons.

$(singletons [d|

  -- Create a partially ordered set class that represents a set with a single binary relation ('lte').
  --
  -- (This is actually a totally ordered set.)
  --
  -- 'lte' stands for \"less than or equals\", but it could really be any binary relation.
  class POSet s where
    lte :: s -> s -> Bool

  -- Define an example set we can use.
  data MySet = Zero | One | Two deriving Show

  -- Show that 'Zero' is less than everything else.
  instance POSet MySet where
    lte Zero Zero = True
    lte Zero One = True
    lte Zero Two = True
    lte One Zero = False
    lte One One = True
    lte One Two = True
    lte Two Zero = False
    lte Two One = False
    lte Two Two = True
  |])

-- | This defines the notion of a "least element" on a set.
--
-- The type signature on the constructor can be read as follows:
--
-- For all sets @s@ and elements @a@ where @s@ is a 'POSet', we know that if
-- @a@ is less than ALL elements of @s@, then we know that @a@ is a "least
-- element" of @s@.
data LeastElem :: a -> Type where
  LeastElem
    :: forall (s :: Type) (a :: s)
     . POSet s
    => Sing a
    -> (forall (x :: s). Sing x -> Lte a x :~: 'True)
    -> LeastElem a

-- | Create an example 'LeastElem' over 'MySet'.
exampleLeastElem :: LeastElem 'Zero
exampleLeastElem = LeastElem (sing @'Zero) go
  where
    go :: forall (x :: MySet). Sing x -> Lte 'Zero x :~: 'True
    go SZero = Refl
    go SOne = Refl
    go STwo = Refl

-- | This class defines laws that a 'POSet' must follow.
--
-- Currently only reflexivity is defined.
--
-- Reflexivity says that if we know that @a@ and @b@ are elements of @s@,
-- and @a@ is less than or equal to @b@, and @b@ is less than or equal to @a@,
-- then @a@ equals @b@.
class POSet s => POSetLaws s where
  posetReflex
    :: forall (a :: s) (b :: s)
     . (Lte a b ~ 'True, Lte b a ~ 'True)
    => Sing a
    -> Sing b
    -> a :~: b

-- | Instace of 'POSetLaws' for 'MySet'.
instance POSetLaws MySet where
  posetReflex
    :: forall (a :: MySet) (b :: MySet)
     . (Lte a b ~ 'True, Lte b a ~ 'True)
    => Sing a
    -> Sing b
    -> a :~: b
  posetReflex SZero SZero = Refl
  posetReflex SOne SOne = Refl
  posetReflex STwo STwo = Refl

-- | This lemma proves that if @a@ and @b@ are both elements of a set @s@, and
-- they are both least elements, then they must be equal.
--
-- This proves that least elements are unique.
--
-- This is the most interesting part of this file.
leastElemUniqLemma
  :: forall (s :: Type) (a :: s) (b :: s)
   . POSetLaws s
  => LeastElem a
  -> LeastElem b
  -> a :~: b
leastElemUniqLemma (LeastElem singA leastProofA) (LeastElem singB leastProofB) =
  case leastProofA singB of
    Refl ->
      case leastProofB singA of
        Refl -> posetReflex singA singB

-- Simple example of using our lemma.
testLemma :: 'Zero :~: 'Zero
testLemma = leastElemUniqLemma exampleLeastElem exampleLeastElem

my-ghc-8.6.2.nix

let
  nixpkgsTarball = builtins.fetchTarball {
    name = "nixos-unstable-2018-11-09";
    url = https://github.com/nixos/nixpkgs/archive/1c49226176d248129c795f4a654cfa9d434889ae.tar.gz;
    sha256 = "0v8vp38lh6hqazfwxhngr5j96m4cmnk1006kh5shx0ifsphdip62";
  };

  nixpkgs = import nixpkgsTarball { };
in

with nixpkgs;

let
  ghc862 =
    haskell.packages.ghc862.override {
      overrides = self: super: {

        singletons = haskell.lib.overrideCabal super.singletons (drv: {
          version = "2.5";
          sha256 = "0bk1ad4lk4vc5hw2j4r4nzs655k43v21d2s66hjvp679zxkvzz44";
        });

        th-desugar = self.callHackage "th-desugar" "1.9" {};
      };
    };

  ghcWithPkgs =
    ghc862.ghcWithPackages (pkgs: with pkgs; [ singletons ]);
in

pkgs.mkShell {
  buildInputs = [ ghcWithPkgs ];
}

If you have nix installed, this can be loaded into GHCi like the following:

$ nix-shell my-ghc-8.6.2.nix --command 'ghci a-poset-lemma.hs'