[Agda] Just getting into dependent typing

[Luke Palmer]

Hi Everybody,

First I'd like to say that Agda is a very cool piece of software.
After seeing some of the things it and related software like Epigram
can do, I'm convinced that given 20 years, such features might make it
into mainstream languages.  :-)

I've read a bunch of the examples, and to get my hands dirty, I tried
to write a simple if function which propogates its condition to the
cases.  But I've been unable to get it to work, and more worrying, it
seems that things are typechecking which should not.  I'm looking for
some help finding out where the gaps in my understanding of dependent
types are.  Here's a sketch of my code:

Absurd, Unit, Bool, Maybe defined as expected.

  Pred : Bool -> Set
  Pred True  = Unit
  Pred False = Absurd

  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

  {- 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}
  -}

  isJust : {a : Set} -> Maybe a -> Bool
  isJust (Just _) = True
  isJust Nothing = False

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

  mapMaybe : {a b : Set} -> (a -> b) -> Maybe a -> Maybe b
  mapMaybe f m = if (isJust m) then Just (f (fromJust m)) else Nothing

Obviously mapMaybe could be written better using case analysis, but
the point of the exercise was not to.

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)?

Thanks,
Luke