[00:13:23] * xkapastel [xkapastel!uid17782@gateway/web/irccloud.com/x-lhzfqgpcxcjhekft] has joined the channel.
[01:05:27] <xkapastel> so i'm trying to figure out how to do type theory in a concatenative style
[01:05:35] <xkapastel> and it kinda feels like, for dependent types, it doesn't actually work
[01:07:09] <xkapastel> i think the composition rule for nondependent types looks like `G :- f : [B1 B0] [A] ->, G :- g : [C] [B0] -> => G :- fg : [B1 C][A] ->`
[01:07:21] <xkapastel> (notation is [codomain][domain] ->)
[01:07:43] <xkapastel> but for dependent types you need to refer to the actual value you got of that type, since the codomain is a type family and not just a type
[02:31:12] * [X-Scale] [[X-Scale]!~ARM@214.20.108.93.rev.vodafone.pt] has joined the channel.
[02:32:31] * X-Scale [X-Scale!~ARM@214.20.108.93.rev.vodafone.pt] has quit (Ping timeout: 260 seconds).
[02:32:32] * [X-Scale] is now known as X-Scale
[06:45:27] * jtimon [jtimon!~quassel@70.30.134.37.dynamic.jazztel.es] has quit (Ping timeout: 260 seconds).
[07:54:56] * xkapastel [xkapastel!uid17782@gateway/web/irccloud.com/x-lhzfqgpcxcjhekft] has quit (Quit: Connection closed for inactivity).
[12:18:45] * rudha [rudha!~rudha@80.32.17.95.dynamic.jazztel.es] has joined the channel.
[12:49:18] * proteusguy [proteusguy!~proteus-g@125.162.138.147] has joined the channel.
[12:56:57] * proteusguy [proteusguy!~proteus-g@125.162.138.147] has quit (Ping timeout: 256 seconds).
[15:02:30] * proteusguy [proteusguy!~proteus-g@125.162.138.147] has joined the channel.
[15:24:03] * proteusguy [proteusguy!~proteus-g@125.162.138.147] has quit (Ping timeout: 258 seconds).
[15:35:02] * rudha [rudha!~rudha@80.32.17.95.dynamic.jazztel.es] has quit (Quit: Leaving).
[15:35:54] * shapr [shapr!~shapr@haskell/developer/shapr] has left the channel ("ERC Version 5.3 (IRC client for Emacs)").
[16:39:43] * jtimon [jtimon!~quassel@70.30.134.37.dynamic.jazztel.es] has joined the channel.
[20:34:56] * jtimon [jtimon!~quassel@70.30.134.37.dynamic.jazztel.es] has quit (Ping timeout: 240 seconds).
[21:28:13] * jtimon [jtimon!~quassel@70.30.134.37.dynamic.jazztel.es] has joined the channel.
[22:11:18] * klltkr [klltkr!~klltkr@unaffiliated/klltkr] has joined the channel.