CODEWITHSUNDEEP
haskellproof
Patrick Browne
Patrick Browne

Reputation: 253

How could I prove this type level Haskell theorem?

With respect to Listing 1, how would I go about proving the type level axiom

(t a) = (t (getUI (t a)))

holds?

Listing 1

    data Continuant a = Continuant a  deriving (Show,Eq)
        
    class UI a where -- ...
          
    instance UI Int where -- ...
        
    class Category t  where
      getUI :: (UI a) => (t a) -> a

   instance Category Continuant where
     getUI (Continuant a) = a
        
     -- Does axiom (t a) = (t (getUI(t a))) holds for given types?
     test :: Int -> Bool
     test x =  (Continuant x) == (Continuant (getUI (Continuant x)))

The code is based on a paper where it is stated:

For all implementations of getUI one may require that the axiom (t a) = (t (getUI (t a))) holds. This must be proven to hold for every specific type class instance declaration. For finite types this can be done by a program that enumerates all possibilities. For infinite types this must be done manually via proofs by induction.

My current intuition is that the test function in some way satisfies the axiom, but I do not think that it amounts to a proof.

This question follows on from a previous question.

Upvotes: 1

Views: 191

Answers (1)

luqui
luqui

Reputation: 60463

To prove this, just start with one side of the equation and rewrite until you get to the other side. I like to start with the more complicated side.

when x :: Int,

Continuant (getUI (Continuant x))
    --      ^^^^^^^^^^^^^^^^^^^^
    -- by definition of getUI in Category Continuant Int
    = Continuant x

That was easy! This does count as a proof (mind, not a formally verified one -- Haskell is not powerful enough to express term-level proofs. But it's so trivial it wouldn't be worth the boilerplate in agda.).

I was a bit bewildered by the phrasing of this axiom, since it seems to be mixing up types and terms quite a lot. Skimming the paper, it seems like this is only intended to work for simple single-constructor newtypes, thus this mixing is justified (still odd). Anyway, it seems like the paper doesn't have the Category class parameterized on a: i.e. instead of

class Category t a where ...

it would be

class Category t where ...

which makes more sense to me, that the class describes polymorphic wrappers, rather than a possibly different description of how it wraps each individual type (especially since it appears that the axiom requires the implementation to be the same no matter what a you pick!).

Upvotes: 3

Related Questions