[Agda] generative thunk?

[Thorsten Altenkirch]

Hi Andreas,

> you are hitting the repercussions of the 2008 Nottingham coup d'etat on Agda coinduction.

Not true. The new mechanism using \infty, \sharp and \fat was initially implemented on top of the old one and hence these issues are not related to the alleged coup. The new scheme did make it easier to use coinduction and in particular mixed inductive/coinductive definitions.

>  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.

Indeed, the mechanism was inspired by our work on PiSigma which indeed features a structural equality avoiding this strange behaviour.

>  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.

I think we are at the drawing board all the time :-).

Apart from the generativity issue, there is an issue with termination checking nested inductive/coinductive definitions. The naive extension of the structural termination checking doesn't work properly for coinductive definitions inside inductive ones. It should be possible to do better here by using parity games (you should have some experts on this nearby) but I haven't had time to think about this.

I realize that you are not so keen on this since you'd rather use sized types anyway.

Cheers,
Thorsten


> 
> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda