[Agda] the joys and sorrows of abstraction.

[Peter Hancock]

On 16/05/2018 21:36, Martin Escardo wrote:
> (many things I heartily endorse).

Like Martin, I find implicit-argument resolution very convenient. I 
don't fully understand how it works, but I figure when it doesn't,
then at least I can write stuff out with (more verbose) Martin-Lof combinators.
(If not, I'll wait for Agda's successor.) On the whole I'm very pleasantly
surprised how well basic things usually seem to work, and the help it gives
in figuring out intricate constructions.

Agda is an experimental language. Great. If it were to become a thoroughly
solid, easy to understand tool one could widely recommend, 
I expect that would be by a process of removing unclear features.

I sometimes wonder though, whether the implementation of reductions
(at least in type-checking) should not bite the bullet and use explicit substitutions.
Could some of the performance issues Phil is running into might not be
so severe if this was done in the right way? After all, the semantics of
type-theory is usually presented in this way, at least by Martin-Lof.
It's hard to believe this is just some elderly theoretician's aberration.
Or is there some reason why solid foundations and practical implementations
should not coincide?

Hank