Thanks for the thorough response.
I've found Barras&Bernardo's work (at least, slides) about ICC*, I'll
have a look at it.
Could you provide with names of works by Altenkirch/Morris/Oury/you?
The unordered pair example was especially interesting, since I am
somewhat concerned with which operations do not break parametricity
for *unordered sets* (as opposed to lists) - turns out, not too many.
2009/5/18 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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Eugene Kirpichov Web IR developer, market.yandex.ru