[Haskell-cafe] Tutorial: Curry-Howard Correspondence

[Roberto Zunino]

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.