[Agda] type annotation in-place

[Andrew Pitts]

On 8 October 2015 at 14:48, Nils Anders Danielsson <nad at cse.gu.se> wrote:
> On 2015-10-08 09:39, Andrew Pitts wrote:
>>
>> Is Agda's "abstract" keyword documented/exlained anywhere?
>
>
> Yes, but perhaps not on the wiki.
>
> Once I wrote this:
>
>   The basic idea is that it should be possible to replace the
>   "right-hand sides" of abstract definitions with /anything/ that
>   type-checks, and this should not affect the type-checking of any
>   definition outside of the given "abstract block" in any way.

OK, I get the general idea. But it would be nice to see an explanation
of the semantics of this at a higher level than could be got by
examining the relevant parts of the Haskell code -- I don't suppose
there is one? Ditto for the "private" keyword (which I know from
bitter experience only guarantees a certain amount of privacy, because
of the way Agda pattern matching works
<http://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/#comment-80163>).

More generally, it seems to me that understanding how the classic
theory of abstract data types mixes with dependent type theory is an
interesting topic. Perhaps there are PhD theses on it already of which
I am unaware?

Andy