--- Day changed Mon Feb 26 2018
apostolisIs there a way to automatically construct construct eliminators?26/02 12:08
{AS}apostolis: Yes26/02 12:18
{AS}apostolis: In general there is, but I am not sure there is for Agda26/02 12:19
{AS}apostolis: You could get them for some universe26/02 12:20
{AS}Like https://github.com/larrytheliquid/generic-elim26/02 12:20
apostolisWhat I want to do is transform a function f : (x : A) -> B x into f : B con1 -> B con2 -> (x : A) -> B x26/02 12:22
apostolisI want to glue each case with haskell code.26/02 12:24
{AS}apostolis: where A is defined as con1 | con2?26/02 12:25
apostolis{AS} : Yes.26/02 12:25
{AS}apostolis: so how would you define such transformation?26/02 12:26
{AS}Can you give an example26/02 12:26
{AS}I mean, I am not sure this is possible for an arbitrary function :)26/02 12:26
apostolisHasn't Jesper actually done this?26/02 12:27
{AS}I don't know, maybe someone else knows26/02 12:28
apostolishttps://lirias.kuleuven.be/bitstream/123456789/452283/2/Pattern-matching-without-K-2014-06-05b.pdf26/02 12:30
apostolisI am not an expert, I think this is it.26/02 12:31
apostolisOr I could find another way, trying to find the path of least resistance. :)26/02 12:35
{AS}apostolis: So I mean, McBride have shown that you can elaborate a set of recursively defined functions to functions just using eliminators+K26/02 12:53
jesperWhat do you mean by "automatically construct eliminators"? Do you mean derive the definition of the eliminator from a datatype? Or do you mean translating a function by pattern matching to eliminators?26/02 13:28
jesperMy work is on the latter, but I'm not sure how that would help you in your example since you'd still just have a function f : (x : A) -> B x, only now it's defined by eliminators instead of by pattern matching26/02 13:29
apostolisjesper : the second.26/02 13:29
apostolisI am actually thinking of using reflection. There are other things that I will do as well.26/02 13:31
jesperYou could probably use the eliminator for A to construct an equivalence between "(x : A) -> B x" and "B con1 -> B con2 -> B x" (and then no more (x : A) is needed)26/02 13:32
apostolisIn essence , while session types define a global type that determines locally the implementation, I want to create a global function that is executed differently per local user.26/02 13:32
jesperDoing things like this with reflection seems like a cool idea but so far I've only hardcoded stuff in Haskell :)26/02 13:33
apostolisHardcoded/26/02 13:35
apostolis?26/02 13:35
jesperI mean it's part of the Agda implementation, not using reflection26/02 13:35
apostolisAh, ok.26/02 13:35
jesperSo what you want to do is implement a function on some abstract type A, and then depending on the user you can run it on a different implementation of A. But you still want to do pattern matching on A?26/02 13:36
apostolisA single agent deconstructs the value, performs the pattern matching, then it sends the data to the others.26/02 13:38
apostolisI need to split the function into parts and have each agent execute the correct part.26/02 13:38
apostolisI think it is possible with reflection.26/02 13:39
apostolisMaybe creating eliminators is not necessary after all. I could use reflection to split the function to the correct places.26/02 13:40
jesperWell it depends on how granular you want to split the function26/02 13:40
jesperthe desugaring of pattern matching is basically splitting up a function into single case analyses26/02 13:41
apostolisI am just starting to learn reflection. Reading agda-prelude code to get familiar with it.26/02 13:43
apostolisWith my current understanding of the problem, since a single agent performs the deconstruction, it might be possible to not need to split the function into multiple cases. 26/02 14:08
apostolisWe'll see eventually if this is true.26/02 14:08

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!