[Haskell-cafe] Free theorems for dependent types?

[Conor McBride]

Hi

Questions of parametricity in dependent types are made more
complex by the way in which the "Pi-type"

   (x : S) -> T

corresponds to universal quantification. It's good to think
of this type as a very large product, tupling up individual
T's for each possible x you can distinguish by observation.
"For all x" here means "For each individual x".

By contrast, your typical universally quantified type

   forall x. t

gives you fantastic guarantees of ignorance about x! It's
really a kind of intersection. "For all x" here means
"For a minimally understood x" --- your program should work
even when x is replaced by a cardboard cutout rather than
an actual whatever-it-is, and this guarantees the
uniformity of operation which free theorems exploit.
I'm reminded of the Douglas Adams line "We demand rigidly
defined areas of doubt and uncertainty.".

In the dependent case, how much uniformity you get depends
on what observations are permitted on the domain. So what's
needed, to get more theorems out, is a richer language of
controlled ignorance. There are useful developments:

   (1) Barras and Bernardo have been working on a dependent
     type system which has both of the above foralls, but
     distinguishes them. As you would hope, the uniform
     forall, its lambda, and application get erased between
     typechecking and execution. We should be hopeful for
     parametricity results as a consequence.

   (2) Altenkirch, Morris, Oury, and I have found a way
     (two, in fact, and there's the rub) to deliver
     quotient structures, which should allow us to specify
     more precisely which observations are available on a
     given set. Hopefully, this will facilitate parametric
     reasoning --- if you can only test this, you're bound
     to respect that, etc. My favourite example is the
     recursion principle on *unordered* pairs of numbers
     (N*N/2).

     uRec :
     (P : N*N/2 -> Set) ->
     ((y : N) -> P (Zero, y)) ->
     ((xy : N*N/2) -> P xy -> P (map Suc xy)) ->
     (xy : N*N/2) -> P xy

     Given an unordered pair of natural numbers, either
     one is Zero or both are Suc, right? You can define
     some of our favourite operators this way.

     add  = uRec (\ _ -> N) (\ y -> y) (\ _ -> Suc . Suc)
     max  = uRec (\ _ -> N) (\ y -> y) (\ _ -> Suc)
     min  = uRec (\ _ -> N) (\ y -> y) (\ _ -> id)
     (==) = uRec (\ _ -> Bool) isZero (\ _ -> id)

     I leave multiplication as an exercise.

     The fact that these operators are commutative is
     baked into their type.

To sum up, the fact that dependent types are good at
reflection makes them bad at parametricity, but there's
plenty of work in progress aimed at the kind of information
hiding which parametricity can then exploit.

There are good reasons to be optimistic here.

All the best

Conor