[Agda] Pie in the sky

[Samuel Gélineau]

On 2010-09-24 at 9:44 PM, Alan Jeffrey wrote:
> Yes, but the default is provided by the *type* of f, not by the name of f,
> so when the type inference system deduces the type of f, this will cause new
> implicit arguments to be filled in, which may cause further type inference.

My understanding was that the signature was a nice place to write the
defaults, but that adding them should in no way change the function's
type. If f and g both have the same signature except for their choice
of default, do you really want them to have distinct types? If f has
type ((x y : T) ->  {x==y ? refl : x == y} ->  U) and foo asks for a
value of type ((x y : T) ->  {_ : x == y} ->  U), do you really want
(foo f) not to type-check?


If you do insist on defaults being part of the type, then I have an
alternate proposal for you.

If the types A and (? d : A) really are different, there should be a
mechanism to extract a value of type A from a value v of type (? d :
A). Call this mechanism (val v). There should also be a mechanism to
convert a value of type A into a value of type (? d : A), for those
times when d does not have the right type and you need to pass in a
value x of type A explicitly. Call this mechanism (explicit x). And
while we're at it, let's throw in (implicit p), for those times when
the value p proves that the default value d does have the correct
type.

My proposal is to add two new builtins, (_﹖_∶_) and val, defined as follows.


infix 0 _﹖_∶_
data _﹖_∶_ (CommonA : Set) (default : CommonA) (A : Set) : Set where
  explicit : A → CommonA ﹖ default ∶ A
  implicit : CommonA ≡ A → CommonA ﹖ default ∶ A

val : ∀ {CommonA default A} → CommonA ﹖ default ∶ A → A
val (explicit a) = a
val .{A} {default} {A} (implicit refl) = default


Whenever Agda infers that an omitted parameter x has type (CommonA ﹖
default ∶ A), it would try {x = implicit refl} instead of {x = _}. The
solves a meta without introducing new ones, so it shouldn't affect
termination. Using the new builtins would look as follows.


f : (x y : ℕ) → {x≡y : x ≡ x ﹖ refl ∶ x ≡ y} → suc x ≡ suc y
f x y {x≡y} with val x≡y
f x .x {_} | refl = refl

foo : suc (2 + 3) ≡ suc (1 + 4)
foo = f (2 + 3) (1 + 4)

bar : ∀ x y → x ≡ y → suc x ≡ suc y
bar x y p = f x y {explicit p}


> Could be.  I'm still worried about nontermination.  Of course, we still know
> soundness, because type checking is terminating, and pragmatically there's
> not much difference between nontermination and trying to typecheck a model
> of category theory :-)

I find it funny that we're working in a language where every function
has to pass a termination checker, yet each language extension gets
scrutinized to make sure they are terminating. Somebody should write a
provably-terminating Agda compiler in Agda; this would make it much
easier to ensure that further language extensions preserve
termination.

– Samuel