The Coq mailing list

[Amin Timany <amintimany AT gmail.com>]

Dear Michael,

Sorry for the late reply.

> On 17 Dec 2014, at 16:09, Soegtrop, Michael 
> <michael.soegtrop AT intel.com>
>  wrote:
> 
> Dear Amin,
> 
> thanks a lot for your very detailed answer! It contains a lot of 
> interesting ideas/hints/pointers. But it also brings up a few more 
> questions:
> 
> 1.) Partly this seems to be a problem of simplification of fixpoints. The 
> type terms generated by the fixpoint are huge and ugly, but when I do a 
> compute on them, they become very small and nice. One thing I couldn't find 
> in Gallina is a function to do reductions on a term. I know it should never 
> make a logical difference, but especially with large developments, it could 
> make a significant performance difference, if I could do reductions of 
> terms at Gallina level. I also think that it would solve the problem here 
> (except for the nesting depht problem).

In gallina, you can use the following command:

Definition x := Eval tac in y.

Where tac is a computation tactic, e.g., simpl, cbv, compute, etc. 
Unfortunately, this construction is only at the level of gallina and not 
terms. So,

Definition x := z (Eval tac in y).

will generate a parsing error!

> 
> 2.) Is the Type Class mechanism considered to be part of Gallina or outside 
> of it at the vernacular / tactics level? In the first case, does the 
> implementation of Type Class instance search with eauto mean that the Type 
> Class feature breaks the parametricity feature of Gallina?

As far as I know, type class system is a big sub system and involves gallina 
(Class X := {A : B}.) vernacular (typeclasses eauto := debug) and tactics 
("typeclasses eauto” is a tactic that tries to resolve a goal using typeclass 
resolution). I don’t know what you mean by parametricity feature of gallina.

> 
> 3.) Is the instance search an easily decidable problem?

Type class resolution involves unification and in case of dependent types 
should be undecidable. Unless if they have in some ways restricted it to keep 
it decidable. 

> 
> Best regards,
> 
> Michael
> 

Regards,
Amin