Ghosts of Departed Proofs by Matt Noonan [3]

Philipp Zander

slides on https://prednaz.github.io/posts/2021-03-08-gdp_talk.html
complete example code on https://gitlab.com/rdnz/ghosts-proofs-map

expanded return type

-- | Lookup the value at a key in the map
-- if the key is in the map.
lookup :: Ord key => key -> Map key value -> Maybe value

member :: Ord key => key -> Map key value -> Bool

-- MainExpand.hs

data AppError =
  InvalidKey Integer | SomeOtherProblems
  deriving (Show)

-- | Validate key and map and potentially return an appropriate AppError.
validateMapKey ::
  Integer              ->
  M.Map Integer String ->
  Maybe AppError
validateMapKey key map =
  case M.member key map of
    False -> Nothing
    True  -> Just $ InvalidKey key

processMapKey ::
  Integer              ->
  M.Map Integer String ->
  String
processMapKey key map =
  case validateMapKey key map of
    Just appError -> "Error: " <> show appError
    Nothing       ->
      case M.lookup key map of
        Nothing -> error "impossible because we just applied validateMapKey"
        Just result -> result

expanded return type vs restricted argument types

Parse, don’t validate by Alexis King
Type Safety Back and Forth by Matt Parsons
Keep your types small… by Matt Parsons

first attempt at restricted argument types

-- NamedFirst.hs

newtype Named name a = Named a

name :: a -> Named name a
name a = Named a

forgetName :: Named name a -> a
forgetName (Named a) = a

-- MapWithProofsFirst.hs

data Member key map = Member

-- MapWithProofsFirst.hs

module MapWithProofsFirst (Member ()) where

member ::
  (Ord key)                        =>
  Named keyName key                ->
  Named mapName (M.Map key _value) ->
  Maybe (Member keyName mapName)
member key map =
  if M.member (forgetName key) (forgetName map)
  then Just Member
  else Nothing

-- MapWithProofsFirst.hs

lookup ::
  (Ord key)                       =>
  Named keyName key               ->
  Named mapName (M.Map key value) ->
  Member keyName mapName          ->
  value

-- MainFirst.hs

validateMapKey ::
  Named keyName Integer              ->
  Named mapName (Map Integer String) ->
  Either AppError (Member keyName mapName)
validateMapKey key map =
  case member key map of
    Just proof -> Right proof
    Nothing    -> Left $ InvalidKey (forgetName key)

processMapKey ::
  Integer            ->
  Map Integer String ->
  String
processMapKey key map =
  let
    keyNamed :: Named keyName Integer
    keyNamed = name key
    mapNamed :: Named mapName (Map Integer String)
    mapNamed = name map
  in case validateMapKey keyNamed mapNamed of
    Left appError -> "Error: " <> show appError
    Right proof   -> lookup keyNamed mapNamed proof

second attempt at restricted argument types

-- MainFirst.hs

validateMapKey ::
  Named keyName Integer              ->
  Named mapName (Map Integer String) ->
  Either AppError (Member keyName mapName)
validateMapKey key map =
  case member key map of
    Just proof -> Right proof
    Nothing    -> Left $ InvalidKey (forgetName key)

processMapKey ::
  Integer            ->
  Map Integer String ->
  String
processMapKey key map =
  let
    zeroNamed :: Named zeroName Integer
    zeroNamed = name 0
    keyNamed  :: Named keyName Integer
    keyNamed  = name key
    mapNamed  :: Named mapName (Map Integer String)
    mapNamed  = name map
  in case validateMapKey zeroNamed mapNamed of
    Left appError -> "Error: " <> show appError
    Right proof   -> lookup keyNamed mapNamed proof

wellTyped :: Int
wellTyped =
  let
    aList    :: [variable1]
    aList    = []
    bList    :: [variable2]
    bList    = aList
    boolList :: [Bool]
    boolList = aList
  in
    length bList

illTyped :: [variable1] -> ([Bool], [variable2])
illTyped aList =
  let
    boolList :: [Bool]
    boolList = aList
    bList   :: [variable2]
    bList   = aList
  in (boolList, bList)

    • Couldn't match type ‘variable1’ with ‘Bool’
   |
42 |     boolList = aList
   |                ^^^^^

    • Couldn't match type ‘variable2’ with ‘variable1’
   |
44 |     bList = aList
   |             ^^^^^

-- MainFirst.hs

validateMapKey ::
  Named keyName Integer              ->
  Named mapName (Map Integer String) ->
  Either AppError (Member keyName mapName)
validateMapKey key map =
  case member key map of
    Just proof -> Right proof
    Nothing    -> Left $ InvalidKey (forgetName key)

processMapKey ::
  Integer            ->
  Map Integer String ->
  String
processMapKey key map =
  let
    zeroNamed :: Named zeroName Integer
    zeroNamed = name 0
    keyNamed  :: Named keyName Integer
    keyNamed  = name key
    mapNamed  :: Named mapName (Map Integer String)
    mapNamed  = name map
  in case validateMapKey zeroNamed mapNamed of
    Left appError -> "Error: " <> show appError
    Right proof   -> lookup keyNamed mapNamed proof

-- Named.hs

{-# language RankNTypes #-}
module Named (Named (), name, forgetName) where

newtype Named name a = Named a

name ::
  a                                     ->
  (forall name. Named name a -> result) ->
  result
name a continuation = continuation (Named a)

forgetName :: Named name a -> a
forgetName (Named a) = a

-- Main.hs

processMapKey ::
  Integer            ->
  Map Integer String ->
  String
processMapKey key map =
  name key $ \keyNamed ->
  name map $ \mapNamed ->
  case validateMapKey keyNamed mapNamed of
    Left appError -> "Error: " <> show appError
    Right proof   -> lookup keyNamed mapNamed proof

-- Main.hs

processMapKey ::
  Integer            ->
  Map Integer String ->
  String
processMapKey key map =
  name key $ \(keyNamed :: Named keyName Integer)              ->
  name map $ \(mapNamed :: Named mapName (Map Integer String)) ->
  case validateMapKey keyNamed mapNamed of
    Left appError -> "Error: " <> show appError
    Right proof   -> lookup keyNamed mapNamed proof

-- Main.hs

processMapKey ::
  Integer            ->
  Map Integer String ->
  String
processMapKey key map =
  name 0   $ \zeroNamed ->
  name key $ \keyNamed  ->
  name map $ \mapNamed  ->
  case validateMapKey zeroNamed mapNamed of
    Left appError -> "Error: " <> show appError
    Right proof   -> lookup keyNamed mapNamed proof

    • Couldn't match type ‘name1’ with ‘name’
      Expected type: Member name1 name2
        Actual type: Member name name2
   |
37 |     Right proof -> lookup keyNamed mapNamed proof
   |                                             ^^^^^

propositional logic

-- MapWithProofs.hs

insert ::
  (Ord key)                       =>
  Named keyName key               ->
  value                           ->
  Named mapName (M.Map key value) ->
  (forall resultName. InsertResult keyName key value mapName resultName -> r) ->
  r

type InsertResult keyName key value mapName resultName =
  (
    Named resultName (M.Map key value),
    Member keyName resultName,
    mapName `KeySubset` resultName
  )

data map1 `KeySubset` map2 = KeySubset

-- Main.hs

insertExample :: String
insertExample =
  name 0                   $ \key0                             ->
  name 1                   $ \key1                             ->
  name (M.singleton 0 "a") $ \mapOld                           ->
  insert key1 "b" mapOld   $ \(mapNew, _proofKey, proofSubset) ->
  case member key0 mapOld of
    Nothing    -> error "impossible because `0` is member of `M.singleton 0 a`"
    Just proof -> lookup key0 mapNew (keySubset proofSubset proof)

-- MapWithProofs.hs

keySubset ::
  map1 `KeySubset` map2 ->
  Member key map1       ->
  Member key map2
keySubset _proof1 _proof2 = Member

-- MapWithProofs.hs

keySubset ::
  Either
    ((map1 `KeySubset` map2, Member key map1) -> Void)
    (Member key map2)

((S ∧ M) ⇒ ⊥) ∨ N

-- Main.hs

myKeySubset ::
  map1 `KeySubset` map2 ->
  Member key map1       ->
  Member key map2
myKeySubset proof1 proof2 =
  case keySubset of
    Right proof      -> proof
    Left implication -> absurd $ implication (proof1, proof2)

S ⇒ (M ⇒ N)

other

lightweight existential types

-- Named.hs

{-# language RankNTypes #-}
name ::
  a                                     ->
  (forall name. Named name a -> result) ->
  result
name a continuation = continuation (Named a)

-- Main.hs

insertExample :: String
insertExample =
  name 0                   $ \key0                             ->
  name 1                   $ \key1                             ->
  name (M.singleton 0 "a") $ \mapOld                           ->
  insert key1 "b" mapOld   $ \(mapNew, _proofKey, proofSubset) ->
  case member key0 mapOld of
    Nothing    -> error "impossible because `0` is member of `M.singleton 0 a`"
    Just proof -> lookup key0 mapNew (keySubset proofSubset proof)

lightweight existential types

GHC core developer Richard Eisenberg hopes to submit paper on lightweight existential types for ICFP 2021 by 2021-03-02 [1]
not motivated by Ghosts of Departed Proofs but interestingly by the other two approaches to formal verification of Dependent Haskell and LiquidHaskell [2]
exists keyword that syntactically works like forall [2]
hopes to have a new extension to GHC roughly by May [1]

lightweight existential types

name :: exists name. a -> Named name a

comparison with SMT based verification and type theory based verification

propositional logic only, no predicate logic
- lacks numbers and data structures
- there is a reason why formal verification uses SMT instead of SAT
- often impossible to export enough axioms to support all kinds of use cases
manual proofs like with dependent types and unlike SMT based verification
library code is not verified

reading recommendation

https://ocharles.org.uk/blog/posts/2019-08-09-who-authorized-these-ghosts.html contains a great example demonstrating the Curry–Howard isomorphism well and using the technique to avoid redundant checks

References

[1] Richard Eisenberg. 2020. Richard eisenberg on simplifying constraint solving in ghc. Retrieved February 18, 2021 from https://www.youtube.com/watch?v=flwz6V5Ps8w&t=3m41s

[2] Richard Eisenberg. 2021. Update on dependent haskell. Retrieved February 18, 2021 from https://www.youtube.com/watch?v=TXDivoj1v6w&t=5m17s

[3] Matt Noonan. 2018. Ghosts of departed proofs (functional pearl). In Proceedings of the 11th acm sigplan international symposium on haskell (Haskell 2018), Association for Computing Machinery, New York, NY, USA, 119–131. DOI:https://doi.org/10.1145/3242744.3242755