[Agda] Just getting into dependent typing

[Nils Anders Danielsson]

On Mon, Feb 25, 2008 at 6:22 PM, Luke Palmer <lrpalmer at gmail.com> wrote:
>
>   mapMaybe : {a b : Set} -> (a -> b) -> Maybe a -> Maybe b
>   mapMaybe f m = if (isJust m) then Just (f (fromJust m)) else Nothing

This definition does not type check. If you load it up in the Emacs
interface you will see that parts of the expression are yellow. This
means that there are some unsolved meta-variables; Agda has not been
able to infer all of the implicit arguments.

In batch mode Agda prints out "Unsolved metas at the following
locations: [...]". Unfortunately nothing is printed out in the agda -I
mode. I have added a bug report.

> how
>  would an experienced dependent typer implement an if construct which
>  communicates its condition to its branches (if possible)?

Using the dependent eliminator for booleans. In fact your
if_then_else_ /is/ the dependent eliminator for booleans, but you
can't expect Agda to infer the P argument automatically.

[I see now that Ulf has already answered. Oh well...]

-- 
/NAD