--- Day changed Fri Dec 15 2017
srpxhttps://www.reddit.com/r/haskell/comments/7jxfr3/what_is_the_easiest_way_to_extend_morte_to_enable/15/12 04:39
lengmenHey I'm interested in Agda coding style guides. Any suggestions? Google search didn't lead me anywhere. If not, is there a good Haskell style guide that has transferable tips?15/12 08:48
lengmenLike for example is it a good idea to always do universe polymorphism. Or should I leave it to when I need it?15/12 08:52
mietekgood IRC style is hanging around in the channel for an answer :)15/12 11:43
srpxIs it possible to extract the second element of Sigma on CoC with Type:Type?15/12 18:19
pgiarrussosrpx: IIRC the only problem is that it might be inconsistent, but Type:Type is inconsistent anyway15/12 18:23
pgiarrussomore precisely, I read impredicativity (as in System F/CiC, not just Type:Type) combined with strong sums can already create paradoxes15/12 18:24
pgiarrussoI’m referring to footnote 1 of http://www.staff.city.ac.uk/~ross/papers/pts.pdf15/12 18:25
pgiarrusso(though I might misunderstand it)15/12 18:26
srpxI'm ok with paradoxes now because there seems to be no simple language that isn't paradoxal.15/12 18:26
pgiarrussosrpx: but your question is confusing — I took a wild guess at what you’re asking, but why/how are you combining CoC + Type:Type? And asking about CoC in the #agda channel?15/12 18:26
srpxIs that not a good place to ask about CoC? Where else, then?15/12 18:27
pgiarrussoIf you use CoC for the Calculus of Constructions, that’s the foundation of Coq, not Agda; but I’ve never seen Type:Type in Coq15/12 18:27
pgiarrussoor, well, in Coq you have Type i : Type (i + 1) and the indexes are hidden15/12 18:27
srpxOh, you're right, perhaps #coq would be a better place.15/12 18:27
pgiarrussobut Type: Type is not that15/12 18:28
srpxAnyway, the reason for my question is, I need a language that 1. is simple enough for me to implement, 2. can prove useful things (like extracting the second element of sigma, induction, etc.)15/12 18:28
srpxThere seems to be both languages simple enough for me to implement (CoC) but that can't prove useful things, and languages too complex for me to implement (CoIC, Idris, etc.) that can prove useful things. No middle ground ):15/12 18:29
pgiarrussojust to finish: I do understand you can’t add “strong sums” (Sigma where you can extract second argument) to System F, because of paradoxes (Is it Girard’s paradox? I know that was discovered in System U first)15/12 18:29
pgiarrussoif you ask about induction, maybe Aaron Stump’s work is relevant?15/12 18:29
srpxAh, and since there's no expressive language simple enough for me to implement, I thought: perhaps if I use CoC, except with Type:Type, that'll be simple enough for me to implement, while also having all those interesting terms. Of course, that'd be inconsistent, but I could use it to write code now, and port it to a consistent core later (shouldn't be too different, I guess).15/12 18:30
pgiarrussobut IIUC CoC still cannot do induction conveniently/at all?15/12 18:31
pgiarrussoso http://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta-tlca-14.pdf is relevant15/12 18:31
srpxYep, it is extremely relevant! There is also this recent paper from 2017: http://homepage.cs.uiowa.edu/~astump/papers/cedille-draft.pdf which cites the one about self types15/12 18:32
pgiarrussoyep15/12 18:33
srpxpgiarrusso: problem is, CoC is extremely simple (really, it is just lambdas and forall). I can implement it. Those papers introduce *a lot* of new constructs that I don't understand very well. The language goes from 2 binders to 6 or 7, I guess? So that's a huge jump in complexity. I'm not sure I could implement it. Perhaps?15/12 18:33
pgiarrussothat calculus adds *one* binder, iota; the rest is presentation15/12 18:34
pgiarrussoalso, well, I’d say that CoC + Type:Type is Agda + Type:Type15/12 18:35
pgiarrussoor, well, it’s lambda-*15/12 18:35
srpxpgiarrusso: iota = self types? It also needs positive recursion, and I have no idea how to implement that properly...15/12 18:35
pgiarrussoiota is self-types, yes — iota is the greek letter used to write them in the 2014 paper15/12 18:35
srpxoh, ok15/12 18:35
pgiarrussoon the 6-7 binders:15/12 18:36
srpxbut then, it still requires self types, and there are other constructors here, no? There is that implicit forall thing, and... well, see: https://i.imgur.com/5YxVKlv.png I count 8 different binders, no? Kinda scary15/12 18:37
pgiarrussothat paper has, essentially, just self types, Pi-types and lambda abstractions. They are just copied at multiple levels15/12 18:37
srpxhmmm15/12 18:37
pgiarrussoif you do that in CoC, you also get more than 2 binders15/12 18:37
srpxI see, interesting. Hm...15/12 18:37
pgiarrussoyou can see this by looking at pure type systems or the lambda cube15/12 18:38
pgiarrussoso, I’m afraid to link at nlab, but https://ncatlab.org/nlab/show/pure+type+system seems actually helpful15/12 18:40
pgiarrussothe basic idea is that you just have lambda types and pi-types, like in Agda15/12 18:40
pgiarrussoand then you decide which sort can depend on which sort15/12 18:40
pgiarrussosorry, I didn’t explain what is a “sort”, but maybe you have seen the definition in CoC?15/12 18:41
pgiarrussowith Type : Type, Type is the only sort15/12 18:42
pgiarrussosorry, my improvised explanation of PTS is bad15/12 18:44
srpxpgiarrusso: yep but even the top of the lambda cube (with all possible dependencies, which becomes exactly CoC, no?) you still can't do something as simple as Sigma.snd15/12 18:45
pgiarrussohm15/12 18:45
srpxah, sorry for not understanding, actually15/12 18:45
srpxlet me finish reading the ncatlab article15/12 18:46
pgiarrussoso, top of lambda cube is CoC indeed15/12 18:46
pgiarrussobut... I’m wondering why you can’t do Sigma.snd in CoC. Maybe you mean that if you try to Church-encode Sigma you can’t write snd? That’s true, but it’s not obvious Type:Type would help?15/12 18:47
srpxbtw the Type:Type thing was just "ok, if we introduce *this* fallacy to coc, would we be able to prove Sigma.snd"? I'm aware that you can have two sorts, and then PTS can be instantiated in either STLC (enabling only value->value) functions, or system-f (enabling polimorphism), or coc (enabling types to depend on values), or other combinations15/12 18:48
srpxpgiarrusso: ah I have no reason to think it would help, it was just a "ok, we don't have a CONSISTENT core that can prove Sigma.snd"... but do we have an INCONSISTENT one which does? Type:Type is the inconsistent core that is closest to CoC, so I just wondered if that somehow gave it the extra power it needed for Sigma.snd15/12 18:49
ezyangDefinitionally, you can prove Sigma.snd with any inconsistent core 15/12 18:50
srpxBecause you can prove everything, right? That's what I hear. But I'm not sure how that would work in practice.15/12 18:51
pgiarrussoyou can prove everything, but it’s hard15/12 18:52
srpxAh, I see. 15/12 18:52
pgiarrussoHere’s one version of Girard’s paradox in System U-, defined in Coq: https://coq.inria.fr/library/Coq.Logic.Hurkens.html15/12 18:53
srpxOk, I think the most promising part of this conversation is: if I just take my implementation of CoC and add self types (I can do that, they just allow a type to refer to its own value, right?) then I'll be able to have O(1) pattern-matching and induction? What about the implicit forall thing, and the positive recursion? No idea how I implement that on CoC (without breaking everything).15/12 18:54
pgiarrussoI don’t get Girard’s paradox, but all the papers describing it are not trivial15/12 18:54
srpxWell, that's a lot of code.15/12 18:55
pgiarrussoYep, which is why I’ve never really *tried* to get it, and never gotten a loop when programming in lambda-*15/12 18:55
pgiarrussoStill: CoC is just MLTT with some special hierarchy of universes; type: type is a much simpler hierarchy15/12 18:56
pgiarrussoso you can play with it in Agda15/12 18:56
pgiarrussowith `agda —type-in-type`15/12 18:56
pgiarrusso(that’s a double hyphen, `--type-in-type`)15/12 18:56
pgiarrussoso, you could try what programs you can write in Agda like that before implementing such a system15/12 18:57
pgiarrussoback to Stump’s work15/12 18:57
pgiarrussoI had forgot about the implicit forall, I don’t know why it’s there and if that’s essential to its expressivity, but I’d expect not?15/12 18:58
pgiarrussofor positive recursion... I’m not an expert, and if you’re inconsistent anyway you can skip the check and just allow recursion?15/12 18:59
pgiarrussoor, well, ask somebody else how to do it or how hard it is, I’ve never done it15/12 19:00
pgiarrussothough checking positivity does not *seem* hard: you just traverse a type looking for recursive occurrences and keeping a flag that tells you if a position is positive or negative15/12 19:01
srpxCoC is just MLTT with Type(N) : Type(N+1)?15/12 19:02
srpxSo how is MLTT like? Type(0) : Type(1) : end?15/12 19:02
pgiarrussono, that’s MLTT, CoC adds impredicative Prop15/12 19:03
pgiarrussofor both theories you can have many universes or not15/12 19:03
srpxnot sure what an impredicative prop is, but not reelvant for now I guess15/12 19:03
pgiarrussoI mean, the CoC in the lambda cube does not have a infinite hierarchy of universes, but it’s OK to add them15/12 19:03
srpx@pgiarrusso but if I'm inconsistent anyway then why would I bother with self types, as I'm already to prove everything with Type:Type anyway?15/12 19:04
lambdabotUnknown command, try @list15/12 19:04
srpxwoops, without the @15/12 19:04
pgiarrussowell, impredicative Prop means that forall A: Prop, T lives again in the same Prop; if you don’t do that you’re doing MLTT15/12 19:04
srpxpgiarrusso: but okay, sorry for so many questions!15/12 19:05
pgiarrussopositivity checking looks a bit like writing:15/12 19:05
pgiarrusso occurs_negative x sign (s -> t) = occurs_negative x (-1 * sign) s || occurs_negative x sign t15/12 19:05
pgiarrusso(I think)15/12 19:05
pgiarrussoon your Q:15/12 19:05
pgiarrussoI agree you can code up Girard’s paradox (even though it’s lots of code) and do everything with it I guess15/12 19:06
pgiarrussoI guess you can’t port that to better systems later15/12 19:06
pgiarrussoalso, I’m not sure inconsistent means you can write all programs you want to write; you can just inhabit their types15/12 19:07
pgiarrussobut “I can write a function Nat -> Nat” doesn’t mean “I can write the function Nat -> Nat that I want”15/12 19:08
pgiarrussoamong other things, I think still nobody knows if you can write a fixpoint operator in such systems (a fellow PhD student wondered for a while for his PhD thesis)15/12 19:08
pgiarrussobut maybe I miss something?15/12 19:08
srpxpgiarrusso: ah, makes sense15/12 19:09
srpxeverything is terrible :(15/12 19:09
pgiarrussoalso maybe useful, a relatively mature PTS implementation: https://github.com/Toxaris/pts15/12 19:10
srpxI guess I'll just base this dapp browser on the untyped lambda calculus and forget about proofs for now15/12 19:10
pgiarrussodon’t know your goals but that’s surely simple15/12 19:10
pgiarrussoI mean, Stump’s research *claims* to be about exactly the problems you describe, I just can’t say if it helps you15/12 19:11
srpxpgiarrusso: I'd just like to have a browser for ethereum dapps with a backend pane where you can see what theorems have been proven about that dapp / contract (like: "this dapp has proven to be zero-sum!")15/12 19:11
srpxof course, for that I need to integrate a proof language with the browser, and I'm just a single person, can't write a whole implementation of Idris myself, for example... thus the need for simpler cores15/12 19:12
srpxhttps://gist.github.com/MaiaVictor/4d53e60bad6cb2c9c52a0d01d89c094d -- pgiarrusso this is an implementation of CoC, so this is also almost a valid implementation of PTS, right? If I get it, from CoC to PTS it requires to change a few lines of code15/12 19:13
srpxpgiarrusso: perhaps I should email him!15/12 19:13
srpxpgiarrusso: how did you know his works?15/12 19:13
pgiarrussogot pointers to the self-types for pretty unrelated reasons15/12 19:15
pgiarrussoit’s similar to some object-oriented type system I care about 😅15/12 19:16
srpxah, I see! interesting15/12 19:16
pgiarrussoregarding changing from CoC to PTS... well, really not sure15/12 19:17
pgiarrussofor all I know, compiling that PTS implementation I linked with GHC.js is a better idea15/12 19:17
srpxso I dont get pts indeed15/12 19:20
pgiarrussosrpx: wait, *you* are MaiaVictor, right?15/12 19:22
srpxpgiarrusso: yes, why?15/12 19:23
pgiarrussosrpx: we’ve crossed before, and I remember I’ve classified you as clever15/12 19:25
pgiarrusso(I’m also Blaisorblade)15/12 19:25
pgiarrusso(and I’m also on #dependent)15/12 19:25
pgiarrussoand also, because I was confused you posted a secret gist from MaiaVictor :-)15/12 19:26
pgiarrussoand I remember you asked some question and I got confused and my answer turned out to be somewhat unhelpful :-(15/12 19:27
srpxOh, really? Outside IRC? I'd love to know when was that! And sorry about that question :(15/12 19:28
srpx(And Girard, Stump and cia are clever, I'm an ant merely trying to apply their works [and failing])...15/12 19:29
srpxBut that's cool nether less, small world15/12 19:29
pgiarrussoon cstheory.stackexchange.com and on ##dependent15/12 19:29
srpxOh, I see15/12 19:29
pgiarrussoalso, sorry, I’m trying to stop saying “clever”: http://composition.al/blog/2015/04/30/say-experts-instead-of-smart-people/15/12 19:30
srpxcstheory is a fun place, the few answers I get there are infinitely useful and often change completely how I view a subject, but it is so hard to get them15/12 19:30
pgiarrussothis stuff just takes lots of time to get, “clever” doesn’t mean you get it in five minutes15/12 19:31
pgiarrussomore like 5 months15/12 19:31
srpx"If I am told over and over that I am smart, then it gets harder and harder for me to publicly admit to not knowing the things I don’t know."15/12 19:33
srpxI'm glad I'm in a point where I just openly admit I'm a fucking retard that has no idea what he's doing. People aren't less helpful because of that and this keeps the pressure low so I can build the things I want. Perfect lol15/12 19:34
pgiarrussoso, when Andrew Appel a few years ago wanted a very small proof checker, this is what he built, using the smallest corner of the lambda cube: https://www.cs.princeton.edu/~appel/papers/flit.pdf15/12 19:49
srpxamazing! thanks15/12 19:59
mietekpgiarrusso: nice link15/12 23:26

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