[Haskell-cafe] Re: help with MPTC for type proofs?

[oleg at pobox.com]

David Roundy wrote:
> class Commutable a b d c
>
> commute :: Commutable a b d c =>
>           (Patch a b, Patch b c) -> (Patch a d, Patch d c)
>
> But for this to work properly, I'd need to guarantee that
>
> 1. if (Commutable a b d c) then (Commutable a d b c)
>
> 2. for a given three types (a b c) there exists at most one type d
>   such that (Commutable a b c d)

The problem seems easily solvable, exactly as described. We need to
take care of the two requirements separately.


> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
>
> module D1 where
>
> data Patch a b = Patch String deriving Show
>
> -- This is identical to what Tom Schrijvers wrote
> class Commutable a b c d |
>                 a b c -> d,     -- 2.
>                 a d c -> b      -- based on 1. + 2.
>
> -- But how do we make sure that Commutable a d c b exists whenever
> -- Commutable a b c d does? very easily: with the help of another
> -- type class
> instance (Commutable' a b c d, Commutable' a d c b)
>     => Commutable a b c d
>
> class Commutable' a b c d | a b c -> d
>
> -- The desired function
> commute :: Commutable a b c d =>
>            (Patch a b, Patch b c) -> (Patch a d, Patch d c)
> commute ((Patch p1),(Patch p2)) = ((Patch p1),(Patch p2))
>
> -- Testing
> -- Define some patch labels
>
> data PL1
> data PL2
> data PL2I
> data PL3
> data PL4
>
> instance Commutable' PL1 PL2 PL3 PL2I
> -- If the latter is commented out, there will be an error in testab below
> instance Commutable' PL1 PL2I PL3 PL2
>
> pa :: Patch PL1 PL2 = Patch "PA: 1->2"
> pe :: Patch PL2 PL3 = Patch "PE: 2->3"
>
> -- Test as was in David Roundy's message
> test (a,b) = do (b',a')     <- return $ commute (a,b)
>                 (b'', a'')  <- return $ commute (a,b)
>                 (a''',b''') <- return $ commute (b',a'')
>                 return ()
>
> testab :: IO () = test (pa,pe)

However, something tells me that the above approach isn't useful. We
really would like to have as many patch labels as _dynamically_
needed. Also, we probably would like to specify which patches commute
dynamically, rather than statically. That is, we wish to examine the
patches and only then conclude if they commute. Thus we need to
program with evidence. The function commute becomes a semantic
function: it really does something, at run-time. It examines the
patches. If it decides the patches commute, it produces the pair of
patches, marked with a unique and unforgeable type d -- along with the
evidence that d is indeed determined by b, and vice versa. We need
this evidence for the creative mixing of patches, as in the original
test. This approach is not unlike the one described half a year ago,
in response to a similar query:

  http://www.haskell.org/pipermail/haskell-cafe/2005-December/012703.html

I still don't know if the were some problems with that
approach. Anyway, here's the complete code:

> {-# OPTIONS -fglasgow-exts #-}
>
> module D2 where
>
> data Patch a b = Patch String deriving Show
>
> -- Define the commutation pair
> data CP a b c = forall d. CP (Patch a d) (Patch d c) (EQP b d)
>
> data EQP b d = EQP -- Hide the constructor
>
> -- The following creates the proof
> -- Assume patches commute if their bodies are the same
> commute :: Patch a b -> Patch b c -> CP a b c
> commute (Patch p1) (Patch p2) | p1 == p2 =  CP (Patch p1) (Patch p2) EQP
>
> -- Testing
> -- Define some patch labels
>
> data PL1
> data PL2
> data PL3
> data PL4
>
> pa :: Patch PL1 PL2 = Patch "PA: 1->2"
> pe :: Patch PL2 PL3 = Patch "PA: 1->2"
>
> -- coercion functions, using the evidence
> a1 :: Patch a d -> EQP b d -> Patch a b
> a1 (Patch p) EQP = Patch p
> a2 :: Patch d c -> EQP b d -> Patch b c
> a2 (Patch p) EQP = Patch p
>
> test a b = do CP b' a' e'       <- return $ commute  a b
>               CP b''  a'' e''   <- return $ commute  a b
>               CP a''' b''' e''' <- return $ commute  (a1 b' e') (a2 a'' e'')
>               return ()
>
> testab :: IO () = test pa pe