3 ms·

Exactly! Maybe you've seen them before but what you just wrote are so-called "copatterns". See: https://www.cs.mcgill.ca/~bpientka/papers/unnesting-copatterns-

Exactly! Maybe you've seen them before but what you just wrote are so-called "copatterns". See: https://www.cs.mcgill.ca/~bpientka/papers/unnesting-copatterns-2015.pdf https://www.cs.mcgill.ca/~bpientka/papers/unnesting-copatter... https://doi.org/10.1017/S0956796819000182 https://doi.org/10.1017/S0956796819000182 https://agda.readthedocs.io/en/latest/language/copatterns.html https://agda.readthedocs.io/en/latest/language/copatterns.ht... Agda even has extra sugar on top for postfix projectors: you could write `myPair .ProjL` (as expression and as copattern). Syntax for pattern-matching anonymous function crucially uses that (yup, we have multi-clause anonymous functions!). You'd write: introProduct f g z .ProjL = f z introProduct f g z .ProjR = g z or introProduct = λ { f g z .ProjL → f z ; f g z .ProjR → g z } Note that most languages already have that "codata" thing but it's usually called "record" or "struct".

guerrilla 6y ago
I only found Setzers slides on this yesterday after trying to figure this out as I haven't been keeping up on Agda. So this is basically "copattern" matching on record projections. Records/structs are then the dual of variants/emums where we name and type the the destructors instead of the constructors. Thank you for confirming it. Agda's syntax then is meant to mimick descendants of C a little bit with that dot. I'm still fuzzy but it seems like this can be directly translated into an underlying term rewriting system and would just work almost unmodified and all we've done is opened a second route for type checking terms based on orthogonal conditions? I'll have a look at the nested copatters paper as that probably answers my question. Thank for the resources. They seem much clearer than my search results. I wonder why people don't start explaining codata with records instead of coNats and coLists. The latter was confusing.

guerrilla 6y ago

I only found Setzers slides on this yesterday after trying to figure this out as I haven't been keeping up on Agda. So this is basically "copattern" matching on record projections. Records/structs are then the dual of variants/emums where we name and type the the destructors instead of the constructors. Thank you for confirming it. Agda's syntax then is meant to mimick descendants of C a little bit with that dot. I'm still fuzzy but it seems like this can be directly translated into an underlying term rewriting system and would just work almost unmodified and all we've done is opened a second route for type checking terms based on orthogonal conditions? I'll have a look at the nested copatters paper as that probably answers my question. Thank for the resources. They seem much clearer than my search results. I wonder why people don't start explaining codata with records instead of coNats and coLists. The latter was confusing.