[Haskell-cafe] Free theorems for dependent types?
conor at strictlypositive.org
Mon May 18 04:57:07 EDT 2009
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
(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
More information about the Haskell-Cafe