--- Day changed Thu Apr 20 2017 | ||

glguy | quchen: Did you ever figure out why the rewrite syntax matches on both the lhs and the equality? | 20/04 15:38 |
---|---|---|

quchen | glguy: Unfortunately not. | 20/04 15:38 |

quchen | The question was »how does rewrite work«, right? | 20/04 15:38 |

glguy | Yes. When you put the lhs in a with Agda replaces occurences of that expression in the current context and matches that against whatever you match | 20/04 15:39 |

quchen | rewrite (eq : a = b) -> replace all »a« with »b« in the body, even when »a« is a tree | 20/04 15:39 |

quchen | tree as in not-just-a-simple-atom | 20/04 15:39 |

glguy | *especially* when it's a "tree" | 20/04 15:40 |

glguy | That's when it matters | 20/04 15:40 |

glguy | Because you don't want it to be one | 20/04 15:40 |

glguy | so that when you match on the refl that you can replace a variable representing the lhs with a . pattern | 20/04 15:40 |

quchen | <quchen> f ps rewrite eqn = rhs | 20/04 15:40 |

quchen | <quchen> >>>>> | 20/04 15:40 |

quchen | <quchen> f ps with a | eqn | 20/04 15:40 |

quchen | <quchen> … | ._ | refl = rhs | 20/04 15:40 |

glguy | quchen: to see what it's doing, take some code that uses a rewrite and instead of " … | ._ | refl = rhs" | 20/04 15:41 |

glguy | Look at " … | lhs | eq = ?" | 20/04 15:41 |

quchen | Okay, canonical example: commutativity of addition, succ n + m = succ (n + m) | 20/04 15:42 |

glguy | You'll see that the left-hand side of the equality as it occurs in the context has not be replaced with a simple variable 'lhs' | 20/04 15:42 |

glguy | has now* | 20/04 15:42 |

glguy | has now been* even | 20/04 15:42 |

quchen | Hah, better: associativity. | 20/04 15:43 |

quchen | assoc-+ (succ x) y z rewrite assoc-+-rewrite x y z = refl | 20/04 15:43 |

quchen | assoc-+ (succ x) y z rewrite assoc-+ x y z = refl | 20/04 15:43 |

quchen | That one. | 20/04 15:43 |

glguy | next matching on eq with the constructor 'refl' requires us to be able to replace the lhs pattern with the forced value coming from the refl | 20/04 15:43 |

glguy | so we use a dot pattern to indicate that that pattern's value is forced by matching on something else | 20/04 15:43 |

quchen | So ._ and .refl are identical here? | 20/04 15:44 |

glguy | No, the ._ isn't .refl | 20/04 15:44 |

quchen | Ah right, it’s the LHS | 20/04 15:44 |

quchen | Of the equality | 20/04 15:44 |

glguy | yes | 20/04 15:44 |

quchen | And since it has to unify with refl’s LHS that makes it inferrable | 20/04 15:44 |

glguy | So it's a two step process of abstracting the lhs out of the context and then forcing that to have some value | 20/04 15:45 |

quchen | So we can put the dot there | 20/04 15:45 |

quchen | What if we leave the dot away? | 20/04 15:45 |

glguy | Yeah, not only can we, I think we must use a dot | 20/04 15:45 |

quchen | What links the _ with the refl? | 20/04 15:45 |

glguy | refl's type links it | 20/04 15:45 |

glguy | You can't pattern match on refl unless it's possible to replace the a in (a === b) in the context | 20/04 15:46 |

quchen | Pattern matching on refl still confuses me a bit (so does path induction in HoTT, the two problems are likely related). | 20/04 15:47 |

quchen | For me, (refl : a = b) tells the typechecker to add the substitution (a -> b). | 20/04 15:47 |

quchen | Is that even right? | 20/04 15:47 |

dolio | What are a and b? | 20/04 15:48 |

quchen | Some values ..? | 20/04 15:48 |

dolio | Well then no. | 20/04 15:48 |

quchen | Let me socratize you back and ask: what are a and b? :-) | 20/04 15:48 |

dolio | Matching on an indexed type is only allowed to refine variables, not arbitrary expressions. | 20/04 15:48 |

quchen | »Refinment«, what is that exactly? | 20/04 15:50 |

quchen | What Hindley-Milner often calls »substitution«? | 20/04 15:50 |

dolio | It is like adding your substitutions. | 20/04 15:50 |

quchen | Ah, okay. Common ground, excellent. :-) | 20/04 15:50 |

dolio | It's okay to add 'a := Zero' to your constraint set. | 20/04 15:50 |

dolio | It's not okay to add 'f Zero := Zero'. | 20/04 15:50 |

quchen | Ah, now I understand the »only refine variables not expressions« statement. Good. | 20/04 15:51 |

glguy | when matching a == b, a can be a bit more than variables. You can have constructors in there with variables, though I'm not sure what the exact restriction is | 20/04 15:53 |

glguy | in the end you'll only be refining variables | 20/04 15:53 |

dolio | So if my skimming is correct, you 'with' on the expression because that replaces the expressions with a variable inside the with that you're then allowed to refine. | 20/04 15:53 |

dolio | That's what glguy was probably trying to explain. | 20/04 15:54 |

quchen | dolio: So you’re getting at that the refine-trick creates a variable that has the value of an expression, and the substitutes that variable with something else | 20/04 15:54 |

quchen | ..? | 20/04 15:54 |

quchen | Sent that too fast. Your last sentences seem to confirm this thought. | 20/04 15:55 |

dolio | If you do 'with f Zero ; ... | w = ?' then at ?, all occurrences of `f Zero` in types of things will have been replaced by `w`. | 20/04 15:55 |

quchen | Is parameter-vs-index of relevance here? I always wondered why | 20/04 15:56 |

quchen | data _≡_ {α} {A : Set α} (x : A) : A → Set α where | 20/04 15:56 |

quchen | and not e.g. | 20/04 15:57 |

quchen | data _≡_ {α} {A : Set α} : A -> A → Set α where | 20/04 15:57 |

quchen | or | 20/04 15:57 |

dolio | The former looks a little nicer. | 20/04 15:57 |

quchen | Does it? It looks much more heterogeneous to me. | 20/04 15:57 |

glguy | you only learn about your indices when pattern matching | 20/04 15:58 |

quchen | s/more/less/ | 20/04 15:58 |

quchen | glguy: Indices is left of the :, right? | 20/04 15:58 |

dolio | It lets you write `refl : x = x` instead of `refl x : x = x`. | 20/04 15:58 |

glguy | parameters first. then indicies | 20/04 15:58 |

dolio | Also if you tried `refl : {x : A} -> x = x`, I'm not sure if Agda would do as good a job figuring out the value of x so that you could just write `refl`. | 20/04 15:59 |

dolio | Maybe it would. | 20/04 15:59 |

quchen | So when matching against a (Vec A n), I only learn about the (n), not about the (A)? That makes sense. | 20/04 16:01 |

quchen | The (n) may vary among constructors, the (A) may not. | 20/04 16:01 |

dolio | quchen: This 'with' abstracting expressions into variables is doing the same job as the argument to P in substitution, by the way. | 20/04 16:01 |

quchen | substitution as in »subst : a = b -> P a -> P b«? | 20/04 16:02 |

dolio | Yeah. It might be clearer with a different type, though. | 20/04 16:03 |

dolio | Let me think. | 20/04 16:03 |

quchen | The »?« example you gave me earlier is probably fairly good. | 20/04 16:05 |

quchen | I still don’t get it, but it sounds like it’s the right direction. | 20/04 16:06 |

quchen | »with xxx does not merely create a synonym for xxx that we can match on« | 20/04 16:07 |

quchen | It creates more, namely some form of refinement rule | 20/04 16:07 |

dolio | It 'just' introduces variables for arbitrary expressions. | 20/04 16:10 |

quchen | Kind of like a dependent »let« | 20/04 16:11 |

dolio | And replaces those expressions with the variable in the context. | 20/04 16:11 |

dolio | Or, at least, in some of it. | 20/04 16:11 |

dolio | I think you can technically replace 'with' by creating a function with additional arguments. | 20/04 16:12 |

quchen | I think we’ve reduced not understanding »rewrite« to not understanding »with« :-D | 20/04 16:12 |

dolio | My memory is a bit hazy. Maybe rewrite is what does it in the entire context. | 20/04 16:12 |

quchen | when I do »with f Zero; … | w = ?«, then w’s type has to unify with »f Zero«s. For this to work, »f Zero« has to have a known type. Could that play a role? | 20/04 16:17 |

dolio | So, I think this is exactly how with works.... | 20/04 16:18 |

dolio | When you have `with A | B | C | ...` | 20/04 16:19 |

dolio | It is providing those expressions as the values of a telescope `w | x | y | ...` | 20/04 16:19 |

dolio | Where w has the type that A has. | 20/04 16:19 |

dolio | x has the type that B has, but with A replaced with w. | 20/04 16:20 |

dolio | y has the type that C has, but with A replaced with w and B replaced with x. | 20/04 16:20 |

dolio | And so on. | 20/04 16:20 |

quchen | The replacement of »A« with »w« is the crux though, since A can be an entire expression. So here we are replacing subexpressions again, no? | 20/04 16:22 |

quchen | dolio glguy anyway, thanks a lot for your help! I’ll have to go catch a bus, but I think I learned something here. | 20/04 16:28 |

quchen | Maybe I should find a paper about Agda’s typechecker and read through that. But maybe that’s too precise. Oh well, I’ll understand it soon I hope! :-) | 20/04 16:29 |

quchen | So thanks again, and see you around! | 20/04 16:29 |

dolio | quchen: Yes. | 20/04 16:29 |

dolio | quchen: Note that you can do this by making a function and calling it with A, B, C, ... as arguments. | 20/04 16:30 |

quchen | Hm, right. | 20/04 16:30 |

dolio | The function would be defined with w, x, y, ... as arguments. | 20/04 16:30 |

dolio | And also have all the arguments from the original function that it needs. | 20/04 16:30 |

dolio | So in that sense, with is just saving you from defining these auxiliary functions everywhere (and having to come up with names for them). | 20/04 16:31 |

quchen | That makes sense. | 20/04 16:33 |

quchen | I’m a bit biased from Haskell, where substitution of variables and unification is fairly easy. | 20/04 16:33 |

quchen | But dependent types make this a whole lot more complex (to me). | 20/04 16:33 |

quchen | Anyway, off to the bus! Bye :-) | 20/04 16:35 |

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