[Agda] Externally vs internally consistent exensions of Agda

[Nils Anders Danielsson]

On 2011-10-11 03:20, Alan Jeffrey wrote:
> Is this cheating? I hope not, as I really don't fancy having to hide
> everything away under a monad.

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.

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.

-- 
/NAD