[Agda] Termination checking failure

[Nils Anders Danielsson]

On 2009-11-22 23:12, Ivan Tomac wrote:
> Yes, that does work for that particular case. I should have been a bit
> more clear though. The code here is simplified version of the problem I
> ran into before where the above wouldn't work. What happens in a more
> general case for example with an applicative functor instead of Id:
>
> sequence : ∀ {F a} → RawApplicative F → Stream (F a) → F (Stream a)
> sequence A (cons f fs) =
>    cons <$> f ⊛ ((λ as → ♯ as) <$> sequence A (♭ fs))
>    where
>    open RawApplicative A

You cannot do this in the general case. Assume that F is the state
monad, for instance. You cannot compute the resulting state in finite
time.

--
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.