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

Hi On 20 May 2009, at 07:08, Eugene Kirpichov wrote:

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.

Unordered sets or bags? Both are interesting, but hiding multiplicity makes sets tricky. Anyway, the news on publications is not so good. There's a paper "Observational Equality, Now!" by Altenkirch, McB, Swierstra which describes more or less how we handle observational equalities in general, but the specific instantiation of that pattern to quotients is more recent. An older paper "Constructing Polymorphic Programs with Quotient Types" by Abbott, Altenkirch, McB, Ghani extends container theory to things which are fuzzy about position (bags, cycles, etc), so may have some relevance. One formulation of quotients in Epigram 2, by the aforementioned Altenkirch, Morris, McB, Oury, are sadly documented only by the source code of the implementation, which you can find here http://www.e-pig.org/darcs/epigram/src/Quotient.lhs if you're curious. We knocked that up in about half an hour one afternoon shortly before the money ran out. The basic idea is terribly simple. A quotient is an abstract type X/f wrapping a carrier set X which has a notion of normal form given by f : X -> Y, for some Y. (e.g. f might be even, and Y Bool, giving arithmetic modulo 2). Equality on X/f is just equality at Y of whatever f gives on the packed C values. You can almost unpack X/f freely, gaining access to the element of the carrier, applying any (possibly dependent) function g you like to it -- just as long as you can prove that forall x x'. f x == f x' -> g x == g x' Any such g on X readily lifts to X/f. This to design and redesign an interface of quotient-respecting functions and then work compositionally. Amusingly, under certain circumstances, the idea of quotient by an equivalence fits this picture: given R : X -> X -> Prop, just take Y, above, to be X -> Prop (a predicate describing an equivalence class; predicates are equal by mutual inclusion). That allows you permutative quotients which don't admit a more concrete normal form, like general unordered pairs. Of course, if you do have an order on the data, you can just take f to be sort! Sorry for lack of writings, for which this status dump is poor compensation. Things aren't very applied yet, but the machinery for restricting observation in exchange for guarantees is on its way. We'll see what the summer brings. All the best Conor

Free theorem's are theorems about functions that rely only on parametricity. For example, consider any function f with the type forall a. a -> a

From its type, I can tell you directly that this theorem holds: forall g :: A -> B, x :: A, f (g x) = g (f x)

(Note that the f on the left is B -> B, the f on the right is A -> A). The term was popularized by Philip Wadler, in his paper "Theorems for Free!" [1]. He noticed that many of the properties of functions that one likes to prove come "for free" from their parametric type. For example, it's useful to know that reverse (map fromEnum xs) == map fromEnum (reverse xs) But this theorem comes for free from the type of reverse! Given any - f :: forall a. [a] -> [a] - g :: A -> B - xs :: [A] we have the free theorem - f (map g xs) = map g (f xs). What this is saying is that any function (forall a. [a] -> [a]) can't do a whole lot; it can inspect the structure of the list it has been given, and rearrange, duplicate, and/or remove some elements. But the output list can only contain elements from the input list, without inspecting the elements themselves. Therefore, if f [1,2,3] == [1,1,2] then f "abc" == "aab" and f [True, True, False] == [True, True, True] and f [ [], [1], [1,2] ] == [ [], [], [1,2] ] and so on. Therefore mapping some pure function over the result can be done before or after applying f; and we don't have to know *anything* about f, aside from its type, to prove this. -- ryan [1] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.9875 On Sun, May 17, 2009 at 7:51 PM, Joe Fredette wrote:

This word has piqued my interest, I've hear it tossed around the community quite a bit, but never fully understood what it meant. What exactly is a 'free theorem'?

Eugene Kirpichov wrote:

...

Hello,

Is there any research on applying free theorems / parametricity to type systems more complex than System F; namely, Fomega, or calculus of constructions and alike?

This seems very promising to me for the following reason: Take the free theorem for 'sort::(a->a->Bool)->[a]->[a]'. The theorem could possibly be a lot more powerful if there were a way to encode in the type of 'sort' that it accepts a reflexive transitive antisymmetric predicate, but the only way to express that is with dependent types.

Looks like the only thing one needs to add to System F is the relational translation rule for a dependent product; but I haven't tried doing it myself.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Or in a language without bottoms. 2009/5/20 David Menendez :

On Sun, May 17, 2009 at 11:52 PM, Ryan Ingram wrote:

...

Free theorem's are theorems about functions that rely only on parametricity.

For example, consider any function f with the type   forall a. a -> a

...

From its type, I can tell you directly that this theorem holds:  forall g :: A -> B, x :: A,      f (g  x) = g (f x)

(Note that the f on the left is B -> B, the f on the right is A -> A).

Note also that the theorem only holds in a strict language (i.e., not Haskell).

data A = A deriving Show data B = B deriving Show

f :: a -> a f = const undefined

g :: A -> B g = const B

*Main> f (g A) *** Exception: Prelude.undefined *Main> g (f A) B

-- Dave Menendez http://www.eyrie.org/~zednenem/ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Eugene Kirpichov Web IR developer, market.yandex.ru

Thanks, at least the title looks like exactly what I've been looking for, however I cannot quickly appreciate the notation-heavy contents: I definitely will as soon as possible. 2009/5/20 Masahiro Sakai :

From: Eugene Kirpichov Date: Sun, 17 May 2009 23:10:12 +0400

...

Is there any research on applying free theorems / parametricity to type systems more complex than System F; namely, Fomega, or calculus of constructions and alike?

You may be interested in this: "The Theory of Parametricity in Lambda Cube" by Takeuti Izumi http://www.m.is.sci.toho-u.ac.jp/~takeuti/abs-e.html#cube

-- Masahiro Sakai _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Eugene Kirpichov Web IR developer, market.yandex.ru