[Haskell-cafe] Free theorems for dependent types?
Eugene Kirpichov
ekirpichov at gmail.com
Wed May 20 02:08:06 EDT 2009
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
More information about the Haskell-Cafe
mailing list