The Coq mailing list

[Bas Spitters <b.spitters AT cs.ru.nl>]

Dear Hugo,

On Friday 18 March 2005 19:31, Hugo Herbelin wrote:
> * Interestingly, a typical concept that would allow to express the
> expected constraint is the one of "implicit product" described in the
> context of the Calculus of Constructions by Alexandre Miquel (The
> Implicit Calculus of Constructions, TLCA '01).
>
> Roughly, an untyped lambda-term of the form "\x.t" is typable of type
> "!x:A,B(x)", where "!" denotes implicit product, if x does not occur
> in t (i.e. if it is not computationally used).
>
> As for parameters, implicit products in constructors type would not
> enforce universes constraint wrt the inductive itself.
>
> Thanks to implicit products, the expected term and term_rec could then
> be _predicatively_ rewritten into
>
>   Inductive term : Set -> Set :=
>
>   | Var : !A:Set, A -> term A
>   | App : !A:Set, term A -> term A -> term A
>   | Fun : !A:Set, term (option A) -> term A.
>
>   term_rec : forall
>     (P:forall A:Set, term A -> Set)
>     (var_case:!A, forall (a:A), P A (Var A a))
>     (app_case:!A, forall (a b:term A), P A a -> P A b -> P A (App A a b))
>     (fun_case:!A, forall (a:term (option A)), P (option A) a -> P A (Fun A
> a)) (A:Set)
>     (a:term A),
>     (P A a)
>
> Implicit products have not been studied in the context of the Calculus
> of Inductive Constructions though.

It seems that this is possible with the following method that Pierre Letouzey 
and I have used for implicit arguments in program extraction.
We define a monad nc_type, which makes an argument "implicit" by putting it 
in 
Prop. We can than use the usual monadic programming style to work with these 
arguments. (There is a bit more to say about this, but I won't do that now.)

Your example can be done as follows:

Inductive nc_type (A:Type) : Prop := nc : A -> nc_type A.
Implicit Arguments nc.
Notation "t !" := (nc_type t) (at level 50).

 Inductive term : Prop -> Type :=
  | Var : forall A:Set, A! -> term (A!)
  | App : forall A:Set, term (A!) -> term (A!) -> term (A!)
  | Fun : forall A:Set, term ((option A)!) -> term (A!).

However, I understand that in Russell's example the arguments are not really 
implicit.

Best,

Bas