[Agda] Just getting into dependent typing

[Dan Licata]

On Feb25, Luke Palmer wrote:
> 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)?

(1) The "incorrect" code has unsolved metavariables in mapMaybe, namely
the argument to fromJust proving that isJust is True (which you've left
as an implicit argument).  So it doesn't really compile.  You can see
the unsolved metas if you load the file in the emacs mode; I've never
used the command-line mode.

(2) One way to do it is this:

    -- you could make this polymorphic, but this is all we need here
    data Id : Bool -> Bool -> Set where
      Refl : {b : Bool} -> Id b b

    if_/_then_else : (b : Bool) -> (P : Bool -> Set) -> P True -> P False -> P b
    if True  / _ then t else f = t
    if False / _ then t else f = f
    
    isJust : {a : Set} -> Maybe a -> Bool
    isJust (Just _) = True
    isJust Nothing = False
    
    fromJust : {a : Set} -> (x : Maybe a) -> Id (isJust x) True -> a
    fromJust (Just x) p = x
    fromJust Nothing  ()
    
    mapMaybe : {a b : Set} -> (a -> b) -> Maybe a -> Maybe b
    mapMaybe {A} {B} f m = (if (isJust m) / (\b -> Id (isJust m) b -> Maybe B) 
                            then (\ id -> Just (f (fromJust m id)))
                            else (\ _ -> Nothing))
                           Refl

  To use the dependent if-then-else to propogate the appropriate fact,
  you need to choose "P" so that it tells you that the scrutinized
  expression (isJust m) is True/False in the appropriate branch.  You
  can do this using Id.  

  I think it's worth understanding how dependent inductive family elims
  like 'if' work, but it's much more convenient to program with pattern
  matching, rather than isJust/fromJust.  Then Agda progagates lots of
  information for you, eliminating the overhead of coming up with and
  writing down the appropriate P.

Make sense?
-Dan