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 <[email protected]>: > 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 > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe > -- Eugene Kirpichov Web IR developer, market.yandex.ru _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
