[Agda] Pie in the sky

[Alan Jeffrey]

On 09/25/2010 12:22 AM, Samuel Gélineau wrote:
> 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?

Let's say you put the default argument into the function itself, rather 
than the function's type, something like:

   lambda {x ? M : T} -> N  with type  {x : T} -> U

then eta-beta-equivalence gives:

   lambda {x ? M : T} -> N
     =eta= lambda {x : T} -> ((lambda {x ? M : T} -> N) x)
     =beta= lambda {x : T} -> N

and oh dear, the default has disappeared.  Eta-beta on functions is so 
hard-wired into dependent type theory that I'd be worried about messing 
with it.

And yes, you'd need (foo f) in your example not to typecheck.  Let's say 
foo = lambda g -> M -- this gets its implicit parameters resolved at 
compile time, say to give lambda g -> M'.  But M[f/g] would resolve the 
implicit parameters differently, so we'd have foo f having different 
semantics than M[f/g], thus breaking beta-equivalence.

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

Hmm, that's interesting -- a type (? d : A), I hadn't thought of it that 
way round.  I'm not sure how it would interact with the constraint 
satisfaction algorithm for type inference -- when given a constraint X : 
(? Y : Z), at what point do you transform this to the constraints X = Y, 
X : Z?

If the primitive is {x ? M : T} -> U, then the point that M is 
introduced is the point at which the constraint satisfaction algorithm 
decides that an implicit argument needs to be introduced.  (Which it 
must be said is slightly mysterious to me, and indeed I've caught the 
type inference system being rather opportunistic about introducing 
implicit arguments before.)

> 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

A.