[Agda] Termination not being proven

[Will Sonnex]

Hi Nils,

Thanks for the response, very enlightening.

> No. Your programs could contain arbitrary ill-founded code:
>
>  inhabited : {A : Set} → A
>  inhabited = inhabited
>
> Using inhabited one can prove anything (which fits in Set).

I realise why one must have termination checking in Agda, but I'm only
disabling it for Haskell code that has been mapped to Agda. You could
certainly produce this function by expressing it in Haskell but my
proofs will only ever use this mapped Haskell in a computation sense,
never to represent a proof.

Is there a way in Agda to define an arbitrary subset of Set, say
"Hask" for Haskell types. One could use this to accept potentially
non-terminating values and then even if one could define "inhabited :
{A : Hask} →A", it could only ever be applied to other Hask types. As
long as we did not take inhabitance of a Hask type to be a sound proof
I think (tentatively) that the overall system would be sound.


> If you want to ensure soundness, then you need to represent partial
> functions in some "safe" way, for instance by introducing a term
> representation for a partial language, or by using the partiality monad.

This looks very useful.


Thanks again,

Will