[Agda] Just getting into dependent typing

[Ulf Norell]

On Mon, Feb 25, 2008 at 7:22 PM, Luke Palmer <lrpalmer at gmail.com> wrote:

> Hi Everybody,
>
> Anyway, this compiles fine, but doesn't seem to run fine.
>
> Main> mapMaybe not (Just False)
> _63 not (Just False)
> Main> mapMaybe not Nothing
> _63 not Nothing
>
> I assume that _63 is a variable generated by an implicit argument.
> But shouldn't it fail to compile if it was unable to deduce it?  What
> is yet more distressing is the fact that this implementation of
> mapMaybe compiles:
>
>  mapMaybe' f m = Just (f (fromJust m))
>
> Which shows me that all my if magic was doing nothing.
>
> So two questions:  why is this "incorrect" code compiling, and how
> would an experienced dependent typer implement an if construct which
> communicates its condition to its branches (if possible)?


To command line interface doesn't tell you about unsolved metavariables
unless you ask it (:metas). It probably should. The command line interface
isn't very polished and not actively maintained, you're encouraged to use
the emacs interface instead which has lots more features (and will tell you
about unsolved metas).

Your implementation of if looks fine, but the type checker won't be able to
infer the predicate in all situations (for instance, not in the definition
of mapMaybe). It is also optimistic to hope that the proof argument to
fromJust can be inferred. The only chance of that happening is if it's
blindingly obvious, i.e. you're applying fromJust to Just x for some x.
Metavariable instantiation doesn't do proof search so having a proof of the
right type lying around is not going to help.

If you want to implement mapMaybe using if you can (but it's not pretty):

fromJust : {a : Set}(m : Maybe a) -> Pred (isJust m) -> a
fromJust (Just x) _ = x
fromJust Nothing  ()

mapMaybe : {a b : Set} -> (a -> b) -> Maybe a -> Maybe b
mapMaybe {a}{b} f m =
  (if_then_else_
    { \x -> (Pred x -> Pred (isJust m)) -> Maybe b }
    (isJust m)
    (\prf -> Just (f (fromJust m (prf unit))))
    (\_ -> Nothing)
  ) id

Pattern matching is doing a lot more when you have dependent types than in a
simply typed setting, so trying to do without it often requires significant
effort.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080225/105cf1e5/attachment.html