[Agda] Foundations of copatterns [Re: The joys and sorrows of abstraction]

[Andreas Abel]

 > (The co-patterns of Andreas et al are also very good for making
 > readable definitions; I’m not so sure if they have firm foundations —
 > pardon my ignorance.)

Andy,

concerning foundations of copattern matching, there is a forthcoming 
ICFP paper by Jesper Cockx and me

   http://www.cse.chalmers.se/~abela/lhs-checking-submitted.pdf

that describes the transformation of dependent copattern matching into 
case trees.

The second step, going from case trees to "introducers" for coinductive 
types hasn't been formally described.  This would require a description 
of productivity checking without sized types.  The foundational question 
for sized types has not been fully settled for dependent types, but see 
my work on non-dependent types...

Best,
Andreas

On 17.05.2018 09:18, Andrew Pitts wrote:
> On 16 May 2018 at 22:24, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
>> One good thing about Agda is that it can be very readable, if you write
>> well.
> 
> For me this aspect of Agda is very important and why I have ended up
> using it. Access to dependent pattern matching is a crucial part of
> what makes it so nice. And even if Agda does not do it that way for
> historical reasons, we do apparently have a good account of
> elaborating such patterms to elimation combinators. (From what I
> understand, this is used by Lean to translate code with patterns back
> into its core type theory.)
> 
> (The co-patterns of Andreas et al are also very good for making
> readable definitions; I’m not so sure if they have firm foundations —
> pardon my ignorance.)
> 
> Andy
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 


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

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/