--- Day changed Thu Mar 30 2017 | ||

quchen | I’m trying to define a type for sorted vectors, but I’m having trouble defining the recursive step. | 30/03 09:22 |
---|---|---|

quchen | http://lpaste.net/354093 | 30/03 09:22 |

quchen | Line 7 is the problem, I need to recursively talk about that the rest of the list is sorted, but I also need its first element. | 30/03 09:22 |

quchen | (… if present, to make things worse.) | 30/03 09:23 |

{AS} | quchen: use an implicit variable | 30/03 09:43 |

{AS} | change ∀ x₁ x₂ to ∀ x₁ x₂ {xs} | 30/03 09:43 |

quchen | forall x1 x2 {xs} -> x1 <= x2 -> Sorted xs -> Sorted (x1 :: x2 :: xs)? | 30/03 09:45 |

{AS} | Yeah | 30/03 09:45 |

quchen | But then I don’t get the recursive step that guarantees that (x2 :: xs) is also sorted | 30/03 09:45 |

{AS} | quchen: so change it to forall x1 x2 {xs} -> x1 <= x2 -> Sorted (x2 :: xs) -> Sorted (x1 :: x2 :: xs) | 30/03 09:46 |

quchen | Ah, that looks promising. | 30/03 09:46 |

canndrew | mietek: at least 5 minutes, nah i don't use instance arguments (and wasn't aware of their existance) | 30/03 16:34 |

canndrew | {AS}: yes, a whole bunch of mutual definitions that refer to each in their types and can't be split into seperate files | 30/03 16:34 |

sleffy | Is there a nice lemma in the stdlib which relates `lookup` and `map`? I'm looking for something which gives `lookup i (map f xs) = f (lookup i xs)` | 30/03 16:46 |

sleffy | For `Vec`s. | 30/03 16:46 |

mudri | I've been wondering today why stdlib has a two-phase IsStructure-Structure convention, rather than a three-phase IsStructure-StructureOn-Structure convention, as exemplified by ↓↓↓. | 30/03 17:24 |

lpaste_ | mudri pasted “ModuleExperiments.agda” at http://lpaste.net/354104 | 30/03 17:25 |

mudri | I thought of it recently as a nicer way to deal with semirings which are also partial orders. | 30/03 17:26 |

{AS} | canndrew: so you might be hitting an actual limitation | 30/03 17:35 |

{AS} | Theoretically type checking Agda is exponential in time | 30/03 17:36 |

{AS} | If there is a lot of type-level computation, it might take a while | 30/03 17:36 |

rntz^2 | merely exponential? | 30/03 17:38 |

rntz^2 | that seems wrong. can't agda compute the ackermann function? | 30/03 17:38 |

{AS} | rntz^2: that is exponential | 30/03 17:43 |

{AS} | rntz^2: https://en.m.wikipedia.org/wiki/EXPSPACE | 30/03 17:47 |

{AS} | Sorry that was Exponential space | 30/03 17:49 |

rntz^2 | ah, yeah | 30/03 17:50 |

canndrew | {AS}: damn, any tips for speeding it up (other than what's on the wiki)? | 30/03 17:57 |

rntz^2 | hm, apparently deciding regular expression equivalence is EXPSPACE-complete | 30/03 17:58 |

rntz^2 | I wonder whether anybody's implemented it in agda | 30/03 17:58 |

{AS} | rntz^2: you might be right, but as far as I understand everything is exponential, just with more and more exponents :) | 30/03 18:01 |

{AS} | I am probably wrong | 30/03 18:02 |

{AS} | canndrew: do you have an example of your code | 30/03 18:03 |

{AS} | Or what it does? | 30/03 18:03 |

canndrew | {AS}: sure: https://github.com/canndrew/malk-agda/blob/master/Core.agda | 30/03 18:11 |

canndrew | implementation of type theory in type theory | 30/03 18:11 |

canndrew | or at least an attempt at one | 30/03 18:11 |

{AS} | canndrew: that definitely looks like something that will take a long time to type check :) | 30/03 18:36 |

{AS} | For more complex theories I would probably make things as simply typed as possible and then show required properties externally | 30/03 18:37 |

{AS} | Instead of baking everything in the types | 30/03 18:37 |

canndrew | naaaah, I want a type of well-typed terms. what good is type theory if it can't implement type theory? :) | 30/03 18:47 |

comietek | canndrew_: its Conor, not Connor | 30/03 19:14 |

canndrew_ | comietek: thanks! | 30/03 19:19 |

canndrew_ | and sorry for that code, the naming and organisation leave a lot to be desired. | 30/03 19:19 |

comietek | No worries | 30/03 19:19 |

comietek | Can't read now on phone | 30/03 19:19 |

comietek | But this is interesting stuff | 30/03 19:20 |

comietek | Why do you think you can do TT in TT? | 30/03 19:20 |

comietek | canndrew_: ^^ | 30/03 19:23 |

canndrew_ | comietek: it's more that I hope I can do it rather than think I can | 30/03 19:56 |

canndrew_ | but I don't see why it shouldn't be possible | 30/03 19:56 |

comietek | canndrew_: I'm going to do the thing that I hate when people do | 30/03 20:01 |

comietek | Gödel? | 30/03 20:01 |

canndrew_ | I don't understand Gödel well enough to understand how or if it applies here. If I run into a brick wall while trying to implement this then maybe that'll teach me. | 30/03 20:13 |

mietek | very good | 30/03 20:22 |

mietek | canndrew_: you may be interested in joining ##dependent | 30/03 20:22 |

rntz^2 | hm. you shouldn't be able to show the consistency of TT in TT, but that doesn't mean you can't do *some* stuff with it | 30/03 20:31 |

rntz^2 | the standard way to show consistency would be by normalization and then showing there's no normal-form proof of bottom, for example | 30/03 20:31 |

rntz^2 | so you run up against the "can't write a total interpreter for a total language in itself" | 30/03 20:32 |

rntz^2 | but you can still write an interpreter that's in a nontermination monad | 30/03 20:32 |

mietek | thanks, rntz^2, for doing the thing I hate the most | 30/03 20:32 |

mietek | "can't write a total interpreter for a total language in itself" | 30/03 20:32 |

mietek | show me the money | 30/03 20:33 |

mietek | have you proven that? | 30/03 20:33 |

rntz^2 | ok, look, do you believe that TT can't show TT consistent? | 30/03 20:33 |

mietek | it’s irrelevant what I believe | 30/03 20:33 |

mietek | are you backing out now? | 30/03 20:33 |

rntz^2 | if you won't believe it until it's proven, I'll do it if you pay me :P | 30/03 20:33 |

rntz^2 | if you just want me to explain why I think it's impossible, and it's not a very long argument, I'll do it for free | 30/03 20:34 |

rntz^2 | so, do you accept that TT can't show TT consistent (by some analogue of godel's second incompleteness theorem) | 30/03 20:34 |

mietek | I don’t think you can show that | 30/03 20:34 |

rntz^2 | sorry, don't think that TT can show TT consistent, or don't think that you can show that "TT can't show TT consistent"? | 30/03 20:35 |

mietek | primarily, because in order to show that, you would need to formalise TT in TT | 30/03 20:35 |

rntz^2 | in order to show *what* | 30/03 20:35 |

mietek | the proposition you are asking me to accept | 30/03 20:36 |

mietek | I don’t think you can write it down | 30/03 20:36 |

rntz^2 | ... could you just say for me what it is you don't think can be shown instead of referring to what I'm saying because your pronouns have several different possible referents and I don't know which one it is you're referring to | 30/03 20:37 |

mietek | <rntz^2> so, do you accept that TT can't show TT consistent (by some analogue of godel's second incompleteness theorem) | 30/03 20:37 |

mietek | you are asking me if I accept some vaguely-stated proposition | 30/03 20:38 |

mietek | I don’t think you can state it formally | 30/03 20:38 |

rntz^2 | ... do you think godel stated godel's second incompleteness theorem formally? | 30/03 20:38 |

rntz^2 | or are you saying there's something special about TT that isn't special about PA? | 30/03 20:38 |

mietek | I’m not disputing Gödel; I have an issue with people who invoke Gödel’s name without actually doing the proofs | 30/03 20:39 |

rntz^2 | ok, fine. pay me a salary of $1000/month and I'll try to do a formal proof that agda can't write a total interpreter for agda (or some other system, if you prefer). but I'm not doing unpaid labor for you :P | 30/03 20:40 |

* mietek shrugs | 30/03 20:40 | |

mietek | so, you can’t | 30/03 20:40 |

mietek | and yet, you repeat it, as if you could | 30/03 20:41 |

mietek | I wouldn’t do that | 30/03 20:41 |

rntz^2 | well, I ain't you. | 30/03 20:42 |

{AS} | mietek: didn't someone refer you to a proof of Gödels second some time ago? | 30/03 21:43 |

mietek | {AS}: please read again | 30/03 21:44 |

{AS} | mietek: I did read, I am just confused where you disagreed | 30/03 21:45 |

{AS} | Oh, this is #agda | 30/03 21:45 |

mietek | yeah, wrong channel, but just for completeness’ sake (ha!) | 30/03 21:45 |

mietek | I have a problem with making any statement about TT within TT | 30/03 21:46 |

mietek | this has nothing to do with Gödel | 30/03 21:46 |

mietek | if you want to make a statement about TT within TT, you have first to formalise TT in TT | 30/03 21:46 |

mietek | now, the interesting thing we found last time this came up was http://www.von-eitzen.de/math/tntrep.xml | 30/03 21:47 |

mietek | apparently this is a formalisation of TNT in TNT | 30/03 21:47 |

mietek | I haven’t had the time to look at it yet | 30/03 21:47 |

{AS} | I see :) | 30/03 21:48 |

dolio | If you can't represent a type theory within itself, you have already failed the first step of writing an interpreter. | 30/03 21:52 |

mietek | dolio: we don’t know if we can or can’t represent TT in TT | 30/03 22:00 |

mietek | I have been over this so many times I just can’t do it again, not today | 30/03 22:02 |

mietek | Brown-Palsberg 2016, part 1 | 30/03 22:02 |

mietek | also, ##dependent is a better place for arguing about this than #agda | 30/03 22:03 |

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