[Agda] Just getting into dependent typing

[Conor McBride]

Hi folks

Plenty of good replies already, but I thought I'd
poke around with the ideas. A few remarks spring to
mind.

On 25 Feb 2008, at 18:22, Luke Palmer wrote:

>   if_then_else_ : {P : Bool -> Set} -> (b : Bool) -> P True -> P  
> False -> P b
>   if True  then t else f = t
>   if False then t else f = f

You'd have to be pretty lucky to be able to infer
P in the above. You can do it (and Agda will do it)
if you get a constraint like

   P b = T

where b is a variable, so you can readily form the
abstraction \b -> T, but when constraints on P are
more complex, there's no canonical thing to do.
It's better not to let the machine guess,
especially as which programs typecheck are likely
to depend on the computational behaviour of any P
a machine might synthesize.

Note that even the above choice of \b -> T is only
canonical given the eta law for function spaces:
Coq, which has only beta, would not be entitled to
that presumption.

To help people get their heads round dependently
typed programming, we need to tell a clearer story
about how implicit  arguments get inferred: not many
people have well-developed intuition about what it
involves (pattern unification, anyone?). One can only
get so far with trial and error, and it's never
satisfying.

Of course, Epigram synthesizes "motives" like the
above P all the time, but only under very carefully
controlled circumstances which ensure that there's
a sensible choice, corresponding to "just
programming by pattern matching". Language design
moral of story: it's difficult, dangerous, and
expensive to work with dependent elimination schemes
as *expression* forms; it's better to think about
how to construct patterns on the left than about
how to access data on the right. Good old
if-then-else and case expressions are bad news
when you just stick them in anyplace.


>
>   {- I also tried this:
>   if_then_else_ : {a : Set} -> (b : Bool) -> ({_ : Pred b} -> a) ->
> ({_ : Pred (not b)} -> a) -> a
>   if True  then t else f = t {unit}
>   if False then t else f = f {unit}
>   -}

Having said that, the above alternative is
kind of sensible. Don't we get (apologies for
having a broken Agda installation just now, hence
not testing)

   mapMaybe f m =
     if (isJust m)
       then (\{p} -> f (fromJust m {p}))
       else Nothing

? That's to say, we just plumb the proof from
where it's generated to where it's used.

Note: it's no loss to have a *uniform* return
type here, because each branch learns the result
of the test from its extra premise. Not as
pretty as pattern matching, but just as
informative. In fact, you can code pattern
matching that way if you express those premises
as (heterogeneous, in general) equations,
rather than reflecting the result of ad hoc
Boolean testing. That's effectively how Epigram
works, and it shows why "motive synthesis" from
a known result type is an easier problem than
higher-order unification.

There's a serious question here about how to
program with propositional information lying
around, and at the moment, the best answer that's
up and running is Matthieu Sozeau's. His Russell
system at least book-keeps the guarantees
generated by testing and the requirements demanded
by usage, so that the appropriate verification
conditions can be passed to Coq for thumping with
automatic tactics.

This example has good pattern matching
alternatives, but plenty do not: try working with
data in an abstract set with a total order and
trichotomy. You don't get to express "learning"
through refinement of patterns, because the set
is abstract, but you can generate propositional
information by inspecting data from which
requirements can then be discharged. Boring
proof-plumbing happens all over the place.

I think Luke has raised an important point
(although certainly not a new one) which deserves
longer term thought as well as shorter term
workarounds. I suspect that having a universe of
proof irrelevant propositions may be the key to
progress here...

All the best

Conor