Logs: freenode/#haskell
| 2021-03-28 14:44:34 | × | acidjnk_new quits (~acidjnk@p200300d0c72b9586d8aaf3880c64deb7.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2021-03-28 14:46:06 | <edwardk> | ski: managed to get them to all shake out, actually. |
| 2021-03-28 14:46:22 | <ski> | so, falling out, naturally ? |
| 2021-03-28 14:46:37 | <kuribas> | Uniaika: btw, I tested my xml parser on a big xml, and reasonably complex parser. It works like a charm, the errors are precise and clear. Definitely worth our time :) |
| 2021-03-28 14:46:45 | <edwardk> | https://github.com/ekmett/linear-logic/blob/main/src/Linear/Logic.hs and https://github.com/ekmett/linear-logic/blob/main/src/Linear/Logic/Functor.hs used to be full of them |
| 2021-03-28 14:46:51 | <Uniaika> | kuribas: ah, glorious!! :) |
| 2021-03-28 14:46:56 | <Uniaika> | I'm happy for you |
| 2021-03-28 14:47:34 | <kuribas> | Uniaika: I cannot imagine how painful debugging xml-conduit must be... |
| 2021-03-28 14:48:06 | <ski> | (reminds me of how i managed to remove all `undefined's from some code, by replacing `ContT () M' by `ContT Void M'. using `Void' kept me straight/sane, so that i could convince myself that the original `undefined's would never have been triggered (i didn't need to use `void :: Void -> a', in this piece of code)) |
| 2021-03-28 14:48:17 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:6df1:6df7:a151:690b) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-03-28 14:48:18 | <edwardk> | ski: well, when working with _'s to derive the terms you need them to hack around the lack of correct usage info. so you slip in Unsafe.Linear.toLinear's a bunch and i have an unsafePar combinator that i use instead of my par constructor to build ⅋'s while I have a definition flayed open. |
| 2021-03-28 14:48:33 | <edwardk> | But once the definition is done, I can go through and strip all that stuff out |
| 2021-03-28 14:48:38 | <edwardk> | and get a nice safe haskelly definition |
| 2021-03-28 14:48:44 | × | ixlun quits (~matthew@109.249.184.133) (Read error: Connection reset by peer) |
| 2021-03-28 14:48:45 | <Uniaika> | kuribas: and we will probably never know! As a matter of fact, I almost entirely forgotten the details of our session together |
| 2021-03-28 14:49:08 | <siers> | Hi! I wanted to write a data record that would have an parametric existential type which the compiler could inline and specialize typeclass instances. I wrote it like this (only with single type for now) and it might work the way I want, but the data record updates aren't implemented. Is there a different way to do this? |
| 2021-03-28 14:49:10 | <siers> | http://sprunge.us/5Ui15a?haskell |
| 2021-03-28 14:49:14 | <kuribas> | Uniaika: basically you told me to write unit tests, we did and then I found the error rather quickly :) |
| 2021-03-28 14:49:35 | <Uniaika> | kuribas: ah yes, now I recall, the never-ending parsing stuff |
| 2021-03-28 14:49:59 | <Uniaika> | siers: why do you hate yourself so much? |
| 2021-03-28 14:50:08 | <siers> | Uniaika, :) |
| 2021-03-28 14:50:15 | <edwardk> | but this appears to give a model of full intuitionistic linear logic, all 4 connectives with all the laws interoperating them, along all 4 of Top, Bot, 0 and 1 as distinct entities. |
| 2021-03-28 14:50:24 | <siers> | Uniaika, tell me |
| 2021-03-28 14:50:24 | <Uniaika> | just write the damn SPECIALISE by hand :P |
| 2021-03-28 14:50:45 | <Uniaika> | < siers> Uniaika, tell me // nope, I'm not foraging into your psyche today :P |
| 2021-03-28 14:51:01 | <ski> | edwardk : oh, you're doing something like Mike Shulman's approach |
| 2021-03-28 14:52:14 | <ski> | hm |
| 2021-03-28 14:53:28 | <mniip> | it's a little hard to say what the approach actually is |
| 2021-03-28 14:54:02 | <mniip> | since the original paper kind of calls for a category bifibered over Hask |
| 2021-03-28 14:54:13 | <edwardk> | ski: yeah this is shulman's approach but extended to allow me to offer a real linear logic rather than affine logic, because i have more distinctions available in the target language |
| 2021-03-28 14:54:25 | <mniip> | but here (P+, P-) is actually represented by its P+ part |
| 2021-03-28 14:54:40 | <mniip> | with the P+ to P- mapping being assigned by type family |
| 2021-03-28 14:54:48 | <mniip> | which we can do because we're in an open kind |
| 2021-03-28 14:55:02 | <edwardk> | yeah |
| 2021-03-28 14:55:31 | <edwardk> | we have newtypes upon which to hang the types of refutations |
| 2021-03-28 14:55:48 | <mniip> | another thought is, what if we talk about the algebra synthetically |
| 2021-03-28 14:55:53 | <edwardk> | but unlike shulman's approach none of our connectives actually coincide exactly in terms of how positive evidence works |
| 2021-03-28 14:56:14 | <mniip> | we model Not as (P+, P-) mapsto (P-, P+) but what if we made it a syntactical operation |
| 2021-03-28 14:56:15 | <edwardk> | because we have fine enough distinctions in the target that With and (*) no longer have the same positive form |
| 2021-03-28 14:56:51 | <edwardk> | i'm somewhat inclined to try to model the positive connectives as Not's of the negative connectives. |
| 2021-03-28 14:56:52 | <edwardk> | why? |
| 2021-03-28 14:57:01 | <mniip> | we have a bifibration Chu(Hask, 0) -> Hask x Hask^op |
| 2021-03-28 14:57:06 | <edwardk> | i made the negative connectives polymorphic in their runtime representations ;) |
| 2021-03-28 14:57:19 | <mniip> | syntactically that's evidenced by the modality monads/comonads |
| 2021-03-28 14:57:21 | <edwardk> | that would let me do the entire logic unboxed. |
| 2021-03-28 14:58:36 | <mniip> | so really instead of looking at Chu(Hask, 0) |
| 2021-03-28 14:58:46 | <mniip> | we're looking at Hask ~ Chu(C, 0) for some C we don't talk about |
| 2021-03-28 14:58:56 | <edwardk> | yeah |
| 2021-03-28 14:58:57 | <mniip> | I think that's what it is at least |
| 2021-03-28 14:59:05 | <edwardk> | that sounds right |
| 2021-03-28 14:59:38 | <mniip> | that kind of explains why Why is so weird |
| 2021-03-28 14:59:55 | <mniip> | because it comes from an adjunction with C which we haven't talked about |
| 2021-03-28 14:59:57 | × | cantstanya quits (~chatting@gateway/tor-sasl/cantstanya) (Ping timeout: 240 seconds) |
| 2021-03-28 15:01:07 | <mniip> | 1616943426 [17:57:06] <edwardk> i made the negative connectives polymorphic in their runtime representations ;) |
| 2021-03-28 15:01:11 | <mniip> | do you have an unboxed Y yet |
| 2021-03-28 15:01:23 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-03-28 15:01:25 | <edwardk> | ooh |
| 2021-03-28 15:01:48 | <mniip> | just kidding you can't |
| 2021-03-28 15:01:54 | <edwardk> | i think the pattern synonym overhead that manufactured the proof would be larger |
| 2021-03-28 15:02:12 | <mniip> | this goes back to the unboxed Refl threada |
| 2021-03-28 15:02:18 | <edwardk> | (# Proxy# a | Proxy# b #) |
| 2021-03-28 15:02:20 | <ski> | unrelatedly, would any of you happen to know what coherence condition one should have, if one wanted to "lift" a free functor over another (with the same domain category) ? i was thinking we may want the forgetfuls in a pullback, and then maybe also the frees in a pushout ? and what are reasonably coherence conditions ? |
| 2021-03-28 15:02:38 | <edwardk> | is a machine int |
| 2021-03-28 15:02:48 | <mniip> | actually I'd love to fix the unboxed Refl story |
| 2021-03-28 15:02:48 | <edwardk> | you were saying? |
| 2021-03-28 15:02:55 | <mniip> | but I'm not sure how |
| 2021-03-28 15:02:56 | ski | looks at Gurkenglas |
| 2021-03-28 15:02:57 | <edwardk> | oh wait |
| 2021-03-28 15:03:00 | <edwardk> | that doesn't quite work |
| 2021-03-28 15:03:46 | <mniip> | apparently coercions are second class citizens in core |
| 2021-03-28 15:04:01 | <mniip> | (why?) |
| 2021-03-28 15:04:02 | <edwardk> | (# Refl# a c | Refl# b c #) -- where we need the coercion to come into scope when you match on Refl# by evil pattern synonym magic |
| 2021-03-28 15:04:02 | → | cantstanya joins (~chatting@gateway/tor-sasl/cantstanya) |
| 2021-03-28 15:04:25 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) |
| 2021-03-28 15:04:57 | <mniip> | wait |
| 2021-03-28 15:05:08 | <mniip> | richard's main argument was that coercions should terminate |
| 2021-03-28 15:05:28 | <mniip> | and hence CoVars are special beasts that only refer to "evaluated" coercions |
| 2021-03-28 15:05:40 | <mniip> | but don't we have the exact same story for unlifted bindings |
| 2021-03-28 15:05:55 | <edwardk> | yes, my Refl# here has to be a zero width object with a rule that says when you pattern match on it ito manufacture the (~) witness in a pattern synonym out of yolo fresh air. |
| 2021-03-28 15:05:58 | <ski> | how's `Refl#' defined ? |
| 2021-03-28 15:06:19 | <mniip> | likely Void# |
| 2021-03-28 15:06:26 | <mniip> | with a pattern synonym with unsafeCoerce# in it |
| 2021-03-28 15:06:41 | <mniip> | I'd really love to be able to define Refl# as an unlifted newtype over (~) |
| 2021-03-28 15:06:43 | <mniip> | that would be sick |
| 2021-03-28 15:06:47 | <mniip> | but there be dragons |
| 2021-03-28 15:06:53 | <edwardk> | newtype Refl a b = Refl (# #) -- pattern Refl# :: () => (a ~ b) => Refl# a b -- by using an evil unsafeCoerce Refl'd to manufacture the witness |
| 2021-03-28 15:07:54 | <edwardk> | er Refl#'s for the first two in that line |
| 2021-03-28 15:08:14 | <mniip> | I prefer calling it :~:# for consistency |
| 2021-03-28 15:08:21 | <edwardk> | yeah |
| 2021-03-28 15:08:22 | <mniip> | Refl# :: a :~:# a |
| 2021-03-28 15:08:24 | <edwardk> | its :~:# |
| 2021-03-28 15:08:57 | <edwardk> | though here i might as well just define Y# a b c as a Int# internally and build the two proofs manually rather than generalize |
| 2021-03-28 15:09:00 | <edwardk> | to reduce overhead |
| 2021-03-28 15:09:22 | × | _ashbreeze_ quits (~mark@64.85.214.234.reverse.socket.net) (Remote host closed the connection) |
| 2021-03-28 15:09:35 | <mniip> | what is the rep of (# a ~ b | c ~ d #) anyway? |
| 2021-03-28 15:09:45 | <mniip> | a register and two zero width slots? |
| 2021-03-28 15:09:50 | <edwardk> | yeah |
| 2021-03-28 15:09:54 | <edwardk> | one zero width |
| 2021-03-28 15:09:58 | <mniip> | er right |
| 2021-03-28 15:10:35 | → | _ashbreeze_ joins (~mark@64.85.214.234.reverse.socket.net) |
All times are in UTC.