Merging Local Types for Synthesis

MergeForSynthesis.org

Merging Local Types for Synthesis

This document is a literate Idris2 file that the compiler can understand, and if one uses polymode for eMacs can highlight…

In this document, we outline a proof of Merge For Synthesis for a simple representation of Local type. Merging this into Capable is going to be trifficult!

Preamble

Important preamble stuff.

module MergeForSynthesis

import Decidable.Equality
import Data.Maybe
import Data.List
import Data.List.Quantifiers

%default total

and helper functions that we do not really need.

namespace Helpers
  export
  isDecided : Dec a -> Bool
  isDecided (Yes _) = True
  isDecided (No _)  = False

  export
  decidable : b -> (a -> b) -> Dec a -> b
  decidable def _ (No no) = def
  decidable _   f (Yes a) = f a

Base Types

Some simple base types and definitions.

||| Simple Base types
data Ty = N | B

Show Ty where
  show N = "N"
  show B = "B"

Uninhabited (N = B) where
  uninhabited Refl impossible

DecEq Ty where
  decEq N N = Yes Refl
  decEq N B = No absurd
  decEq B N = No (negEqSym absurd)
  decEq B B = Yes Refl

Eq Ty where
  (==) x y = isDecided (decEq x y)

Ord Ty where
  compare N N = EQ
  compare N B = LT
  compare B N = GT
  compare B B = EQ

Here we define merging of base types. This is where we could introduce more advance analysis i.e. sub-typing.

namespace Ty
  public export
  data Merge : (x,y,z : Ty) -> Type where
    M : Merge x x x

  export
  mergeTy : (x,y : Ty) -> Dec (DPair Ty (Merge x y))
  mergeTy x y with (decEq x y)
    mergeTy x x | (Yes Refl)
      = Yes (x ** M)
    mergeTy x y | (No contra)
      = No (\case (_ ** M) => contra Refl)

Local Types

Following the less is more construction.

data Local = End
           | Call String
           | Rec String Local
           | Offer  (List (String, Ty, Local))
           | Select (List (String, Ty, Local))

Show Local where
  show End = "End"
  show (Call str)
    = "(Call \{show str})"

  show (Rec str x)
    = "(Rec \{str} \{show x})"

  show (Offer xs)
    = "(Offer \{assert_total $ show xs})"

  show (Select xs)
    = "(Select \{assert_total $ show xs})"

Diagonals for Local Types.

‘Diagonals’ support head-oriented comparison of inductive structures.

The key take-away is we state when two instances of the same inductive type have the same head. If the head is okay proceed to the body, otherwise fail. This trick supports reducing pattern matching to roughly n instead of n squared.

namespace Diag
  public export
  data Diag : (x,y : Local) -> Type where
    End : Diag End End
    Call : Diag (Call x) (Call y)
    Rec :  Diag (Rec x a) (Rec y b)
    Offer : Diag (Offer xs) (Offer ys)
    Select : Diag (Select xs) (Select ys)

  public export
  diag : (x,y : Local) -> Maybe (Diag x y)
  diag End End = Just End
  diag (Call str) (Call a) = Just (Call)
  diag (Rec str x) (Rec a y) = Just (Rec)
  diag (Offer xs) (Offer ys) = Just (Offer)
  diag (Select xs) (Select ys) = Just (Select)
  diag _ _ = Nothing


  public export
  data SameShape : (x,y : Local) -> Type where
    SS : {x,y : Local} -> Diag x y -> SameShape x y

  urgh : (diag x y = Nothing) -> Diag x y -> Void
  urgh Refl End impossible
  urgh Refl Call impossible
  urgh Refl Rec  impossible
  urgh Refl Offer  impossible
  urgh Refl Select impossible

  export
  sameShape : (x,y : Local) -> Dec (SameShape x y)
  sameShape x y with (diag x y) proof a
    sameShape x y | Nothing = No (\case (SS z) => urgh a z)
    sameShape x y | (Just z) = Yes (SS z)

Type Aliases

public export
Branch : Type
Branch = (String, Ty, Local)

public export
Branches : Type
Branches = List (String, Ty, Local)

Predicates Acting Upon Branches

Shared Labels & Keys

namespace Branch
  public export
  data SharedLabel : (x,y : Branch) -> Type where
    SLabel : SharedLabel (l,ta,ca) (l,tb,cb)

  export
  sharedLabel : (x,y : Branch) -> Dec (SharedLabel x y)
  sharedLabel (la, ta, ca) (lb,tb,cb) with (decEq la lb)
    sharedLabel (la, ta, ca) (la,tb,cb) | (Yes Refl)
      = Yes SLabel
    sharedLabel (la, ta, ca) (lb,tb,cb) | (No contra)
      = No (\SLabel => contra Refl)

  public export
  data SharedKey : (x, y : Branch) -> Type where
    IsShared : SharedKey (l,t,ca) (l,t,cb)

  export
  sharedKey : (x,y : Branch) -> Dec (SharedKey x y)
  sharedKey (la,ta,ca) (lb,tb,cb) with (decEq la lb)
    sharedKey (la,ta,ca) (la,tb,cb) | (Yes Refl) with (decEq ta tb)
      sharedKey (la,ta,ca) (la,ta,cb) | (Yes Refl) | (Yes Refl)
        = Yes IsShared
      sharedKey (la,ta,ca) (la,tb,cb) | (Yes Refl) | (No contra)
        = No (\IsShared => contra Refl)
    sharedKey (la,ta,ca) (lb,tb,cb) | (No contra)
      = No (\IsShared => contra Refl)

Transport

Re-purpose Any to say where shared labels and branches are in a list of branches.

public export
HasEntry : (0 p : (x,y : Branch) -> Type)
        -> (x  : Branch)
        -> (xs : List Branch)
              -> Type
HasEntry p x = Any (p x)

export
hasEntry : (f  : (x,y : Branch) -> Dec (p x y))
        -> (x  : Branch)
        -> (xs : List Branch)
              -> Dec (HasEntry p x xs)
hasEntry f x
  = any (f x)

Sorting

A nasty hack for much later on.

public export
data Sort : (xs,ys  : List (String,Ty,Local)) -> Type where
  IsSorted : Sort xs ys

public export
sortBS : (xs : List (String,Ty,Local))
            -> List (String,Ty,Local)
sortBS
  = sortBy (\(la,ta,ca), (lb,tb,cb) => compare (la,ta) (lb,tb))

export
sorted : (xs : List (String,Ty,Local)) -> Sort xs (sortBS xs)
sorted xs = IsSorted

‘Set’ Difference

Capture where list xs differs with ys.

public export
data Diff : (xs, ys, zs : List Branch) -> Type where
  EmptyD : Diff Nil ys Nil
  InclD : (HasEntry SharedLabel x ys -> Void)
      -> Diff     xs  ys zs
      -> Diff (x::xs) ys (x::zs)

  PassD : HasEntry SharedLabel x      ys
      -> Diff     xs  ys     zs
      -> Diff (x::xs) ys zs

export
diff : (xs, ys : List Branch)
              -> DPair (List Branch) (Diff xs ys)
diff [] ys
  = ([] ** EmptyD)
diff (x :: xs) ys with (hasEntry sharedLabel x ys)
  diff (x :: xs) ys | (Yes prf) with (diff xs ys)
    diff (x :: xs) ys | (Yes prf) | (res ** prfs)
      = (res ** PassD prf prfs)
  diff (x :: xs) ys | (No contra) with (diff xs ys)
    diff (x :: xs) ys | (No contra) | (res ** prfs)
      = (x::res ** InclD contra prfs)

Merging Local Types.

namespace Merge

Definition and Proof that we can merge two Local types into a single type, or not.

We parameterise the merging of branches to remove co-inductive structures.

When X Meet Y.

Meet is a view on the results of merging two branches x and y, such that we require the result of the meeting at the type-level.

Definition

Lemma X will ‘Meet’ Y if labels and types match, and continuations can merge.

Meeting either:

YM

Successful and will produce a new branch.

NM

X does not meeting with Y, think sharks and jets ;-)

FMT

Although X should meet with Y the types themselves do not meet.

FMM

Although X should meet with Y, and the types meet, merging fails.

public export
data Result = YesMeet Branch | NoMeet | FailMeet

public export
data Meet : (0     p : (x,y,z : Local) -> Type)
         -> (  x,y : Branch)
         -> (  r   : Result)
                    -> Type
  where
    YM : (prfSH : Equal    la lb)
      -> (prfTY : Ty.Merge ta ta tc)
      -> (prfME : p        ca cb cc)
               -> Meet p (la,ta,ca) (la,ta,cb) (YesMeet (la,tc,cc))
    NM : (prfSH : Equal la lb -> Void)
               -> Meet p (la,ta,ca) (lb,tb,cb) NoMeet
    FMT : (prfSH : Equal    la lb)
       -> (prfTY : {tc : _} -> Ty.Merge ta tb tc -> Void)
                -> Meet p (la,ta,ca) (la,tb,cb) (FailMeet)
    FMM : (prfSH : Equal    la lb)
       -> (prfTY : Ty.Merge ta ta tc)
       -> (prfM  : {cc : _} -> p ca cb cc -> Void)
                -> Meet p (la,ta,ca) (la,tb,cb) (FailMeet)

‘Proof’

Blah blah blah…

export
meet : (f : (x,y : Local) -> Dec (DPair Local (p x y)))
    -> (x,y : Branch)
           -> DPair Result (Meet p x y)
meet f (la, ta, ca) (lb, tb, cb) with (decEq la lb)
  meet f (la, ta, ca) (la, tb, cb) | (Yes Refl) with (mergeTy ta tb)
    meet f (la, ta, ca) (la, tb, cb) | (Yes Refl) | (Yes (tc ** prfTy)) with (f ca cb)
      meet f (la, ta, ca) (la, ta, cb) | (Yes Refl) | (Yes (ta ** M)) | (Yes (cc ** prfM))
        = (YesMeet (la,ta,cc) ** YM Refl M prfM)
      meet f (la, ta, ca) (la, tb, cb) | (Yes Refl) | (Yes (tc ** prfTy)) | (No contra)
        = (FailMeet ** FMM Refl M (\x => contra (_ ** x)))

    meet f (la, ta, ca) (la, tb, cb) | (Yes Refl) | (No contra)
      = (FailMeet ** FMT Refl (\x => contra (_ ** x)))

  meet f (la, ta, ca) (lb, tb, cb) | (No contra)
    = (NoMeet ** NM contra)

When X Meets YS.

Meets is a proposition that only records no meets and successful meets only.

Definition

A valid meet between X and YS is one in which there are only no meetings or successful ones. The result will be a potentially empty list of the successful meetings.

public export
data Meets : (0 p : (x,y,z : Local) -> Type)
          -> (x   : Branch)
          -> (ys  : List Branch)
          -> (zs  : List Branch)
                 -> Type
  where
    EmptyMS : Meets p x Nil Nil
    MeetXY : Meet  p x  y      (YesMeet z)
          -> Meets p x     ys             zs
          -> Meets p x (y::ys)         (z::zs)
    MeetNo : Meet p x y NoMeet
          -> Meets p x ys zs
          -> Meets p x (y::ys)            zs

Proof

By structural induction blah blah blah…

export
meets : (f : (x,y : Local) -> Dec (DPair Local (p x y)))
     -> (x  : Branch)
     -> (ys : List Branch)
           -> Dec (DPair Branches (Meets p x ys))
meets f x []
  = Yes ([] ** EmptyMS)
meets f x (y :: xs) with (meet f x y)
  meets f (la, (ta, ca)) ((la, (ta, cb)) :: xs) | ((YesMeet (la, (tc, cc))) ** (YM prfSH prfTY prfME)) with (meets f (la,ta,ca) xs)
    meets f (la, (ta, ca)) ((la, (ta, cb)) :: xs) | ((YesMeet (la, (tc, cc))) ** (YM prfSH prfTY prfME)) | (Yes (zs ** prf))
      = Yes ((la, (tc, cc)) :: zs ** MeetXY (YM prfSH prfTY prfME) prf)
    meets f (la, (ta, ca)) ((la, (ta, cb)) :: xs) | ((YesMeet (la, (tc, cc))) ** (YM prfSH prfTY prfME)) | (No contra)
      = No (\case (fst ** snd) => case snd of
                                       (MeetXY x y) => contra (_ ** y)
                                       (MeetNo x y) => contra (fst ** y))

  meets f (la, (ta, ca)) ((lb, (tb, cb)) :: xs) | (NoMeet ** (NM prfSH)) with (meets f (la, ta, ca) xs)
    meets f (la, (ta, ca)) ((lb, (tb, cb)) :: xs) | (NoMeet ** (NM prfSH)) | (Yes ((fst ** snd)))
      = Yes (fst ** MeetNo (NM prfSH) snd)
    meets f (la, (ta, ca)) ((lb, (tb, cb)) :: xs) | (NoMeet ** (NM prfSH)) | (No contra)
      = No (\case ((z :: zs) ** (MeetXY x y)) => contra (zs ** y)
                  (fst ** (MeetNo x y)) => contra (fst ** y))

  meets f (la, (ta, ca)) ((la, (tb, cb)) :: xs) | (FailMeet ** (FMT prfSH prfTY))
    = No (\case (fst ** snd) => case snd of
                                     (MeetXY x y) => case x of
                                                          (YM prf z prfME) => prfTY z
                                     (MeetNo x y) => case x of
                                                          (NM g) => g Refl)
  meets f (la, (ta, ca)) ((la, (tb, cb)) :: xs) | (FailMeet ** (FMM prfSH prfTY prfM))
    = No (\case (fst ** snd) => case snd of
                                     (MeetXY x y) => case x of
                                                          (YM prf z prfME) => prfM prfME
                                     (MeetNo x y) => case x of
                                                          (NM g) => g Refl)

Meetings between XS & YS

A meeting between two list of branches is a collection of successful ‘meets’. We use this proposition to record branch intersection.

Definition

public export
data Meeting : (0 p : (x,y,z : Local) -> Type)
            -> (xs  : List Branch)
            -> (ys  : List Branch)
            -> (zs  : List Branch)
                   -> Type
  where
    EmptyM : Meeting p Nil ys Nil

    MeetXYS : {zs,as : _}
           -> Meets   p x ys zs
           -> Meeting p xs ys as
           -> Meeting p (x::xs)  ys (zs ++ as)

Proof

By structural induction on blah blah blah…

export
meeting : (f : (x,y : Local) -> Dec (DPair Local (p x y)))
       -> (xs : Branches)
       -> (ys : List Branch)
             -> Dec (DPair Branches (Meeting p xs ys))
meeting f [] ys
  = Yes ([] ** EmptyM)

meeting f (x :: xs) ys with (meets f x ys)
  meeting f (x :: xs) ys | (Yes (z ** pz)) with (meeting f xs ys)
    meeting f (x :: xs) ys | (Yes (z ** pz)) | (Yes (zs ** prf))
      = Yes (z ++ zs ** MeetXYS pz prf)
    meeting f (x :: xs) ys | (Yes (z ** pz)) | (No contra)
      = No (\case (fst ** snd) => case snd of
                                       (MeetXYS y w) => contra (_ ** w))
  meeting f (x :: xs) ys | (No contra)
    = No (\case (fst ** snd) => case snd of
                                     (MeetXYS y z) => contra (_ ** y))

Merging Local Types

Here we finally define two co-inductive proofs for merging local types.

One for merging branches, the other for terms themselves.

Propositions

Merging Branches

Merging these with those produces results, if each this and that shares a label and a type, and the branches can merge.

mutual
  namespace Branches
    public export
    data Merge : (these, those, results : List Branch) -> Type
      where
        Empty  : Merge Nil Nil Nil
        Extend : SharedKey (a,x,this) (b,y,that)
              -> Merge this  that  result
              -> Branches.Merge these those results
              -> Merge ((a,x,this)::these) ((b,y,that)::those) ((a,x,result)::results)

Protocol

Merging protocols is ‘full’ merge but with offer and select swapped.

Thus:

• For leaf terms this requires the terms to match.
• For Rec, the continuations must be mergable.
• For branching:
  • Offers must be total and each branch must match.
  • Select gathers information from both sides, and merges the intersections plus the differences.

  namespace Protocol
    public export
    data Merge : Local -> Local -> Local -> Type
      where
        End  : Merge End End End
        Call : {a,b : _} -> a = b -> Merge (Call a) (Call b) (Call a)
        Rec  : {a,b,this,that : _} -> a = b -> Merge this that result
            -> Merge (Rec a this)
                     (Rec b that)
                     (Rec a result)

        Offer : {this,that : _} -> Branches.Merge        this         that         result
             -> Merge (Offer this) (Offer that) (Offer result)

        Select : {this,that,shared:_}
              -> Diff this that lefts
              -> Diff that this rights
              -> Meeting Merge this that shared

              -> Merge (Select this) (Select that) (Select (shared ++ lefts ++ rights))

Uninhabited (Branches.Merge Nil (y::ys) zs) where
  uninhabited _ impossible

Uninhabited (Branches.Merge (x::xs) Nil zs) where
  uninhabited _ impossible

Proof Sketches

Branches

By structural induction on blah blah blah…

mutual
  namespace Branches
    export
    merge : (these, those : List Branch)
                         -> Dec (DPair (List Branch)
                                       (Branches.Merge these those))
    merge [] []
      = Yes ([] ** Empty)

    merge [] (x :: xs)
      = No (\case (fst ** snd) => absurd snd)

    merge (x :: xs) []
      = No (\case (fst ** snd) => absurd snd)

    merge (x :: xs) (y :: ys) with (sharedKey x y)
      merge ((l, (t, ca)) :: xs) ((l, (t, cb)) :: ys) | (Yes IsShared) with (merge ca cb)
        merge ((l, (t, ca)) :: xs) ((l, (t, cb)) :: ys) | (Yes IsShared) | (Yes (fst ** prf)) with (merge xs ys)
          merge ((l, (t, ca)) :: xs) ((l, (t, cb)) :: ys) | (Yes IsShared) | (Yes (fst ** prf)) | (Yes (x ** snd))
            = Yes ((l, (t, fst)) :: x ** Extend IsShared prf snd)
          merge ((l, (t, ca)) :: xs) ((l, (t, cb)) :: ys) | (Yes IsShared) | (Yes (fst ** prf)) | (No contra)
            = No (\case ((l,t,z)::zs ** Extend IsShared prfM rest) => contra (zs ** rest))

        merge ((l, (t, ca)) :: xs) ((l, (t, cb)) :: ys) | (Yes IsShared) | (No contra)
          = No (\case ((l,t,z)::zs ** (Extend IsShared prfM rest)) => contra (z ** prfM))

      merge (x :: xs) (y :: ys) | (No contra)
        = No (\case ((l,t,z)::zs ** (Extend IsShared prfM rest)) => contra IsShared)

Protocols

By structural induction on blah blah blah…

namespace Protocol

  merge_rhs_rhs_2 : (SameShape this that -> Void) -> Merge this that fst_0 -> Void
  merge_rhs_rhs_2 f End = f (SS End)
  merge_rhs_rhs_2 f (Call prf) = f (SS Call)
  merge_rhs_rhs_2 f (Rec prf x) = f (SS Rec)
  merge_rhs_rhs_2 f (Offer x) = f (SS Offer)
  merge_rhs_rhs_2 f (Select x y z) = f (SS Select)

  export
  merge : (this, that : Local) -> Dec (DPair Local (Merge this that))
  merge this that with (sameShape this that)
    merge this that | (Yes (SS sh)) with (sh)
      merge End End | (Yes (SS sh)) | End
        = Yes (End ** End)

      merge (Call x) (Call y) | (Yes (SS sh)) | Call with (decEq x y)
        merge (Call x) (Call x) | (Yes (SS sh)) | Call | (Yes Refl)
          = Yes (Call x ** Call Refl)
        merge (Call x) (Call y) | (Yes (SS sh)) | Call | (No contra)
          = No (\case (Call x ** Call prf) => contra prf)

      merge (Rec x a) (Rec y b) | (Yes (SS sh)) | Rec with (decEq x y)
        merge (Rec x a) (Rec x b) | (Yes (SS sh)) | Rec | (Yes Refl) with (merge a b)
          merge (Rec x a) (Rec x b) | (Yes (SS sh)) | Rec | (Yes Refl) | (Yes (z ** prf))
            = Yes (Rec x z ** Rec Refl prf)

          merge (Rec x a) (Rec x b) | (Yes (SS sh)) | Rec | (Yes Refl) | (No contra)
            = No (\case (Rec x b ** snd) => case snd of
                                                 (Rec prf y) => contra (b ** y))
        merge (Rec x a) (Rec y b) | (Yes (SS sh)) | Rec | (No contra)
          = No (\case (Rec a b ** snd) => case snd of
                                               (Rec Refl z) => contra Refl)

      merge (Offer xs) (Offer ys) | (Yes (SS sh)) | Offer with (merge xs ys)
        merge (Offer xs) (Offer ys) | (Yes (SS sh)) | Offer | (Yes (fst ** snd))
          = Yes (Offer fst ** Offer snd)

        merge (Offer xs) (Offer ys) | (Yes (SS sh)) | Offer | (No contra)
          = No (\case (Offer result ** Offer x) => contra (result ** x))

      merge (Select xs) (Select ys) | (Yes (SS sh)) | Select with (diff xs ys)
        merge (Select xs) (Select ys) | (Yes (SS sh)) | Select | (ls ** prfLS) with (diff ys xs)
          merge (Select xs) (Select ys) | (Yes (SS sh)) | Select | (ls ** prfLS) | (rs ** prfRS) with (meeting merge xs ys)
            merge (Select xs) (Select ys) | (Yes (SS sh)) | Select | (ls ** prfLS) | (rs ** prfRS) | (Yes (shared ** prfSH))
              = Yes (Select (shared ++ (ls ++ rs)) ** Select prfLS prfRS prfSH)
            merge (Select xs) (Select ys) | (Yes (SS sh)) | Select | (ls ** prfLS) | (rs ** prfRS) | (No contra)
              = No (\case (Select (shared ++ (lefts ++ rights)) ** (Select x y z)) => contra (shared ** z))

    merge this that | (No contra)
      = No (\case (fst ** prf) => merge_rhs_rhs_2 contra prf)

Example Cases…

Please use the repl to play with it all.

aLocalType : Local
aLocalType = Select [("this", N, End)]

bLocalType : Local
bLocalType = Select [("that", B, End)]