Re: help with MPTC for type proofs?
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
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
I had not thought of using a double constraint. Very clever. Why not also put this constraint in the class declaration? You don't want any other instances of Commutable (or do you?): class (Commutable' a b c d, Commutable' a d c b) => Commutable a b c d | a b c -> d, -- 2. a d c -> b -- based on 1. + 2. Cheers, Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm
On Fri, May 26, 2006 at 08:39:28PM -0700, oleg@pobox.com wrote:
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.
I guess what hasn't been addressed is the question I didn't know to ask... I want the return type "d" to be a phantom type of some sort (although I'm not clear on the distinction between phantom and existential types). Ordinarily I'd do this with a GADT, which gives me a type that can't match any other. This at least is "safe", but what I want is to relax this constraint. So I'd like to return an existential type which contains the constraint enforces this class. (And I think I'm expressing this very poorly!) In short, I don't want to have to explicitely list which phantom types commute, since the "a b" in Patch a b *will* be phantom, existential types, so (as you say below) we can't list these instances explicitely:
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
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:
Indeed, we definitely need to determine commutation dynamically, but I'd like once that has been determined to be able to use the results statically (see below).
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:
I remember that email. I ended up discarding the idea, when I realized that the problem could be solved much more elegantly using GADTs as a type witness (with unsafeCoerce#, admittedly), so that I don't need to explicitely cast types. I'm hoping that if we can come up with a static solution to this (new) problem, I can again use GADTs to convert the static solution to a dynamic one. (Sorry if I'm being unclear... I suppose that's why I need to ask for help, since I'm not sure what's possible or if possible how it'd be done...) -- David Roundy http://www.darcs.net
Can someone explain to me why this doesn't work?
{-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-} module MPTC where
class C a b c d | a b c -> d, a d c -> b
instance (C a b c d) => C a d c b
data P a b = P deriving (Show)
data CommuteResult a b c where CR :: C a b c d => (P a d, P d c) -> CommuteResult a b c
commute :: (P a b, P b c) -> CommuteResult a b c commute (P, P) = CR (P, P)
test (x,y) = do CR (y',x') <- return $ commute (x,y) CR (y'', x'') <- return $ commute (x,y) CR (x''',y''') <- return $ commute (y',x'') return ()
By my logic, it seems that if x :: P a b y :: P b c then y' and x'' must have types y' :: C a b c d => P a d x'' :: C a b c e => P e c but the functional dependencies of C tell us that e and d must be the same type, so the code should typecheck (which it doesn't)! I'm thinking that either the functional dependency constraint is weaker than I thought, or that somehow GADTs aren't interacting with FDs as I'd like, but I'm not sure which. Or, of course, it may be that my recursive instance is not doing what I like. Or I may be just plain confused, as is pretty clearly the case... -- David Roundy http://www.darcs.net
I'm thinking that either the functional dependency constraint is weaker than I thought, or that somehow GADTs aren't interacting with FDs as I'd like, but I'm not sure which. Or, of course, it may be that my recursive instance is not doing what I like. Or I may be just plain confused, as is pretty clearly the case...
The interaction between FD and GADTs is not very good, in our experience.
Hopefully this will be fixed at some point. But in the mean time, what we
ended up doing is to use GADTs instead of classes and FDs:
data Eq a b where refl_eq :: Eq a a
data Commute a b c d where
On Sat, May 27, 2006 at 11:00:43AM -0400, Stefan Monnier wrote:
I'm thinking that either the functional dependency constraint is weaker than I thought, or that somehow GADTs aren't interacting with FDs as I'd like, but I'm not sure which. Or, of course, it may be that my recursive instance is not doing what I like. Or I may be just plain confused, as is pretty clearly the case...
The interaction between FD and GADTs is not very good, in our experience. Hopefully this will be fixed at some point. But in the mean time, what we ended up doing is to use GADTs instead of classes and FDs:
data Eq a b where refl_eq :: Eq a a
data Commute a b c d where
-- Lemma that says that D is uniquely defined by A, B, and C. Comm_unique :: Commute a b c d -> Commute a b c d' -> Eq d d' -- Proof. Comm_unique p1 p2 = ...
It seems like the trouble with this sort of lemma is that it looks like you'd have to explicitly invoke it, which seems like an awful lot of work... I had been hoping that using class trickery, or some sort of type trickery, I could encode a set of properties that were automatically known by the type-checker. Sadly, the properties we're now talking about are the "easy" ones, and I had hoped that if they could be verified by the compiler, it would make it easier to prove the trickier patch properties! :( I'm beginning to suspect that what I want just isn't possible with Haskell in its current state. As Oleg points out, it could be done with FDs and classes, if we were willing to pass around explicit proof objects and run type coersion functions, but that seems awfully tedious--particularly when these "easy" properties are ones that we can do safely with no coersion required, and the motivation is to work towards making it easier to verify more difficult properties, which I fear would require a whole spaghetti of coersions. Ah well. I suppose can just slog along without these features until ghc 6.8 comes along with classes and GADTs living in harmony... I guess I've gotten spoiled by the nice checking I'm already able to do with just GADTs.
The problem is that in your case it seems that you do not want to explain to the type checker how D depends on A B C: you just want to say that it's uniquely defined. But maybe you can get away with:
data Eq a b where refl_eq :: Eq a a data Commute a b c d -- No axioms provided to Haskell. -- Lemma that says that D is uniquely defined by A, B, and C. Comm_unique :: Commute a b c d -> Commute a b c d' -> Eq d d' -- The proof is not given either. Comm_unique p1 p2 = undefined
When you'll do a case on "Comm_unique a b" (which will tell the type checker that D and D' are one and the same) you'll just want to make sure that Haskell doesn't try to look at the `refl_eq' value.
I don't see how this gives us any safety. What guarantee would we have that a Commute a b c d actually corresponds to the result of a commute function? i.e. couldn't one use Comm_unique (undefined :: Commute Int Int Int x) (undefined :: Commute Int Int Int y) to prove that arbitrary types are identical? -- David Roundy http://www.darcs.net
participants (4)
-
David Roundy -
oleg＠pobox.com -
Stefan Monnier -
Tom Schrijvers