--- Day changed Thu Apr 13 2017 | ||

comietek | subttle: I don't know about fibres, but I did find myself needing the max element of a Fin | 13/04 07:27 |
---|---|---|

comietek | subttle: https://gist.github.com/mietek/bb5e152660c12abf1b59a69aab5d4f0f | 13/04 07:38 |

quchen | I’m getting a strange error when trying to declare {-# BUILTIN NATEQUALS _==_ #-}. I have (_≟_ : Decidable {A = ℕ} _≡_), so (x == y = ⌊ x ≟ y ⌋) ought to be a valid definition for equality of Nats, no? | 13/04 08:12 |

quchen | Yet Agda complains that »succ n != n of type ℕ when checking the pragma BUILTING NATEQUALS _==_« | 13/04 08:12 |

quchen | Another question: other than for scoping across all constructors, is there any reason to put parameters in data definitions on the left-hand side of the »:«? | 13/04 08:25 |

quchen | e.g. data Vector : (A : Set) -> Nat -> A -> Set where … | 13/04 08:26 |

quchen | … instead of data Vector (A : Set) : Nat -> Set where … | 13/04 08:26 |

gallais | quchen: if you put it on the right hand side, it's an index. You'll have to store it in the constructors and the type's level will be bumped by one because of that | 13/04 09:10 |

quchen | Level? | 13/04 09:10 |

quchen | You mean I’ll get a Set1 because of doing something like this? | 13/04 09:11 |

quchen | So my Vector : (A : Set) … will be a Set-1, not a Set? | 13/04 09:11 |

quchen | gallais: | 13/04 09:12 |

gallais | yes | 13/04 09:27 |

quchen | Hm. Then I guess I don’t understand levels anymore. | 13/04 09:30 |

quchen | So far, my mental model was »types that contain other types must be at higher levels than what they contain« | 13/04 09:30 |

quchen | But (Vector {l} (A : Set l) : Nat -> Set l where …) defines a vector that has the same level as its contents | 13/04 09:31 |

quchen | This is exactly what you mentioned, yes, but still it confuses me why this is different to putting the parameter on the RHS of the : | 13/04 09:32 |

comietek | quchen: e.g. https://ziman.functor.sk/oldblog/index.html%3Fp=443.html | 13/04 10:25 |

comietek | http://stackoverflow.com/questions/24600256/difference-between-type-parameters-and-indices | 13/04 10:26 |

comietek | https://www.quora.com/What-is-different-between-a-parameter-and-an-index-to-a-type | 13/04 10:26 |

comietek | http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Data | 13/04 10:26 |

quchen | Okay okay :-) | 13/04 10:33 |

quchen | Thanks! | 13/04 10:33 |

quchen | I’ve read some of them, but it didn’t click yet. | 13/04 10:33 |

quchen | Reading it again might help maybe. | 13/04 10:33 |

quchen | Gut feeling improved, but not crystal clear. So far, so good. :-) | 13/04 10:42 |

quchen | Up next: »rewrite«. I know what it desugars to, which brings me to that I don’t understand unification very well either. | 13/04 10:42 |

quchen | It’s easy to imagine that using x ≡ y allows me to replace all x with y. | 13/04 10:43 |

quchen | But Agda is much more powerful: it also works for whole expressions, like succ x = succ (succ y). | 13/04 10:43 |

quchen | When I rewrite using that, it feels like I’m instructing Agda to find all subexpressions containing succ x and performing the substitution on them. | 13/04 10:44 |

quchen | In other words, I feel like rewrite magically finds all places where one could apply the rewrite. | 13/04 10:44 |

quchen | FWIW, the desugaring I know is from http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.PatternMatching | 13/04 10:47 |

quchen | f ps rewrite eqn = rhs | 13/04 10:47 |

quchen | >>>>> | 13/04 10:47 |

quchen | f ps with a | eqn | 13/04 10:47 |

quchen | … | ._ | refl = rhs | 13/04 10:47 |

quchen | What’s the match on »a« for if all we do is ignore it? Assert that it’s matchable? | 13/04 10:48 |

--- Log closed Thu Apr 13 16:06:15 2017 | ||

--- Log opened Thu Apr 13 16:08:26 2017 | ||

-!- Irssi: #agda: Total of 139 nicks [0 ops, 0 halfops, 0 voices, 139 normal] | 13/04 16:08 | |

-!- Irssi: Join to #agda was synced in 161 secs | 13/04 16:11 | |

subttle | comietek: thank you! | 13/04 16:40 |

subttle | comietek: I have class now but I will take a look tonight | 13/04 20:57 |

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