[Agda] Pie in the sky

[Thorsten Altenkirch]

On 24 Sep 2010, at 15:38, Alan Jeffrey wrote:

> 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

but we could allow instances of the type for defaults, e.g.

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

which are only used if the application matches the instance. 

This may be useful because your instance may depend on the type (indeed you may want to call a theorem prover using reflection). 

And you would be able to type check at definition time.

T.

> 
> 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.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda