[Agda] generative thunk?

[Conor McBride]

Folks

Just to finish the thought.

Here's that wrong'un (already copied to the tracker).

On 30 Dec 2010, at 11:43, I wrote:

> The obvious expedient of defining one copy of thunk
> and using it instead falls foul of the termination checker: if I'm  
> lucky, it
> just moans in the usual miserable way, forcing me to expand  
> definitions I'd
> rather keep tidy. I have an unlucky example which I'm trying to cut  
> to the
> minimum, but it locks my emacs every time.

Note that I have been able to work around this problem, but the
resulting code is unreadable.

All the best

Conor


{-# OPTIONS --universe-polymorphism #-}

module DThunk where

{- This file causes hanging. The trouble is not clear. -}

import Level

------------------------------------------------------------------------
-- A type used to make recursive arguments coinductive

postulate
   Lazy : forall {a} (A : Set a) -> Set a
   thunk : forall {a} {A : Set a} -> A -> Lazy A
   force : forall {a} {A : Set a} -> Lazy A -> A

{-# BUILTIN INFINITY Lazy #-}
{-# BUILTIN SHARP thunk #-}
{-# BUILTIN FLAT force #-}

data Protocol : Set1 where
   D : Lazy Protocol -> Protocol
   PI SG : (S : Set)(T : S -> Protocol) -> Protocol
   _*_ : Protocol -> Protocol -> Protocol

{- I made this definition because it's the "tomorrow idiom",
    accidentally hiding a generative thunk. -}

!> : Protocol -> Protocol
!> P = D (thunk P)

record One : Set where constructor <>

record Sg (S : Set)(T : S -> Set) : Set where
   constructor _,_
   field
     fst : S
     snd : T fst
open Sg public

Step : (Protocol -> Set) -> Protocol -> Set
Step F (D P) = F (force P)
Step F (PI S T) = (s : S) -> Step F (T s)
Step F (SG S T) = Sg S \ s -> Step F (T s)
Step F (P * Q) = Sg (Step F P) \ _ -> Step F Q

Now : Protocol -> Set
Now P = Step (\ _ -> One) P

Anon : (P : Protocol) -> Now P -> Protocol
Anon (D P) _ = force P
Anon (PI S T) f = PI S \ s -> Anon (T s) (f s)
Anon (SG S T) p = Anon (T (fst p)) (snd p)
Anon (P * Q) pq = Anon P (fst pq) * Anon Q (snd pq)

data [_] (P : Protocol) : Set where
   _,_ : (p : Now P)(ps :  Lazy [ Anon P p ]) -> [ P ]

now : {P : Protocol} -> [ P ] -> Now P
now (n , p') = n

anon : {P : Protocol}(p : [ P ]) -> Lazy [ Anon P (now p) ]
anon (n , p') = p'

{- Here's the problem setup. I used !> rather than D (thunk ..) in
    the definition of the time-sliced function space. -}

_-o_ : Protocol -> Protocol -> Protocol
P -o Q = SG (Now P -> Now Q) \ f ->
          !> (PI (Now P) \ p -> Anon P p -o Anon Q (f p))

_/_ : forall {S T} -> [ PI S T ] -> (s : S) -> [ T s ]
f / s = now f s , thunk (force (anon f) / s )

pi1 : forall {S T} -> [ SG S T ] -> S
pi1 p = fst (now p)

{- Now, including the following definition makes something hang
    rather nastily. If you comment out the following, the checker
    does respond, and it complains that -o is not productive, as
    it won't look through the definition of !> -}

{--}
_$_ : {P Q : Protocol} -> [ P -o Q ] -> [ P ] -> [ Q ]
_$_ {P}{Q} f p =
   pi1 f (now p) , thunk ((force (anon f) / now p) $ force (anon p))
{--}

{- If you expand !> as D (thunk ..), invoking more generativity,
    the file checks ok. -}