[Agda] Pie in the sky

[Alan Jeffrey]

Hmm, it tuns out you can get tantalizingly close to being able to code 
up default arguments in existing Agda.  See the attached file, which 
defines a function whose type in the below syntax is:

   ex : (?0 : Nat) -> Nat -> Nat

and can be used, for example with the default value:

   map ex [ 37 ]

or we can override the default, using angle-brackets to indicate an 
override:

   ex < 5 > 37

Rather annoyingly, it doesn't infer a type for:

   ex 37

which is something weird about when inference can deduce that an 
expression has function type -- apparently just being applied to a value 
is not enough!

Note, this is for the version where defaults are typed at 
declaration-time, not usage-time.  Oh, and the surface syntax is 
rubbish, I only did the non-dependent level-monomorphic version, etc. etc.

Perhaps we don't need a language extension after all...

A.

On 09/25/2010 09:29 PM, Jeffrey, Alan S A (Alan) wrote:
> 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.
>

-------------- next part --------------
open import Data.Bool
open import Data.Nat
open import Data.List

module Defaults where

data Just (A : Set) : Set where
  just : A → (Just A)

-- Only doing the non-dependent, level-monomorphic version right now

Default' : (A B C : Set) → Bool → Set
Default' A B C true  = Just (A → B → C)
Default' A B C false = (B → C)

Default : (A B C : Set) → Set
Default A B C = {b : Bool} → (Default' A B C b)

default : {A B C : Set} → A → (A → B → C) → (Default A B C)
default a f {true}  = just f
default a f {false} = f a

_⟨_⟩_ : {A B C : Set} → (Just (A → B → C)) → A → B → C
just f ⟨ a ⟩ b = f a b

-- Example: a binary function on integers with default value zero.

ex : Default ℕ ℕ ℕ
ex = default 0 (_+_)

-- Use the default value

ex0 : ℕ → ℕ
ex0 = ex

-- Override the default value

ex1 : ℕ
ex1 = ex ⟨ 5 ⟩ 37

-- Grumble mutter doesn't do inference properly

ex2 : ℕ
ex2 = ex 37

-- Does do inference property when put in a function-only position

ex3 : List ℕ
ex3 = map ex [ 37 ]