Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 416 417 418 419 420 421 422 423 424 425 426 .. 5022
— 502,152 events total
2020-10-05 01:20:55 × ericsagnes quits (~ericsagne@2405:6580:0:5100:a157:330d:992b:2b45) (Ping timeout: 240 seconds)
2020-10-05 01:20:56 <dolio> Yeah, extensional type theory can do it somehow, because the propositional equalities can be turned back into judgmental equalities.
2020-10-05 01:21:28 <ski> yea .. discarding the proof term. which seems like hocus pocus, to me
2020-10-05 01:22:06 <ski> (hopefully some version of HoTT will improve on this ?)
2020-10-05 01:22:08 <dolio> But, cubical type theory also allows it, basically because it has a mechanism for the variable thing.
2020-10-05 01:22:42 <dolio> You can abstract over a 'dimension' to prove the equality, and then you can give a lambda expression which is doing the variable abstraction.
2020-10-05 01:23:17 <dolio> I think that might be one of the insights of this paper, too: https://arxiv.org/abs/2008.08533
2020-10-05 01:23:55 <ski> oh, is that the square root thing ?
2020-10-05 01:24:39 <dolio> It's a generalization of that (apparently) and other stuff. I hadn't heard of the square root thing until this paper.
2020-10-05 01:24:52 <ski> (i recall reading about 2-dimensional (directed) type theory (Licata, iirc). thinking i could express some of the things there more nicely, with my notation)
2020-10-05 01:25:12 <ski> mhm. ty for the suggestion
2020-10-05 01:25:26 <dolio> Also one of the examples is fresh names in nominal logic, which seems like the sort of thing you'd need for this.
2020-10-05 01:25:41 <dolio> Or, one possible sort of thing.
2020-10-05 01:26:22 <ski> hm. i remember briefly taking a look at nominal logic, at some point, but not quite getting it, or possibly not quite liking it
2020-10-05 01:26:44 → conal joins (~conal@209.58.132.107)
2020-10-05 01:26:55 <dolio> Yeah, I think it's not ideal.
2020-10-05 01:26:58 ski . o O ( lambdaProlog,MacroML,MetaML,MetaOCaml )
2020-10-05 01:28:23 <dolio> Like, in this situation you want sort of a 'fresh variable of a type', but the variables in nominal logic aren't typed.
2020-10-05 01:29:50 <ski> and it's not entirely straight-forward to make a multi -sorted / -typed version of it ?
2020-10-05 01:30:08 <dolio> Well, I don't know. There are other things like that.
2020-10-05 01:30:22 <dolio> Like contextual modal type theory.
2020-10-05 01:30:38 <ski> mm. that's interesting, i recall
2020-10-05 01:30:42 → jle` joins (~mstksg@unaffiliated/mstksg)
2020-10-05 01:31:20 × dcoutts_ quits (~duncan@unaffiliated/dcoutts) (Remote host closed the connection)
2020-10-05 01:31:32 <ski> (relativizing the modality by a context, iirc)
2020-10-05 01:32:11 → nineonine joins (~nineonine@50.216.62.2)
2020-10-05 01:33:29 → snakemasterflex joins (~snakemast@213.100.206.23)
2020-10-05 01:34:19 → ericsagnes joins (~ericsagne@2405:6580:0:5100:97e:4c35:feee:3de8)
2020-10-05 01:34:30 ski . o O ( "A Combinatorial Theory of Formal Series" (about (combinatorial) species) by André Joyal in 1981 (partial (in-progress) translation by Brent A. Yorgey) at <http://ozark.hendrix.edu/~yorgey/pub/series-formelles.pdf> )
2020-10-05 01:35:59 <quintasan> https://github.com/nikita-volkov/hasql-tutorial1/blob/master/library/HasqlTutorial1/Transaction.hs – why is Write and Serializable visible in this file, I don't get it. My module is even simpler (https://pastebin.com/XD1nAVA4) but I'm getting Data constructor not in scope: Write. I'm pretty much sure Write and Serializable come from https://hackage.haskell.org/package/hasql-transaction-1.0.0.1/docs/Hasql-Transaction-Sessions.html
2020-10-05 01:37:38 → nbloomf joins (~nbloomf@2600:1700:83e0:1f40:68ef:3717:d255:fea6)
2020-10-05 01:38:01 <dolio> Anyhow, there's definitely work on HoTT-adjacent stuff that has a better story than the proof term just disappearing.
2020-10-05 01:38:04 × snakemasterflex quits (~snakemast@213.100.206.23) (Ping timeout: 272 seconds)
2020-10-05 01:38:24 <dolio> That's the sort of thing that makes things undecidable.
2020-10-05 01:38:56 × nbloomf quits (~nbloomf@2600:1700:83e0:1f40:68ef:3717:d255:fea6) (Client Quit)
2020-10-05 01:39:47 × murphy_ quits (~murphy_@2604:2000:1281:8a9e:79f9:b15f:8bb9:7d0e) (Ping timeout: 240 seconds)
2020-10-05 01:40:53 <dolio> I actually read a paper a couple days ago about how it's even a problem for constructing models in extensional type theory. Like, even if the extensional type theory is constructive, if you use its features to build a model for another theory, you end up with an uncomputable model.
2020-10-05 01:40:54 → murphy_ joins (~murphy_@2604:2000:1281:8a9e:c24e:de35:eb75:8dab)
2020-10-05 01:41:45 <dolio> Because the part that needs to be decidable in practice (judgmental equality) gets modelled by the undecidable extensional equality.
2020-10-05 01:41:50 <ski> quintasan : tried importing `Hasql.Transaction.Sessions' ?
2020-10-05 01:42:32 <ski> dolio : mhm, i see
2020-10-05 01:43:10 <quintasan> ski: Yeah, now it's even worse
2020-10-05 01:43:26 <quintasan> https://pastebin.com/mZKS16v8
2020-10-05 01:44:49 <quintasan> https://pastebin.com/G8M1XsMp without highlighting
2020-10-05 01:45:14 <quintasan> I'm having a bad time here, it's either me doing something wrong or the docs being wrong (I think it's the former)
2020-10-05 01:46:02 → ddellacosta joins (~dd@86.106.121.168)
2020-10-05 01:46:07 <quintasan> https://gitlab.com/Quintasan/teadb in case anyone wants to inspect what I've done https://gitlab.com/Quintasan/teadb
2020-10-05 01:46:37 → polyrain joins (~polyrain@2001:8003:e501:6901:5451:58df:dd7d:42b9)
2020-10-05 01:46:49 × xff0x quits (~fox@2001:1a81:52c9:f600:e0a1:2683:5939:2315) (Ping timeout: 272 seconds)
2020-10-05 01:47:01 <ski> quintasan : well .. you seem to be passing four parameters, where only two are expected (as the type error says)
2020-10-05 01:48:06 <quintasan> ski: Well... you are probably right but I've tried to do what the documentation tells you to do and I'm stuck :D
2020-10-05 01:48:17 → xff0x joins (~fox@2001:1a81:5300:fe00:7915:3d42:ba93:76ea)
2020-10-05 01:48:23 → nbloomf joins (~nbloomf@2600:1700:83e0:1f40:68ef:3717:d255:fea6)
2020-10-05 01:49:02 <ski> quintasan : where's `insertTeaStatement' ?
2020-10-05 01:49:32 <quintasan> ski: src/Statements.hs
2020-10-05 01:51:13 <ski> what is `name' ?
2020-10-05 01:52:04 <quintasan> name to insert in the database, it's supposed to be plain Text
2020-10-05 01:52:25 <ski> what's the type of it ?
2020-10-05 01:52:29 <ski> mhm
2020-10-05 01:53:23 <ski> insertTea name = transaction Write Serializable (statement Statements.insertTeaStatement name)
2020-10-05 01:53:52 <ski> is probably still not right, i suspect. but perhaps closer
2020-10-05 01:54:01 <quintasan> I'm suspecting the tutorial is wrong because https://github.com/nikita-volkov/hasql-tutorial1/blob/master/library/HasqlTutorial1/Transaction.hs has `import Hasql.Transaction` and then calls `statement` and https://hackage.haskell.org/package/hasql-transaction-1.0.0.1/docs/Hasql-Transaction.html says `statement` takes a -> Statement a b -> Transaction b
2020-10-05 01:54:15 <ski> oh, sorry, wrong order
2020-10-05 01:54:20 <ski> insertTea name = transaction Serializable Write (statement Statements.insertTeaStatement name)
2020-10-05 01:54:50 <ski> yea, that says `statement' only takes two parameters, now four
2020-10-05 01:56:01 <quintasan> https://hackage.haskell.org/package/hasql-transaction-1.0.0.1/docs/Hasql-Transaction-Sessions.html has `transaction` which accepts IsolationLevel -> Mode -> Transaction a -> Session a
2020-10-05 01:56:04 <quintasan> I'm confused
2020-10-05 01:56:58 <Squarism> infinisil, thanks about that existential type trick from yesterday. It was what I needed.
2020-10-05 01:57:04 <ski> and `Serializable' (an `IsolationLevel'), and `Write' (a `Mode'), seems like you wanted to feed them to `transaction' (which will also take a `Transaction b' (which is what `statement' will produce, if you feed it an `a', and a `Statement a b', which seems to fit what `insertTeaStatement' is ..), producing a `Session b')
2020-10-05 01:57:47 × darjeeling_ quits (~darjeelin@122.245.210.179) (Ping timeout: 240 seconds)
2020-10-05 01:58:05 <ski> quintasan : yes. but in your paste(s), you only called `statement', not `transaction'. but you tried to pass `Serializable' and `Write' to the former, not the latter ..
2020-10-05 01:58:21 ski idly wonders what Squarism did with existentials
2020-10-05 01:58:27 × polyrain quits (~polyrain@2001:8003:e501:6901:5451:58df:dd7d:42b9) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-10-05 01:58:40 → jedws joins (~jedws@121.209.186.103)
2020-10-05 01:58:58 <Squarism> ski, cheating the type system. What else is there? =D
2020-10-05 01:59:25 <quintasan> ski: I'm holding on to provided tutorials for my dear life but at this point it looks to be flat-out wrong - https://github.com/nikita-volkov/hasql-tutorial1/blob/master/library/HasqlTutorial1/Transaction.hs#L42
2020-10-05 01:59:38 → justsomeguy joins (~justsomeg@unaffiliated/--/x-3805311)
2020-10-05 01:59:44 <Squarism> I guess I could have done wo but it sorta works so I guess I'll settle for that
2020-10-05 02:02:02 <ski> Squarism : well, i'm guessing (and guessed before), that the interface has changed, that possibly those two parameters (the `IsolationLevel' and the `Mode') previously was to be passed to `statement', but not longer goes there
2020-10-05 02:03:29 <ski> er, sorry
2020-10-05 02:03:37 <ski> quintasan : that ^ was meant for you
2020-10-05 02:04:01 <ski> Squarism : .. still wondering what you used them for :)
2020-10-05 02:08:03 → elliott__ joins (~elliott@pool-108-51-141-12.washdc.fios.verizon.net)
2020-10-05 02:08:53 <Squarism> ski, So I had a function. Say foo :: Bar a . Bar had a function that produced values who's type was independent of "a". So I got a bit dissapointed when I realized I had to know "a
2020-10-05 02:08:56 <Squarism> "
2020-10-05 02:09:08 <Squarism> upon invocation.
2020-10-05 02:10:07 × ddellacosta quits (~dd@86.106.121.168) (Ping timeout: 246 seconds)
2020-10-05 02:10:11 <ski> `Bar a' being a `data' type, which included a function inside ?
2020-10-05 02:10:11 <Squarism> So I did foo :: GenBar. and data GenBar = forall a. Bar => GenBar { val :: a }
2020-10-05 02:10:51 <ski> (if `foo :: Bar a', and `Bar a' is not a type synonym for a function type, then `foo' is not a function, btw)
2020-10-05 02:11:03 <ski> hm
2020-10-05 02:11:06 <Squarism> oh sorry. foo :: Bar a => a
2020-10-05 02:11:13 <Squarism> Bar was a class
2020-10-05 02:11:17 <ski> oh
2020-10-05 02:11:22 <ski> and what's the methods of `Bar' ?
2020-10-05 02:12:14 <Squarism> well it was gimmeString :: a -> String
2020-10-05 02:12:26 <Squarism> sure, a is an argument there.
2020-10-05 02:12:28 <ski> only that ?
2020-10-05 02:12:40 <Squarism> I mean, I make it simpler for ease of discussion.
2020-10-05 02:13:17 <ski> your `GenBar' expresses/encodes `exists a. Bar a *> a' (i presume you meant `Bar a', not just `Bar' in the definition of `GenBar' ..)
←Prev  Next→
Page 1 .. 416 417 418 419 420 421 422 423 424 425 426 .. 5022

All times are in UTC.