[Agda] Pie in the sky

[Alan Jeffrey]

Coming in rather late in the conversation, but...

My dream item for default arguments follows, but I'd bet good money on 
it (and indeed any similar proposal for default values) to cause type 
inference to diverge.  Type checking on fully-inferred code will still 
terminate, but that may not be much use if type inference doesn't.

If I were to add a feature to Agda's implicit arguments it would be to 
allow function definitions to give default values, something like the type:

   {x ? M : T} -> U -- M is the default value

with the semantics that M is untyped when the function is declared, but 
typechecked when it is used.  The current case is handled by syntax sugar:

   {x : T} -> U  =def=  {x ? _ : T} -> U

A simple example of why M shouldn't be typechecked at compile time is a 
function with type:

   f : (x y : T) -> {x==y ? refl : x == y} -> U

so in the common case, we can call (f x x) and have "refl" inferred as 
the default.

My real reason for wanting this is for simulating subtyping on 
class-based languages, e.g. the type (c -> ...) becomes:

   {c' : Class} -> {? ok (isSub c' c) : c' <: c} -> (Object c') -> ...

where:

   OK : {A : Set} -> (Dec A) -> Set
   OK (yes a) = A
   OK (no na) = not A
   ok : {A : Set} -> (dec : Dec A) -> (OK dec)
   ok (yes a) = a
   ok (no na) = na
   isSub : (c d : Class) -> Dec (c <: d)
   isSub = ...

You can probably do other things like coercing this way too.

Note that default values are always used, not just when type inference 
fails, which saves a lot of backtracking!

Also note that there aren't scoping issues here, as the default value is 
given by the author of the function type, not the author of the argument 
type.  If you want to simulate the latter, you do it by:

   module M
     T : Set
     T = ...
     default : T
     default = ...

and then declare a function with type {x : M.T | M.default} -> U.

A.