[Haskell-cafe] Free theorems for dependent types?

[Eugene Kirpichov]

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 <conor at strictlypositive.org>:
> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



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