[Agda] Externally vs internally consistent exensions of Agda

[Alan Jeffrey]

Hi everyone,

A question about what are the victory conditions for an FFI binding in 
Agda (or indeed any other extension of Agda's semantics)...

It seems that there's (at least) two notions of conservativity for an 
extension of Agda: an internal notion and a stronger external one.

Internally, we want to ensure we don't inhabit the empty type, and as a 
consequence we want that (for types with decidable equality) if e and f 
are eta-beta equivalent, then (e == f) always evaluates to true. This 
rules out most effects such as nondeterminism, mutable update, etc. 
unless hidden underneath a monad or similar machinery.

Externally, we could define a notion of testing equivalence (or 
bisimilarity if you prefer such things), and require beta-eta to imply 
testing equivalence. I'd expect that under some pretty mild conditions 
for tests, external conservativity is a stronger property than internal 
conservativity.

As a concrete example of the difference (although you may have to 
forgive a sneaky use of divergence here), consider oracle variables as a 
way of taming nondeterminism. The user is provided with a stream of 
oracle variables, and an operation choose : Oracle -> A -> A -> A such 
that choose o a b runs both a and b and returns whichever one converges 
fastest, but memoizes the results such that on it next run choose o c d 
picks the same branch. This is one of the standard tricks for presenting 
nondeterminism in a pure functional language, and (er, not actually done 
the proofs, but it seems to me quite likely) that it is internally 
conservative but not externally conservative.

I'm coming across examples at the moment where I'm pretty confident of 
implementing them in Agda in an internally conservative fashion, but not 
externally conservative (e.g. side-effecting GET requests hidden behind 
a caching proxy that is internally undetectable, but externally you can 
spot the HTTP traffic and other side-effects such as lower latency on 
cache hits).

Is this cheating? I hope not, as I really don't fancy having to hide 
everything away under a monad.

A.