3 got commuteAnd working, marked **Edit**
source | link

I've ended up in deepEdit: (and murky) waterAfter @DerekElkins first comment here.) Scrap all this:

I've ended up in deep (and murky) water. I think my type for Conj needs to be more polymorphic, possiby Impredicative. I've mucked about trying to give a higher rank type:

type Conj p q = Prop (forall r.((p -> q -> r) -> r))

But GHC isn't playing. (And support for Impredicative polymorphism is "flaky".) And a forall-quantified thing like that looks suspiciously like the definition for False/uninhabited that I was expecting to use.

I think mydo need a higher-rank type, but not Impredicative. And not on the type for Conj needs to be more polymorphic, possiby Impredicative. I've mucked about trying to give a higher rank type:but for commuteAnd

typecommuteAnd :: (forall r. Conj p q =r) Prop-> (forallConj r.((q p r')
->- q(same ->function r)for ->`commuteAnd` r)as above)

But GHC isn't playing. (And support for Impredicative polymorphism is "flaky"OK.) And a forall-quantified thing like that looks suspiciously like the definition for False/uninhabited that I was expecting to usecan happily swap arguments ad infinitum.

[End of Edit]

I've ended up in deep (and murky) water. I think my type for Conj needs to be more polymorphic, possiby Impredicative. I've mucked about trying to give a higher rank type:

type Conj p q = Prop (forall r.((p -> q -> r) -> r))

But GHC isn't playing. (And support for Impredicative polymorphism is "flaky".) And a forall-quantified thing like that looks suspiciously like the definition for False/uninhabited that I was expecting to use.

Edit: (After @DerekElkins first comment here.) Scrap all this:

I've ended up in deep (and murky) water. I think my type for Conj needs to be more polymorphic, possiby Impredicative. I've mucked about trying to give a higher rank type:

type Conj p q = Prop (forall r.((p -> q -> r) -> r))

But GHC isn't playing. (And support for Impredicative polymorphism is "flaky".) And a forall-quantified thing like that looks suspiciously like the definition for False/uninhabited that I was expecting to use.

I do need a higher-rank type, but not Impredicative. And not on the type for Conj but for commuteAnd

commuteAnd :: (forall r. Conj p q r) -> (Conj q p r')
-- (same function for `commuteAnd` as above)

OK. I can happily swap arguments ad infinitum.

[End of Edit]

2 corrected the (speculative) code
source | link
type Conj p q r = Prop ((p -> q -> r) -> r)     -- not right, see later

andInj :: Prop p -> Prop q -> Conj p q r
andInj (Prop p) (Prop q) = Prop (\elim -> elim p q)

andElimL :: Conj p q p -> Prop p
andElimL (Prop conj) = Prop (conj axK)    -- axK is `const`
--  commuteAnd :: (Conj p q r) -> (Conj q p r)
    commuteAnd pq = andInj (andElimR pq) (andElimL pq)
type Conj p q = Prop (forall r.((p -> q -> r) -> r))
type Conj p q r = Prop ((p -> q -> r) -> r)     -- not right, see later

andInj :: Prop p -> Prop q -> Conj p q r
andInj (Prop p) (Prop q) = \elim -> elim p q

andElimL :: Conj p q p -> p
andElimL (Prop conj) = Prop (conj axK)    -- axK is `const`
--  commuteAnd :: (Conj p q r) -> (Conj q p r)
    commuteAnd pq = andInj (andElimR pq) (andElimL pq)
type Conj p q = Prop forall r.((p -> q -> r) -> r)
type Conj p q r = Prop ((p -> q -> r) -> r)     -- not right, see later

andInj :: Prop p -> Prop q -> Conj p q r
andInj (Prop p) (Prop q) = Prop (\elim -> elim p q)

andElimL :: Conj p q p -> Prop p
andElimL (Prop conj) = Prop (conj axK)    -- axK is `const`
--  commuteAnd :: (Conj p q r) -> (Conj q p r)
commuteAnd pq = andInj (andElimR pq) (andElimL pq)
type Conj p q = Prop (forall r.((p -> q -> r) -> r))
1
source | link

To explain why I'm uncomfortable with Newsham's and (especially) Piponi's data wrappers ... (This is going to be more question than answer, but perhaps it'll work towards explaining what's wrong with my IsNat even though it seems very similar to Newsham.)

Piponi page 17 on has:

data Proposition = Proposition :-> Proposition
                  | Symbol String
                  | False deriving Eq

data Proof = MP Proof Proof
     | Axiom String Proposition deriving Eq

I see no types here. Spelling a data constructor :-> does not make it function arrow; and spelling a data constructor MP (for Modus Ponens) does not make it function application. There's a 'smart constructor' operator (@@) for MP, but that doesn't apply no function: it merely does pattern matching on the :-> constructor.

Newsham has (I'll start with the Implication section/Modus Ponens):

data Prop p = Prop p

data p :=> q = Imp (Prop p -> Prop q)

impInj :: (Prop p -> Prop q) -> Prop (p :=> q)
impInj p2q = Prop (Imp p2q)

impElim :: Prop p -> Prop (p :=> q) -> Prop q
impElim p (Prop (Imp p2q)) = p2q p

This looks more like it: we have types, function arrows, function application in impElim. The type constructor Imp with its injection and elimination rules mirror the proof tree structures in the Lectures on Curry-Howard isomorphism. But I'm nervous: why does Imp need a type constructor and data constructor? Again, spelling as :=> doesn't make that a function arrow. Why all this wrapping and unwrapping Prop constructors? Why not plain Prop (p -> q)?

So when I look at the 'Conjunction' section (which actually comes first):

data p :/\ q = And (Prop p) (Prop q)

andInj :: Prop p -> Prop q -> Prop (p :/\ q)
andInj p q = Prop (And p q)

andElimL :: Prop (p :/\ q) -> Prop p
andElimL (Prop (And p q)) = p

andElimR :: Prop (p :/\ q) -> Prop q
andElimR (Prop (And p q)) = q

Those Elim functions don't use function application. They merely pattern match on the constructors. There's no implicational structure for conjunction: we rely entirely that the 'programmer' has used only the andInj rule to build a type (p :/\ q).

So when Newsham gets to the commutativity of conjunction:

commuteAnd :: Prop (p :/\ q) -> Prop (q :/\ p)
commuteAnd pq = andInj (andElimR pq) (andElimL pq)

And claims

Notice that our Haskell proof did not contain any reference to the internal structure of the (:/\) data type. Having defined and proven our rules "andInj", "andElimR" and "andElimL" we shouldn't ever have to peek into the implementation of the (:/\) data type again.

I plain disagree:

  • The signature for commuteAnd does rely on the internal structure of the :/\ type constructor.
  • Although the function definition looks like merely function application, in fact the andElims do "peek" into the structure.

I'd expect we could prove the commutativity of conjunction from its definition, without needing an axiom to say so(?)

OK if I'm being so purist, what do I expect? This for conjunction is based on the Church encoding for pair:

type Conj p q r = Prop ((p -> q -> r) -> r)     -- not right, see later

andInj :: Prop p -> Prop q -> Conj p q r
andInj (Prop p) (Prop q) = \elim -> elim p q

andElimL :: Conj p q p -> p
andElimL (Prop conj) = Prop (conj axK)    -- axK is `const`

Now I can write commuteAnd using 'proper' function application:

--  commuteAnd :: (Conj p q r) -> (Conj q p r)
    commuteAnd pq = andInj (andElimR pq) (andElimL pq)

That function definition is the same as Newsham's. But I've commented out the signature because GHC's inferred type is not general enough. It wants Prop ((p -> p -> p) -> p) -> ((p -> p -> p) -> p). Which is only a fancy variation on the Identity law.

I've ended up in deep (and murky) water. I think my type for Conj needs to be more polymorphic, possiby Impredicative. I've mucked about trying to give a higher rank type:

type Conj p q = Prop forall r.((p -> q -> r) -> r)

But GHC isn't playing. (And support for Impredicative polymorphism is "flaky".) And a forall-quantified thing like that looks suspiciously like the definition for False/uninhabited that I was expecting to use.

So my question: if it's legit what Newsham is doing with nesting constructors and pattern matching everywhere, then what's not legit about my IsNat and pattern matching?