[Agda] generative thunk?

[Andreas Abel]

Hi Conor,

you are hitting the repercussions of the 2008 Nottingham coup d'etat on 
Agda coinduction.  What exactly is going on here I do not know and do 
not approve, but, roughly:

Every use of a SHARP is translated into a new definition (in your case, 
thunk-6, thunk-7, and thunk-8), and they are considered different. This 
is why zut fails.  fut succeeds because only on instance of thunk is 
created, while the two others are meta-variables which are instantiated 
with the correct instance of thunk.

Nisse had plans to fix this by a structural equality test which 
identifies more terms.  In my view, however, there is neither sufficient 
theory nor consensus for the current approach to coinduction in Agda and 
we need to go back to the drawing board.

Could you file this as an issue on the bug tracker?

Thanks,
Andreas

On 12/30/10 4:14 AM, Conor McBride wrote:
> Hi friends
>
> I'm trying to do something quite involved, but I think the
> problem I'm hitting boils down to some unwelcome generativity.
>
> Let me fix my nonstandard ASCII terminology. (My current editor
> displays all unicode characters as blanks. I rather like this
> feature.)
>
> 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 #-}
>
> OK, now I can write this...
>
> put : (th : Set -> Lazy Set)(P : (Set -> Lazy Set) -> Set) ->
> P th -> P th
> put th = \ P p -> p
>
> ...but if I want to be more specific, I hit trouble.
>
> zut : (P : (Set -> Lazy Set) -> Set) ->
> P thunk -> P thunk
> zut = put thunk -- doesn't check
>
> The error message
>
> .Chat.thunk-6 P x != .Chat.thunk-8 x of type Lazy Set
> when checking that the expression put thunk has type
> (P : (Set → Lazy Set) → Set) →
> P (.Chat.thunk-6 P) → P (.Chat.thunk-7 P)
>
> suggests generativity issues, breaking stability under
> substitution.
>
> Amusingly,
>
> fut : (P : (Set -> Lazy Set) -> Set) ->
> P _ -> P _
> fut = put thunk
>
> does typecheck.
>
> It's a bit troubling.
>
> Any clues as to what's going on?
>
> Cheers
>
> Conor
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/