[00:03:41] I think I need to have a go with Coq or Idris or something to get a grasp on dependent types [00:04:00] There's also Agda [00:04:39] https://softwarefoundations.cis.upenn.edu/current/index.html [00:04:54] I'm still working through that book. [00:05:06] the thing about Agda is it doesn't really do proof tactics [00:05:40] I tried to do CPDT book (on Coq) but only got so far through it [00:05:41] It seems to be what they're using in ##dependent, though. [00:06:19] heh the thing you linked I did come across quite recently [00:06:46] it just looked very much too long for me [00:07:03] You wouldn't happen to be in the San Francisco area, would you? There's a meetup working through Software Foundations. [00:07:31] nah I'm in the UK [00:08:12] Ah. The answer is yes surprisingly often. [00:09:09] heh I even had your link bookmarked already [00:09:15] didn't even notice [00:09:19] Slava Pestov showed up to a presentation here on my language, which was nice. [00:10:49] cool, he doesn't seem to have been blogging or anything much recently though [00:10:57] As well as Jon Purdy, who is working on Kitten, which he also did a presentation on earlier. [00:11:25] Kitten looked a bit messy somehow... kinda like my language but not sure if I want to get my head around it [00:11:33] He's constantly on Twitter, posting cat pics :) [00:12:07] oh dear [00:12:57] (These guys hang out here sometimes, too) [00:13:40] Or use to, until the spam/content ratio hit infinity. [00:15:01] but no one spams IRC [00:15:32] except us of course ;) [00:16:41] the Kitten website is a bit lacking in content to be honest [00:17:32] there at least should be more examples and a way to see the various syntax [00:19:10] and having infix operators is just weird [00:19:31] I only have them in so far as you can write (code)_+_(code) [00:20:11] ((b-~)_+_(sqrt((b 2^)_-_(4 a*c*))))_/_(2 a*) [00:20:37] it does make it kinda readable! [00:36:58] my brain still can't make the mapping from dependent product types into stack effects like types [00:41:02] λx.b : ∏(x:A) B(x) [00:41:39] I know if you have ∏(_:A) B that's the same as A -> B [01:23:59] heh http://lambda-the-ultimate.org/node/1299 [01:31:03] to be fair Sigma -> S -> Sum, Pi -> P -> Product [01:31:42] just remember that dependent sum is a product and dependent product is a function [01:32:49] Yeah, confusing. Just ignore the normal meanings assigned to the commonly used greek characters. [01:33:30] I wish they would just name math operators, instead of recycling Greek characters. [01:33:40] lol [01:34:48] I can often read source in any executable language and gain intuition much quicker than reading a paper describing the algorithm with tons of Greek symbols. [01:35:03] Plus there more chance of it being correct. [01:35:09] *there's [01:35:27] hey you were promoting Agda just before [01:36:06] mentioned != promoted [01:36:35] it was more than a mention but anyway I am interested in it, I just don't like how it relies on Axiom K to work properly [01:36:36] But the ##dependent people like it, and they seem smart. [01:36:51] maybe once you know what you're doing Agda is a good place to be [01:38:36] My preferred approach is to let my need for and understanding of theory to grow at about the same rate, alternating between practice and research. [01:38:51] If you get ahead on either one, it can cause problems. [01:39:31] I'm definitely well behind on theory [01:39:46] I've sort of assumed the theory exists and ran ahead with it [01:39:48] Same here. [01:40:28] Although I think the theory I need is slightly different from what is available. [01:40:35] same [01:40:51] So much effort goes into bindings, which I've kind of side-stepped. [01:40:59] but I think as an open problem existing theories can be combined to get what I need [01:41:50] Some papers start with combinators as a simple case, and then move on to lambda calculus. [01:44:10] I'm wondering if I could encode [popn]?[n times[`@] #n =>] [01:45:00] using => for the stack effect arrow since I use -> for logical implication [01:45:59] I don't think it works though since times[`@] would require them all to be the same type mmh [01:47:27] How often would you need such an operation where n is not static? [01:47:56] I don't think that matters, if you need it at all [01:49:57] I should maybe just introduce a symbol like _ for an any type [01:50:49] or rather "I don't care" type [01:52:42] hah I've spotted a bug [01:56:01] What bug? [01:56:13] overn had an off by 1 error [01:56:55] I'm struggling to write a type for this one [01:58:43] [overn]?[`@t {n times[_]}@ts t ts.. #n => t ts.. t] [02:00:12] for all t, and ts of length n, that stack effect [02:01:26] I feel like _ is a bit side-effecty [02:01:41] like "create a new unification variable" [02:02:16] I don't think the "don't care" semantics is much good here [02:10:04] I may just change the semantics of unification variables inside quotations so I can just use [`@] and be done with it :) [02:11:31] if you really wanted the same one you could give it a name outside [02:13:52] [dupn]?[{n times[`@]}@ts ts.. #n => ts.. ts..] [02:41:12] @dip?[`@v `@xs `@ys xs.. v [xs.. => ys..] => ys.. v]: #v#f f# v [02:41:55] Cat gives ('A 'b ('A -> 'C) -> 'C 'b) [02:45:30] @dipn?[`@xs `@ys {n times:`@}@vs xs.. vs.. [xs.. => ys..] => ys.. vs..] [03:01:54] here's where things get interesting [03:02:01] @_?#_?[xs.. bool [xs.. ys..] [xs.. zs..] => [ys..]|[zs..]#]: ? # [03:03:11] instead of forcing the functions to be the same type [03:03:18] rather @_?#_?[xs.. bool [xs.. => ys..] [xs.. => zs..] => [ys..]|[zs..]#]: ? # [03:03:56] [if] #type in Cat gives ('A bool ('A -> 'B) ('A -> 'B) -> 'B) [03:13:13] wtf Cat S2 = (S2 int) wth [03:13:51] tl;dr Cat gives totally bogus types [03:17:58] this is pretty bad, I can't trust this thing [03:20:37] * MDude [MDude!~MDude@c-73-187-225-46.hsd1.pa.comcast.net] has quit (Ping timeout: 260 seconds). [03:22:15] so either if is useless if the type system worked, or if is useful and you can't give it a useful type in Cat [04:17:40] * jtimon [jtimon!~quassel@117.29.134.37.dynamic.jazztel.es] has quit (Ping timeout: 240 seconds). [05:59:14] * FreeFull [FreeFull!~freefull@defocus/sausage-lover] has quit. [07:32:50] * rudha [rudha!~rudha@p200300760E7BD9F2D9990A6A2BABF150.dip0.t-ipconnect.de] has joined the channel. [09:19:26] * proteusguy [proteusguy!~proteus-g@49.228.118.146] has joined the channel. [10:34:10] * jtimon [jtimon!~quassel@117.29.134.37.dynamic.jazztel.es] has joined the channel. [14:47:37] is Cat just lacking https://en.wikipedia.org/wiki/Occurs_check [15:17:10] * rotty [rotty!~rotty@yade.chaostreff.at] has quit (Ping timeout: 260 seconds). [15:32:37] * rotty [rotty!~rotty@yade.chaostreff.at] has joined the channel. [16:12:01] * FreeFull [FreeFull!~freefull@defocus/sausage-lover] has joined the channel. [16:52:51] * jtimon [jtimon!~quassel@117.29.134.37.dynamic.jazztel.es] has quit (Remote host closed the connection). [17:25:44] * rotty [rotty!~rotty@yade.chaostreff.at] has quit (Ping timeout: 246 seconds). [17:52:56] * rotty [rotty!~rotty@yade.chaostreff.at] has joined the channel. [18:24:15] * jtimon [jtimon!~quassel@117.29.134.37.dynamic.jazztel.es] has joined the channel. [20:34:00] * kernelj [kernelj!~kernelj@unaffiliated/colonelj] has quit (Write error: Broken pipe). [20:42:52] * kernelj [kernelj!~kernelj@unaffiliated/colonelj] has joined the channel. [22:37:22] * flogbot [flogbot!~flogbot@2001:4800:7814:0:2804:b05a:ff04:4ba7] has quit (Ping timeout: 245 seconds). [22:37:31] * flogbot [flogbot!~flogbot@2001:4800:7814:0:2804:b05a:ff04:4ba7] has joined the channel. [22:37:31] :rajaniemi.freenode.net 353 flogbot = #concatenative :flogbot kernelj jtimon rotty FreeFull proteusguy rudha rgrinberg puckipedia otoburb shmibs flout carvite earl_ shachaf erg koisoke merry rjungemann jeaye ephe_meral groovy2shoes doublec diginet m_hackerfoo hackerfoo strmpnk dustinm`_ kanzure Sgeo jeremyheiler bmp PiDelport [22:37:31] :rajaniemi.freenode.net 366 flogbot #concatenative :End of /NAMES list.