[02:19:20] * FreeFull [FreeFull!~freefull@defocus/sausage-lover] has quit (Quit: Rebooting). [02:21:44] * FreeFull [FreeFull!~freefull@defocus/sausage-lover] has joined the channel. [04:24:10] * jtimon [jtimon!~quassel@245.30.134.37.dynamic.jazztel.es] has quit (Ping timeout: 260 seconds). [06:18:25] * rgrinberg [rgrinberg!~rgrinberg@24-246-56-85.cable.teksavvy.com] has quit (Ping timeout: 240 seconds). [07:28:56] * shikhin [shikhin!shikhin@unaffiliated/shikhin] has quit (Ping timeout: 255 seconds). [07:30:17] * bmp [bmp!sid22344@gateway/web/irccloud.com/x-nrfrmguwbakvjzzc] has quit (Ping timeout: 255 seconds). [07:30:44] * mbrock [mbrock!sid76765@gateway/web/irccloud.com/x-nnirpywbnnmgbwkz] has quit (Ping timeout: 255 seconds). [07:33:33] * shikhin [shikhin!shikhin@unaffiliated/shikhin] has joined the channel. [07:33:48] * bmp [bmp!sid22344@gateway/web/irccloud.com/x-tkfwqbeyjcnfwvuy] has joined the channel. [07:34:10] * mbrock [mbrock!sid76765@gateway/web/irccloud.com/x-nnheccrnktqddwew] has joined the channel. [08:01:41] * Sgeo [Sgeo!~Sgeo@ool-18e4354b.dyn.optonline.net] has quit (Read error: Connection reset by peer). [08:04:47] * Sgeo [Sgeo!~Sgeo@ool-18e4354b.dyn.optonline.net] has joined the channel. [09:04:19] * doublec [doublec!~doublec@unaffiliated/doublec] has quit (Ping timeout: 255 seconds). [09:05:06] * doublec [doublec!~doublec@unaffiliated/doublec] has joined the channel. [11:46:44] * jtimon [jtimon!~quassel@245.30.134.37.dynamic.jazztel.es] has joined the channel. [12:03:26] * jtimon [jtimon!~quassel@245.30.134.37.dynamic.jazztel.es] has quit (Ping timeout: 240 seconds). [13:27:17] * amuck [amuck!~amuck@irc.harug.com] has quit (Ping timeout: 240 seconds). [13:29:22] * amuck [amuck!~amuck@2001:19f0:8001:13b:5400:ff:fe3f:cad9] has joined the channel. [14:34:44] * dondy [dondy!~dondy@x4db3cced.dyn.telefonica.de] has joined the channel. [15:33:58] * jtimon [jtimon!~quassel@245.30.134.37.dynamic.jazztel.es] has joined the channel. [16:18:48] * jtimon [jtimon!~quassel@245.30.134.37.dynamic.jazztel.es] has quit (Ping timeout: 245 seconds). [16:26:46] * jtimon [jtimon!~quassel@245.30.134.37.dynamic.jazztel.es] has joined the channel. [17:29:56] * jtimon [jtimon!~quassel@245.30.134.37.dynamic.jazztel.es] has quit (Ping timeout: 240 seconds). [17:30:05] * jamtho [jamtho!33075a2a@gateway/web/freenode/ip.51.7.90.42] has joined the channel. [17:50:20] * jamtho [jamtho!33075a2a@gateway/web/freenode/ip.51.7.90.42] has quit (Ping timeout: 260 seconds). [20:28:49] * migge [migge!~Thunderbi@ip-62-143-242-0.hsi01.unitymediagroup.de] has joined the channel. [20:34:39] * evincar [evincar!uid207128@gateway/web/irccloud.com/x-wdhldtrggbrffiwp] has joined the channel. [20:55:28] hi evincar [20:56:37] erg: Ahoy [20:57:18] It looks like I've got some people interested in helping with Kitten [20:57:29] So I figured I should hang out here more consistently [20:57:38] i've been reading about idris and such. why are you against dependent types in Kitten? [20:59:06] i can pretty much follow all the type theory notation now. yay [20:59:17] Cool :) [20:59:21] I'm not against them exactly [20:59:52] It would just be more design/implementation work in the typechecker [21:00:10] or more design but less work? [21:00:36] I suppose so [21:00:40] i'm sure you've read that Simply Easy! paper [21:00:44] Yeah [21:02:51] I like the state of things in the type system right now [21:03:20] But there'll probably be more features for dependently typed programming in the future [21:03:41] do you have a plan for tactics in kitten? [21:05:06] Nope, I [21:05:23] ...'m not even that familiar with them [21:05:27] Something to do with proof search? [21:16:13] http://typetheorypodcast.com [21:16:52] in the idris one, he mentions that he started writing idris's typechecker from scratch and it turned out to basically be a theorem-proving engine [21:17:12] tactics, like in coq [21:38:24] * rgrinberg [rgrinberg!~rgrinberg@24-246-56-85.cable.teksavvy.com] has joined the channel. [22:37:06] * rgrinberg [rgrinberg!~rgrinberg@24-246-56-85.cable.teksavvy.com] has quit (Ping timeout: 240 seconds). [23:50:44] evincar: Saw kitten on HN the other day; congrats. [23:57:17] jeaye: Thanks :) [23:57:29] It's growing beyond my control now, I guess [23:57:39] And the thing doesn't even really work yet [23:59:25] :D