[Agda] Externally vs internally consistent exensions of Agda

[Alan Jeffrey]

On 10/21/2011 07:48 AM, Nils Anders Danielsson wrote:
> On 2011-10-11 03:20, Alan Jeffrey wrote:
> Cheating? I'd say the important question is whether you get guarantees
> that are strong enough for your intended purpose, and I guess the answer
> isn't always the same.

Indeed. There are (at least) two possible goals: run-time safety (memory 
safety, maintaining program invariants, not inhabiting empty types, etc) 
and external equivalence (e.g. correctness of compiler optimizations). 
I'm primarily interested in the former, but I can understand that people 
might expect beta-eta equivalence to imply observable equivalence.

> Your question made me think of QuickCheck. The Arbitrary monad doesn't
> satisfy the monad laws if you interpret equality as ordinary
> observational equality (because the monad uses random numbers), but
> presumably it satisfies the monad laws for some other, reasonable notion
> of equality.

Hmm, it may be that there's a way of thinking about program semantics in 
terms of underspecification. Normally underspecification is modeled as 
nondeterminism, but this would be a restricted form of nondeterminism 
which is modeled as being resolved at top level, and so the execution of 
a program is deterministic.

A.