--- Day changed Thu Mar 30 2017
quchenI’m trying to define a type for sorted vectors, but I’m having trouble defining the recursive step.30/03 09:22
quchenhttp://lpaste.net/35409330/03 09:22
quchenLine 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 variable30/03 09:43
{AS}change  ∀ x₁ x₂ to  ∀ x₁ x₂ {xs}30/03 09:43
quchenforall x1 x2 {xs} -> x1 <= x2 -> Sorted xs -> Sorted (x1 :: x2 :: xs)?30/03 09:45
{AS}Yeah30/03 09:45
quchenBut then I don’t get the recursive step that guarantees that (x2 :: xs) is also sorted30/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
quchenAh, that looks promising.30/03 09:46
canndrewmietek: 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 files30/03 16:34
sleffyIs 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
sleffyFor `Vec`s.30/03 16:46
mudriI'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/35410430/03 17:25
mudriI 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 limitation30/03 17:35
{AS}Theoretically type checking Agda is exponential in time30/03 17:36
{AS}If there is a lot of type-level computation, it might take a while30/03 17:36
rntz^2merely exponential?30/03 17:38
rntz^2that seems wrong. can't agda compute the ackermann function?30/03 17:38
{AS}rntz^2: that is exponential30/03 17:43
{AS}rntz^2: https://en.m.wikipedia.org/wiki/EXPSPACE30/03 17:47
{AS}Sorry that was Exponential space30/03 17:49
rntz^2ah, yeah30/03 17:50
canndrew{AS}: damn, any tips for speeding it up (other than what's on the wiki)?30/03 17:57
rntz^2hm, apparently deciding regular expression equivalence is EXPSPACE-complete30/03 17:58
rntz^2I wonder whether anybody's implemented it in agda30/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 wrong30/03 18:02
{AS}canndrew: do you have an example of your code30/03 18:03
{AS}Or what it does?30/03 18:03
canndrew{AS}: sure: https://github.com/canndrew/malk-agda/blob/master/Core.agda30/03 18:11
canndrewimplementation of type theory in type theory30/03 18:11
canndrewor at least an attempt at one30/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 externally30/03 18:37
{AS}Instead of baking everything in the types30/03 18:37
canndrewnaaaah, I want a type of well-typed terms. what good is type theory if it can't implement type theory? :)30/03 18:47
comietekcanndrew_: its Conor, not Connor30/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
comietekNo worries30/03 19:19
comietekCan't read now on phone30/03 19:19
comietekBut this is interesting stuff30/03 19:20
comietekWhy do you think you can do TT in TT?30/03 19:20
comietekcanndrew_: ^^30/03 19:23
canndrew_comietek: it's more that I hope I can do it rather than think I can30/03 19:56
canndrew_but I don't see why it shouldn't be possible30/03 19:56
comietekcanndrew_: I'm going to do the thing that I hate when people do30/03 20:01
comietekGö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
mietekvery good30/03 20:22
mietekcanndrew_: you may be interested in joining ##dependent30/03 20:22
rntz^2hm. 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 it30/03 20:31
rntz^2the standard way to show consistency would be by normalization and then showing there's no normal-form proof of bottom, for example30/03 20:31
rntz^2so you run up against the "can't write a total interpreter for a total language in itself"30/03 20:32
rntz^2but you can still write an interpreter that's in a nontermination monad30/03 20:32
mietekthanks, rntz^2, for doing the thing I hate the most30/03 20:32
mietek"can't write a total interpreter for a total language in itself"30/03 20:32
mietekshow me the money30/03 20:33
mietekhave you proven that?30/03 20:33
rntz^2ok, look, do you believe that TT can't show TT consistent?30/03 20:33
mietekit’s irrelevant what I believe30/03 20:33
mietekare you backing out now?30/03 20:33
rntz^2if you won't believe it until it's proven, I'll do it if you pay me :P30/03 20:33
rntz^2if 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 free30/03 20:34
rntz^2so, do you accept that TT can't show TT consistent (by some analogue of godel's second incompleteness theorem)30/03 20:34
mietekI don’t think you can show that30/03 20:34
rntz^2sorry, 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
mietekprimarily, because in order to show that, you would need to formalise TT in TT30/03 20:35
rntz^2in order to show *what*30/03 20:35
mietekthe proposition you are asking me to accept30/03 20:36
mietekI don’t think you can write it down30/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 to30/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
mietekyou are asking me if I accept some vaguely-stated proposition30/03 20:38
mietekI don’t think you can state it formally30/03 20:38
rntz^2... do you think godel stated godel's second incompleteness theorem formally?30/03 20:38
rntz^2or are you saying there's something special about TT that isn't special about PA?30/03 20:38
mietekI’m not disputing Gödel; I have an issue with people who invoke Gödel’s name without actually doing the proofs30/03 20:39
rntz^2ok, 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 :P30/03 20:40
* mietek shrugs30/03 20:40
mietekso, you can’t30/03 20:40
mietekand yet, you repeat it, as if you could30/03 20:41
mietekI wouldn’t do that30/03 20:41
rntz^2well, 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 again30/03 21:44
{AS}mietek: I did read, I am just confused where you disagreed30/03 21:45
{AS}Oh, this is #agda30/03 21:45
mietekyeah, wrong channel, but just for completeness’ sake (ha!)30/03 21:45
mietekI have a problem with making any statement about TT within TT30/03 21:46
mietekthis has nothing to do with Gödel30/03 21:46
mietekif you want to make a statement about TT within TT, you have first to formalise TT in TT30/03 21:46
mieteknow, the interesting thing we found last time this came up was http://www.von-eitzen.de/math/tntrep.xml30/03 21:47
mietekapparently this is a formalisation of TNT in TNT30/03 21:47
mietekI haven’t had the time to look at it yet30/03 21:47
{AS}I see :)30/03 21:48
dolioIf you can't represent a type theory within itself, you have already failed the first step of writing an interpreter.30/03 21:52
mietekdolio: we don’t know if we can or can’t represent TT in TT30/03 22:00
mietekI have been over this so many times I just can’t do it again, not today30/03 22:02
mietekBrown-Palsberg 2016, part 130/03 22:02
mietekalso, ##dependent is a better place for arguing about this than #agda30/03 22:03

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