I must confess that I find choosing type Prop = CProp ()
to be slightly dangerous, since now CProp (const ()) :: Prop p and there is nothing in that expression that suggests non-termination (~ "invalid" proof). I would rather choose a type admitting only _|_ as its value: type Prop = CProp (forall a. a) or even the H98 (IIRC) type Prop = CProp Void newtype Void = Void Void Using another approach, I also tried data Prop p = Prop (forall r. (p -> r) -> r) but I was then unable to define propCC. Maybe this is because of the presence of the definable functions iso :: Prop p -> p osi :: p -> Prop p and so definifing propCC amounts to proving Peirce's law. (Still not sure about this...) Regards, Zun. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
