[00:02:23] * MDude [MDude!~MDude@pa-67-234-118-37.dhcp.embarqhsd.net] has quit (Ping timeout: 276 seconds). [00:56:21] * MDude [MDude!~MDude@pa-67-234-118-37.dhcp.embarqhsd.net] has joined the channel. [04:49:40] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has quit (Quit: Poof). [04:49:58] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has joined the channel. [05:12:05] * evincar [evincar!~jon@173-228-12-189.dsl.dynamic.fusionbroadband.com] has joined the channel. [05:22:38] maaku: Re your question about statically typing match expressions on 21 May, what I do is say "match case left { L } case right { R }" has type "S..., Either -> T..." where L has type "S..., A -> T..." and R has type "S..., B -> T...", i.e., the branches consume some input stack and the fields of the corresponding constructor, and produce some output stack, and these inputs and outputs must ma [05:22:44] tch [05:24:52] Where S... and T... are stack type variables (a chain of tuples) and A and B are inferred to be some particular types, whatever's actually in the Either you're matching on [05:27:31] In Haskell terms, "matchEither (left_case_body :: (s, a) -> t) (right_case_body :: (s, b) -> t) :: (s, Either a b) -> t" [05:31:19] The main observation is: case branches are the partial inverses of constructor functions. E.g., given "type Pair { case pair (A, B) }" (Haskell: "data Pair a b = Pair a b") the constructor "pair" has type "S..., A, B -> S..., Pair", and "match case pair {}" has type "S..., Pair -> S..., A, B" [05:31:37] They are inverses, and in this case a total inverse because Pair has only one constructor, so the match is irrefutable [05:32:33] When you add stuff to the case blocks, you're supplying continuations, one of which will be applied to the fields of the constructor that matches [05:33:47] It's just like Böhm-Berarducci encoding, representing a data type with a fold; in Haskell, say, "either :: (a -> r) -> (b -> r) -> Either a b -> r" [05:34:57] In concatenative-land you just do the same thing on a stack [05:45:36] So then, if case branches are partial functions, you just need a way to combine partial functions to get a total function. [05:46:22] Then you can easily encode any algebraic type. [05:55:39] hackerfoo: Yup, and I do this syntactically like typical functional languages, but you could do it in another way [05:57:20] You don't even strictly need datatypes; they can be desugared to Böhm-Berarducci encoding and matched in that CPSy way, which generally has pretty good performance [05:57:52] Furthermore, since any function composed after a case statement could always be moved into each branch, there is no reason that the resulting types have to match. [05:59:34] type Either a b = forall r. (a -> r) -> (b -> r) -> r; left x = \ l _ -> l x; right x = \ _ r -> r x; matchEither l r x = x l r [06:00:20] Uh, provided the function works for all of the types the branches do return, I guess :P [06:02:46] Converting "match case left {} right {} k" would ordinarily work only on Either, but if you duplicate the continuation into the branches like "match case left {k} case right {k}", then that might be type-correct if k is polymorphic enough (trivial example: suppose k is "drop") [06:03:04] Not necessarily. You can still select what branches to handle, resulting in a partial function that can be completed by combination with something that handles the other cases in another way. [06:03:44] Example? [06:05:17] I don't find it onerous at all to restrict match branches to the same type, especially since you can easily take & return any additional values you want from the branches [06:05:44] And it has saved me from many a bug [06:06:45] f g | h 0 default [06:07:34] where f :: A -> B, g :: C -> D, h :: B -> Int [06:08:52] `x y default` returns `x` unless it fails, in which case it returns `y` [06:10:38] So it is equivalent to `f h 0 default`, and passing something of type C always returns 0. [06:11:41] So a more restrictive function has the effect of pruning cases before it. [06:12:20] So...because the f branch fails, g isn't even tried? [06:13:15] Or if the g branch is tried, what happens to the D that would result? Is it just ignored (and...therefore not computed)? [06:13:16] Right. There is no reason to try g, because h would fail anyway. [06:13:32] Ah, got it [06:16:48] default is not a primitive: https://github.com/HackerFoo/poprc/blob/master/lib.ppr#L272 [06:17:33] It's built from a weird primitive called otherwise, which is the dual of ! [06:18:34] It fails if the first argument doesn't fail, otherwise it returns the second argument. [06:19:24] I found this while studying linear logic and trying to implement logical negation. [06:21:11] It matches the semantics of a default case, which only succeeds when all other cases fail. [06:23:02] But freed from a case expression, it can be also used to implement error handling and something like default methods. [06:31:21] * tgunr [tgunr!~tgunr@cpe-76-173-89-2.hawaii.res.rr.com] has quit (Quit: My MacBook has gone to sleep. ZZZzzz…). [07:34:25] * delvinj [delvinj!~Miranda@c-73-164-9-150.hsd1.mn.comcast.net] has quit (Ping timeout: 248 seconds). [08:02:44] * erkin [erkin!~erkin@unaffiliated/erkin] has quit (Quit: Ouch! Got SIGIRL, dying...). [09:38:48] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has quit (Quit: Poof). [09:39:04] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has joined the channel. [09:42:21] * werkin [werkin!~erkin@unaffiliated/erkin] has joined the channel. [10:55:38] * evincar [evincar!~jon@173-228-12-189.dsl.dynamic.fusionbroadband.com] has quit (Ping timeout: 276 seconds). [11:25:02] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has quit (Ping timeout: 255 seconds). [11:58:20] * werkin [werkin!~erkin@unaffiliated/erkin] has quit (Quit: Leaving). [12:02:03] * werkin [werkin!~erkin@unaffiliated/erkin] has joined the channel. [12:44:41] * werkin [werkin!~erkin@unaffiliated/erkin] has quit (Quit: Leaving). [12:53:24] * delvinj [delvinj!~Miranda@c-73-164-9-150.hsd1.mn.comcast.net] has joined the channel. [13:03:45] * werkin [werkin!~erkin@unaffiliated/erkin] has joined the channel. [14:18:09] * werkin [werkin!~erkin@unaffiliated/erkin] has quit (Quit: Leaving). [14:29:24] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has joined the channel. [14:34:27] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has quit (Remote host closed the connection). [14:41:25] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has joined the channel. [16:23:14] * erkin [erkin!~erkin@unaffiliated/erkin] has joined the channel. [16:49:20] * jtimon [jtimon!~quassel@40.28.134.37.dynamic.jazztel.es] has joined the channel. [17:04:03] evincar, ok that matches up with my own understanding [17:04:15] but fyi that's not what some of the kitten docs show [17:06:14] * tgunr [tgunr!~tgunr@cpe-76-173-89-2.hawaii.res.rr.com] has joined the channel. [17:06:43] the tutorial (iirc?) shows that de-quoting a sum-type places its actual value on the stack, which has dependent typing [17:47:39] * obfusk [obfusk!~quassel@relto.rasusan.nl] has quit (Remote host closed the connection). [18:44:42] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has quit (Quit: Poof). [18:45:00] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has joined the channel. [19:13:50] * obfusk [obfusk!~quassel@relto.rasusan.nl] has joined the channel. [19:41:07] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has quit (Quit: Poof). [19:41:24] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has joined the channel. [20:05:32] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has quit (Read error: Connection reset by peer). [20:16:22] * pierpal [pierpal!~pierpal@host23-9-dynamic.16-87-r.retail.telecomitalia.it] has joined the channel. [20:25:49] * evincar [evincar!~jon@173-228-12-189.dsl.dynamic.fusionbroadband.com] has joined the channel. [20:29:33] maaku: If the Kitten docs are misleading, I [20:29:37] 'm happy to fix them [20:29:46] I can't find what you're referring to though [20:32:15] Are you talking about "A match expression takes an instance of an ADT, matches on its tag, and unpacks its fields (if any) onto the stack so they can be manipulated."? [20:32:57] That should probably be clarified with some examples of how the fields are unpacked *within each branch* and not just...willy-nilly [21:43:28] * pierpa [pierpa!57100917@gateway/web/freenode/ip.87.16.9.23] has joined the channel. [22:26:38] * erkin [erkin!~erkin@unaffiliated/erkin] has quit (Quit: Ouch! Got SIGIRL, dying...).