Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
proving a lemma about least elements in posets in Haskell using singletons
{-# 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
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 ];
}
@cdepillabout

This comment has been minimized.

Copy link
Owner Author

@cdepillabout cdepillabout commented Nov 12, 2018

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'
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment