--- Day changed Thu Apr 20 2017
glguyquchen: Did you ever figure out why the rewrite syntax matches on both the lhs and the equality?20/04 15:38
quchenglguy: Unfortunately not.20/04 15:38
quchenThe question was »how does rewrite work«, right?20/04 15:38
glguyYes. When you put the lhs in a with Agda replaces occurences of that expression in the current context and matches that against whatever you match20/04 15:39
quchenrewrite (eq : a = b)    ->   replace all »a« with »b« in the body, even when »a« is a tree20/04 15:39
quchentree as in not-just-a-simple-atom20/04 15:39
glguy*especially* when it's a "tree"20/04 15:40
glguyThat's when it matters20/04 15:40
glguyBecause you don't want it to be one20/04 15:40
glguyso that when you match on the refl that you can replace a variable representing the lhs with a . pattern20/04 15:40
quchen <quchen>   f ps rewrite eqn = rhs20/04 15:40
quchen <quchen> >>>>>20/04 15:40
quchen <quchen>   f ps with a | eqn20/04 15:40
quchen <quchen>   … | ._ | refl = rhs20/04 15:40
glguyquchen: to see what it's doing, take some code that uses a rewrite and instead of " … | ._ | refl = rhs"20/04 15:41
glguyLook at " … | lhs | eq = ?"20/04 15:41
quchenOkay, canonical example: commutativity of addition, succ n + m = succ (n + m)20/04 15:42
glguyYou'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
glguyhas now*20/04 15:42
glguyhas now been* even20/04 15:42
quchenHah, better: associativity.20/04 15:43
quchenassoc-+ (succ x) y z rewrite assoc-+-rewrite x y z = refl20/04 15:43
quchenassoc-+ (succ x) y z rewrite assoc-+ x y z = refl20/04 15:43
quchenThat one.20/04 15:43
glguynext matching on eq with the constructor 'refl' requires us to be able to replace the lhs pattern with the forced value coming from the refl20/04 15:43
glguyso we use a dot pattern to indicate that that pattern's value is forced by matching on something else20/04 15:43
quchenSo ._ and .refl are identical here?20/04 15:44
glguyNo, the ._ isn't .refl20/04 15:44
quchenAh right, it’s the LHS20/04 15:44
quchenOf the equality20/04 15:44
glguyyes20/04 15:44
quchenAnd since it has to unify with refl’s LHS that makes it inferrable20/04 15:44
glguySo it's a two step process of abstracting the lhs out of the context and then forcing that to have some value20/04 15:45
quchenSo we can put the dot there20/04 15:45
quchenWhat if we leave the dot away?20/04 15:45
glguyYeah, not only can we, I think we must use a dot20/04 15:45
quchenWhat links the _ with the refl?20/04 15:45
glguyrefl's type links it20/04 15:45
glguyYou can't pattern match on refl unless it's possible to replace the a in (a === b) in the context20/04 15:46
quchenPattern matching on refl still confuses me a bit (so does path induction in HoTT, the two problems are likely related).20/04 15:47
quchenFor me, (refl : a = b) tells the typechecker to add the substitution (a -> b).20/04 15:47
quchenIs that even right?20/04 15:47
dolioWhat are a and b?20/04 15:48
quchenSome values ..?20/04 15:48
dolioWell then no.20/04 15:48
quchenLet me socratize you back and ask: what are a and b? :-)20/04 15:48
dolioMatching 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
quchenWhat Hindley-Milner often calls »substitution«?20/04 15:50
dolioIt is like adding your substitutions.20/04 15:50
quchenAh, okay. Common ground, excellent. :-)20/04 15:50
dolioIt's okay to add 'a := Zero' to your constraint set.20/04 15:50
dolioIt's not okay to add 'f Zero := Zero'.20/04 15:50
quchenAh, now I understand the »only refine variables not expressions« statement. Good.20/04 15:51
glguywhen 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 is20/04 15:53
glguyin the end you'll only be refining variables20/04 15:53
dolioSo 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
dolioThat's what glguy was probably trying to explain.20/04 15:54
quchendolio: 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 else20/04 15:54
quchen..?20/04 15:54
quchenSent that too fast. Your last sentences seem to confirm this thought.20/04 15:55
dolioIf 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
quchenIs parameter-vs-index of relevance here? I always wondered why20/04 15:56
quchendata _≡_ {α} {A : Set α} (x : A) : A → Set α where20/04 15:56
quchenand not e.g.20/04 15:57
quchendata _≡_ {α} {A : Set α} : A -> A → Set α where20/04 15:57
quchenor20/04 15:57
dolioThe former looks a little nicer.20/04 15:57
quchenDoes it? It looks much more heterogeneous to me.20/04 15:57
glguyyou only learn about your indices when pattern matching20/04 15:58
quchens/more/less/20/04 15:58
quchenglguy: Indices is left of the :, right?20/04 15:58
dolioIt lets you write `refl : x = x` instead of `refl x : x = x`.20/04 15:58
glguyparameters first. then indicies20/04 15:58
dolioAlso 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
dolioMaybe it would.20/04 15:59
quchenSo when matching against a (Vec A n), I only learn about the (n), not about the (A)? That makes sense.20/04 16:01
quchenThe (n) may vary among constructors, the (A) may not.20/04 16:01
dolioquchen: 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
quchensubstitution as in »subst : a = b -> P a -> P b«?20/04 16:02
dolioYeah. It might be clearer with a different type, though.20/04 16:03
dolioLet me think.20/04 16:03
quchenThe »?« example you gave me earlier is probably fairly good.20/04 16:05
quchenI 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
quchenIt creates more, namely some form of refinement rule20/04 16:07
dolioIt 'just' introduces variables for arbitrary expressions.20/04 16:10
quchenKind of like a dependent »let«20/04 16:11
dolioAnd replaces those expressions with the variable in the context.20/04 16:11
dolioOr, at least, in some of it.20/04 16:11
dolioI think you can technically replace 'with' by creating a function with additional arguments.20/04 16:12
quchenI think we’ve reduced not understanding »rewrite« to not understanding »with« :-D20/04 16:12
dolioMy memory is a bit hazy. Maybe rewrite is what does it in the entire context.20/04 16:12
quchenwhen 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
dolioSo, I think this is exactly how with works....20/04 16:18
dolioWhen you have `with A | B | C | ...`20/04 16:19
dolioIt is providing those expressions as the values of a telescope `w | x | y | ...`20/04 16:19
dolioWhere w has the type that A has.20/04 16:19
doliox has the type that B has, but with A replaced with w.20/04 16:20
dolioy has the type that C has, but with A replaced with w and B replaced with x.20/04 16:20
dolioAnd so on.20/04 16:20
quchenThe 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
quchendolio 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
quchenMaybe 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
quchenSo thanks again, and see you around!20/04 16:29
dolioquchen: Yes.20/04 16:29
dolioquchen: Note that you can do this by making a function and calling it with A, B, C, ... as arguments.20/04 16:30
quchenHm, right.20/04 16:30
dolioThe function would be defined with w, x, y, ... as arguments.20/04 16:30
dolioAnd also have all the arguments from the original function that it needs.20/04 16:30
dolioSo 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
quchenThat makes sense.20/04 16:33
quchenI’m a bit biased from Haskell, where substitution of variables and unification is fairly easy.20/04 16:33
quchenBut dependent types make this a whole lot more complex (to me).20/04 16:33
quchenAnyway, off to the bus! Bye :-)20/04 16:35

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