ImplicitSyntax

I think that implicit syntax, as it is now in Agda, is too sophisticated. It should not be defined by a new typing system but should be only a syntactic sugar/notation facility on top of the explicit type system.

Here is a simpler approach to implicit syntax, which should be enough. (This is in part inspired by the paper of Necula and Lee on Efficient Representation and Validation of Proofs.)

First we introduce the _ notation so that the user writes _ instead of writing explicitely an argument when he knows the system can infer it without ambiguity. For instance

• id : (A : Set) -> A -> A

one can write id _ zero instead of id Nat zero.

Second, we make the convention that if we write

• f : {x : A} -> {y : B} -> ...

then we declare

• f : (x : A) -> (y : B) -> ...

but when we write f, this is understood as f _ _.

In this way, the ordinary type system is enough, and we have only to explain how to handle the _ symbol.

This mechanism is more restrictive than the one which is implemented now, but easier to understand.

Cons

Nice examples

Examples which cannot be expressed using the restricted version.

Giving names to types:

 Refl : (A -> A -> Set) -> Set
 Refl R = {x : A} -> R x x

 Sym : (A -> A -> Set) -> Set
 Sym R = {x y : A} -> R x y -> R y x

Passing polymorphic functions as arguments...

• in elimination functions:

 elimVec : {A : Set}(P : {n : Nat} -> Vec A n -> Set) ->
           P nil -> ({n : Nat}(x : A)(xs : Vec A n) -> P xs -> P (x :: xs)) ->
           {n : Nat}(xs : Vec A n) -> P xs

• when building sequences of terms:

 Ctx = List Type

 data Terms (Γ : Ctx) : Ctx -> Set where
   ε   : Terms Γ []
   _,_ : Term Γ τ -> Terms Γ Δ -> Terms Γ (τ :: Δ)

 data Var : Ctx -> Type -> Set where
   v0 : Var (τ :: Γ) τ
   vS : forall {Γ σ τ} -> Var Γ τ -> Var (σ :: Γ) τ

 tabulate : {Γ Δ : Ctx} -> ({τ : Type} -> Var Δ τ -> Term Γ τ) -> Terms Γ Δ
 tabulate ...

-- Ulf /NAD

Implicit Syntax (notes from the Language review by Patrik)

Conor: this could be an option:

  Sch ::= Ty | (x : Sch) -> Sch | {x : Ty} -> Sch

  ren : {Γ Δ : Ctx} (r : {τ : Ty} -> Var Γ τ -> Var Δ τ)
      -> {τ : Ty} -> Tm Γ τ -> Tm Δ τ
  ren = ?
  id_ren = ren (\x -> x)

Ulf/Nils Anders: Thierrys suggestion is too limited, but Conors could work.

Ulf: we could experiment with different restrictions - the current system has some problems

Peter: for stability we need to decide what approach to use

Makoto: The current system seems to works, so it is not clear what is gained by restricting it. But the Sch version + some kind of type synonyms is probably enough.

Bengt: I really like the idea of separating the "presentation" (hidden arguments) from the type system.