Goop's Bisectable History

First, the background noise:


module  Goop.Theroy.BisectableHistory
 

 
import  Goop.Theroy.Types
 

 
%default  total

Defining What a History is

Items, the atomic elements of history

The history is only for providing a locally bisectable ordering of items, and as such, it forgets the type information about those things, only remembering it's digest


public  export
 
record  Item  (output  :  Type)  (digest_value  :  output)  where
 
  constructor  MkItem
 
  {0  a  :  Type}
 
  {auto  impl  :  Digest  output  a}
 
  0  item  :  a
 
  {auto  witness  :  digest_value  =  digest  @{impl}  item}

We shall say that if two item's hashes are equal, then they are equal. This will help with "reassociating" items read off of disk with their in-structure counter part.

Note

This is nominally unsound, any collisions in the hash function will break the type system. However, if this implementation's choice of hash, blake3, has collisions found, we will already have bigger issues.

A Set is an object that contains an arbitrarily ordered collection of Item s. The order is important, in that it is preserved, but is only meaningful in so much as allowing the client to explicitly represent the actual order items happened in.