[00:04:23] *** Joins: koo7 (~kook@236.152.broadband3.iol.cz) [00:07:37] *** Quits: koo7 (~kook@236.152.broadband3.iol.cz) (Read error: Connection reset by peer) [00:12:10] *** Joins: koo7 (~kook@236.152.broadband3.iol.cz) [00:15:40] *** Quits: koo7 (~kook@236.152.broadband3.iol.cz) (Read error: Connection reset by peer) [00:24:40] *** Joins: koo7 (~kook@37-48-35-253.tmcz.cz) [00:26:12] *** Parts: koo7 (~kook@37-48-35-253.tmcz.cz) () [03:49:39] *** Joins: koo7 (~kook@236.152.broadband3.iol.cz) [04:02:24] I don't understand the distinction between types with type variables and dependent types. [04:09:43] This post by neelk expaDependent types == first-order logic http://lambda-the-ultimate.org/node/1129#comment-12313 [04:11:33] *** Quits: spectei (~fran@unaffiliated/spectie) (Ping timeout: 244 seconds) [04:12:25] *** Quits: koo7 (~kook@236.152.broadband3.iol.cz) (Read error: Connection reset by peer) [04:13:08] *** Joins: koo7 (~kook@236.152.broadband3.iol.cz) [04:20:31] *** Joins: spectre (~fran@37.152.235.8) [04:21:59] Parametric type polymorphism is when the type variables range over types, but dependent type indexes range over values. [04:27:25] *** Quits: koo7 (~kook@236.152.broadband3.iol.cz) (Read error: Connection reset by peer) [04:27:57] Parametric type polymorphism is the Curry-Howard interpretation of second-order logic. [04:28:05] Dependent types are the Curry-Howard interpretation of first-order logic. [04:28:29] *** Joins: koo7 (~kook@236.152.broadband3.iol.cz) [04:33:36] Why are they important? [04:42:33] *** Quits: koo7 (~kook@236.152.broadband3.iol.cz) (Read error: Connection reset by peer) [04:43:52] *** Joins: koo7 (~kook@236.152.broadband3.iol.cz) [04:45:10] *** Quits: koo7 (~kook@236.152.broadband3.iol.cz) (Remote host closed the connection) [04:47:29] *** Joins: daherb_ (~daherb@ppp-93-104-169-54.dynamic.mnet-online.de) [04:50:26] *** Quits: daherb (~daherb@ppp-93-104-177-0.dynamic.mnet-online.de) (Ping timeout: 240 seconds) [04:54:12] By run-time, Haskell has no type information left, I think I read. Dependent types retain type information at run time, apparently. [07:17:52] *** Quits: drbean (~drbean@124.219.83.55) (Quit: ZNC - http://znc.in) [07:19:47] *** Joins: drbean (~drbean@124.219.83.178) [14:09:13] *** daherb_ is now known as daherb [14:45:10] *** Quits: spectre (~fran@37.152.235.8) (Ping timeout: 260 seconds) [16:48:58] *** Joins: spectre (~fran@2001:8b0:951:728:7a31:c1ff:fecd:969e) [20:52:38] *** Quits: Gurkenglas (Gurkenglas@dslb-188-103-074-033.188.103.pools.vodafone-ip.de) (Ping timeout: 272 seconds) [21:08:42] *** Joins: Gurkenglas (Gurkenglas@dslb-188-103-074-033.188.103.pools.vodafone-ip.de) [21:27:51] *** Quits: Gurkenglas (Gurkenglas@dslb-188-103-074-033.188.103.pools.vodafone-ip.de) (Ping timeout: 255 seconds) [21:40:37] *** Joins: Gurkenglas (~Gurkengla@dslb-188-103-074-033.188.103.pools.vodafone-ip.de) [21:46:45] *** Quits: Gurkenglas (~Gurkengla@dslb-188-103-074-033.188.103.pools.vodafone-ip.de) (Ping timeout: 255 seconds) [22:11:59] *** Joins: Gurkenglas (Gurkenglas@dslb-188-103-074-033.188.103.pools.vodafone-ip.de) [22:18:24] *** Quits: Gurkenglas (Gurkenglas@dslb-188-103-074-033.188.103.pools.vodafone-ip.de) (Ping timeout: 264 seconds) [22:43:31] *** Joins: Gurkenglas (Gurkenglas@dslb-188-103-074-033.188.103.pools.vodafone-ip.de) [22:50:12] *** Quits: Gurkenglas (Gurkenglas@dslb-188-103-074-033.188.103.pools.vodafone-ip.de) (Ping timeout: 264 seconds) [23:15:06] *** Joins: Gurkenglas (Gurkenglas@dslb-188-103-074-033.188.103.pools.vodafone-ip.de) [23:21:24] *** Quits: Gurkenglas (Gurkenglas@dslb-188-103-074-033.188.103.pools.vodafone-ip.de) (Ping timeout: 264 seconds) [23:46:41] *** Joins: Gurkenglas (Gurkenglas@dslb-188-103-074-033.188.103.pools.vodafone-ip.de) [23:53:12] *** Quits: Gurkenglas (Gurkenglas@dslb-188-103-074-033.188.103.pools.vodafone-ip.de) (Ping timeout: 264 seconds)