Logs: freenode/#haskell
| 2021-02-28 21:45:30 | <edwardk> | rednaZ[m]: generally whenever i see a Typeable constraint i try to move to atze van der ploeg's keys or find some other way to recover type information, just a rule of thumb, because Typeable is quite the blunt instrument and gets in the way when i want region parameters for things like ST s, etc. |
| 2021-02-28 21:46:10 | <edwardk> | rednaZ[m]: not saying that this is doable in your circumstance, just giving you my mental model |
| 2021-02-28 21:46:31 | <hololeap> | it almost sounds like you would need dependent types to do this at the type level, but, again, i'm not really understanding what you're trying to do |
| 2021-02-28 21:46:39 | <dolio> | Create a type that represents the set of triples, with the operations you want. Implement it however, and use it in the dependent code. |
| 2021-02-28 21:47:58 | <ij> | Can a type become concrete by adding more typeclass constraints? |
| 2021-02-28 21:48:18 | <edwardk> | ij: is one of them x ~ MyConcreteType ? |
| 2021-02-28 21:49:40 | <hololeap> | edwardk: that doesn't really make it concrete though, does it? it will just fail on anything except one specific type. |
| 2021-02-28 21:50:01 | <ij> | No, it doesn't look like it. hip's "e" pixel channel type is first constrained by Elevator e, which doesn't compile when given to writeImage, but then, if I add (Elevator e, Fractional e) by "image / 400" (or similar), then it compiles |
| 2021-02-28 21:50:20 | <ij> | well, maybe I ought to check what the involved typeclass definitions look like |
| 2021-02-28 21:50:31 | <ij> | maybe they have that "a ~ b" |
| 2021-02-28 21:50:54 | <hololeap> | (/) requires Fractional |
| 2021-02-28 21:50:59 | <hololeap> | :t (/) |
| 2021-02-28 21:51:00 | <lambdabot> | Fractional a => a -> a -> a |
| 2021-02-28 21:51:21 | <ij> | right, but why would it make it choose a concrete type? that I don't understand or how rather |
| 2021-02-28 21:51:25 | <edwardk> | hololeap: Bool isn't really concrete, it just fails if the type is anything except Bool ;) |
| 2021-02-28 21:52:04 | <edwardk> | ij: guessing what you have is defaulting kicking in when Fractional is applied |
| 2021-02-28 21:52:39 | <hololeap> | edwardk: while `foo :: x ~ Bool => x` is semantically the same as `x :: Bool`, i would think they are not the same at the compiler/technical level |
| 2021-02-28 21:53:01 | <edwardk> | hololeap: they are the same modulo a core coercion you can't see |
| 2021-02-28 21:53:41 | <edwardk> | every GADT you've ever used has compiled the latter into the former in the different constructor definitions |
| 2021-02-28 21:53:57 | <ij> | https://kseo.github.io/posts/2017-01-04-type-defaulting-in-haskell.html |
| 2021-02-28 21:53:58 | <hololeap> | ok, fair enough. so will `main :: x ~ IO () => x` compile? |
| 2021-02-28 21:54:05 | <ij> | Fractional defaults to Double indeed |
| 2021-02-28 21:54:26 | → | vchlup_ joins (~vchlup@nat.brnet.cz) |
| 2021-02-28 21:54:30 | <edwardk> | data Foo a where Foo :: Foo Int; makes Foo :: forall a. (a ~ Int) => Foo a |
| 2021-02-28 21:54:31 | <hololeap> | (with a definition for main, obviously) |
| 2021-02-28 21:55:05 | → | kderme48 joins (4fa758c1@ppp079167088193.access.hol.gr) |
| 2021-02-28 21:55:09 | <edwardk> | hololeap: yes |
| 2021-02-28 21:55:31 | <hololeap> | good to know :) |
| 2021-02-28 21:55:32 | <edwardk> | {-# Language TypeFamilies #-}; main :: x ~ IO () => x; main = print "hello" runhaskell main.hs ===> "hello" |
| 2021-02-28 21:57:03 | × | kderme quits (4fa758c1@ppp079167088193.access.hol.gr) (Ping timeout: 240 seconds) |
| 2021-02-28 21:57:25 | → | dansho joins (~dansho@ec2-52-69-229-22.ap-northeast-1.compute.amazonaws.com) |
| 2021-02-28 21:57:30 | → | nullniverse joins (~null@unaffiliated/nullniverse) |
| 2021-02-28 21:57:31 | × | nullniverse quits (~null@unaffiliated/nullniverse) (Max SendQ exceeded) |
| 2021-02-28 21:57:33 | <rednaZ[m]> | edwardk: The fundamental problem when trying to get a OpenSum type is that Haskell does not have type-level sets. This makes me think of row polymorphism. What happened to ermine? |
| 2021-02-28 21:57:57 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Quit: Lost terminal) |
| 2021-02-28 21:58:52 | <edwardk> | rednaZ[m]: i got cancer and eventually left the company right as corporate will to carry it to completion flagged. |
| 2021-02-28 21:59:49 | <edwardk> | then i got better and landed at digital asset for a while and worked on daml instead |
| 2021-02-28 21:59:56 | <dansho> | does this look like an unreasonable amount of allocations? if im reading right its about 1G/s http://codepad.org/7MbUjQ21 |
| 2021-02-28 21:59:57 | <rednaZ[m]> | edwardk: Sorry to heart that. I hope you are o.k. |
| 2021-02-28 22:00:26 | <edwardk> | rednaZ[m]: afaict its all good now. I take a pill or two a day, but everything seems fine |
| 2021-02-28 22:00:28 | → | Rudd0 joins (~Rudd0@185.189.115.108) |
| 2021-02-28 22:00:50 | <rednaZ[m]> | edwardk: In PureScript row's can contain the same label multiple times. Was this different in ermine? |
| 2021-02-28 22:00:56 | <edwardk> | yes |
| 2021-02-28 22:01:00 | <rednaZ[m]> | nice |
| 2021-02-28 22:01:09 | <dolio> | It really isn't nice. |
| 2021-02-28 22:01:11 | <rednaZ[m]> | That is how I understood it from that one youtube video. |
| 2021-02-28 22:01:23 | <edwardk> | ermine rowtypes used 'can be partitioned into' constraints. which are apparently their own brand of crazy. |
| 2021-02-28 22:01:36 | <tomsmeding> | BigLama: "connection" in "connection sharing" refers to the TCP connection, as in a TCP socket (or perhaps TLS connection if you're using https). If you give the header 'Connection: keep-alive' in a HTTP request, you can send another request on the same connection. This is advantageous since you don't have to setup the connection multiple times, which is fairly expensive when using TLS (https). |
| 2021-02-28 22:01:36 | <tomsmeding> | It's not so expensive when using plain http, but still removes some overhead. |
| 2021-02-28 22:01:45 | <rednaZ[m]> | edwardk: Seems like the way to avoid label duplication. |
| 2021-02-28 22:01:48 | <edwardk> | Elem e es becomes 'exists x. such that es can be parititoned into e and x. |
| 2021-02-28 22:02:10 | <edwardk> | similarly Lacks e es becomes exists y. such that y can be partitioned into e and es |
| 2021-02-28 22:02:11 | <tomsmeding> | BigLama: this is purely a performance thing; this has nothing to do with logins or anything on that level. |
| 2021-02-28 22:02:23 | <edwardk> | that part i liked. the practical aspects of typechecking it? not so much |
| 2021-02-28 22:03:02 | <rednaZ[m]> | edwardk: I think of rows as type-level maps from type-level strings to types. |
| 2021-02-28 22:03:21 | <edwardk> | xplat had a nice scheme involving describing such row types in terms of complete atomic boolean algebras, but we never got around to switching from the ad hoc pile of rules we made up to that. |
| 2021-02-28 22:03:54 | <rednaZ[m]> | edwardk: Have you ever thought about general type-level maps from types to types? |
| 2021-02-28 22:04:13 | × | cyphase quits (~cyphase@unaffiliated/cyphase) (Read error: Connection reset by peer) |
| 2021-02-28 22:04:16 | <rednaZ[m]> | Than I could encode type-level sets as maps with index type unit. |
| 2021-02-28 22:04:17 | <edwardk> | rednaZ[m]: have you look at ur/web? |
| 2021-02-28 22:04:30 | <rednaZ[m]> | What is that? |
| 2021-02-28 22:04:32 | <edwardk> | rednaZ[m]: you're basically reinventiong adam chlipala's baby |
| 2021-02-28 22:04:36 | <edwardk> | er reinventing |
| 2021-02-28 22:05:12 | × | kenran quits (~kenran@i59F67BBA.versanet.de) (Quit: leaving) |
| 2021-02-28 22:05:49 | × | Varis quits (~Tadas@unaffiliated/varis) (Remote host closed the connection) |
| 2021-02-28 22:06:23 | <rednaZ[m]> | Thanks for the pointer at adam chlipala. What is ur/web? |
| 2021-02-28 22:06:37 | × | SchwarzeLocke quits (~SchwarzeL@178.239.168.171) (Remote host closed the connection) |
| 2021-02-28 22:06:50 | <rednaZ[m]> | Ah, found it. http://www.impredicative.com/ur/ |
| 2021-02-28 22:07:41 | <dolio> | I kind of think that, in real retrospect, the rows in ermine were a fundemantally wrong choice for the use case. |
| 2021-02-28 22:07:54 | <edwardk> | i agree |
| 2021-02-28 22:08:05 | <edwardk> | lots of heavy lifting put to poor use |
| 2021-02-28 22:08:07 | dcoutts_ | is now known as dcoutts |
| 2021-02-28 22:08:11 | <dolio> | The databases don't actually do natural joins automatically. |
| 2021-02-28 22:08:47 | <dolio> | So the real underlying rows automatically introduce duplicate fields that are only eliminated by further operations. |
| 2021-02-28 22:08:48 | <rednaZ[m]> | Do you think allowing label duplication is the better choice? |
| 2021-02-28 22:09:03 | <dolio> | In some situations, yes. |
| 2021-02-28 22:09:29 | <rednaZ[m]> | In a general-purpose language? |
| 2021-02-28 22:09:49 | <edwardk> | the joinOn (or joinWith, i forget the names) were the real workhorse of the language. |
| 2021-02-28 22:10:03 | <edwardk> | and that didn't lean on 'natural' joins at all |
| 2021-02-28 22:10:33 | <dolio> | That doesn't have an answer. You don't need rows for "general purpose". You need them for various features of a general purpose language, and which feature they're for might make duplicates or non-duplicates better. |
| 2021-02-28 22:10:55 | <dolio> | I would say people under-estimate duplicates, though. |
| 2021-02-28 22:10:57 | <edwardk> | in retrospect a more natural fit to sql would probably have been to have fully qualified Table.FieldName names or something, and then allow FieldName access to those when they were unambiguous, or something awful like that. |
| 2021-02-28 22:10:58 | <rednaZ[m]> | I feel like I need checked exceptions pretty badly. |
| 2021-02-28 22:11:01 | → | cyphase joins (~cyphase@unaffiliated/cyphase) |
| 2021-02-28 22:11:15 | <slack1256> | Does anyone know if "space invariants" were developed onto a full theory? link: https://apfelmus.nfshost.com/blog/2013/08/21-space-invariants.html |
| 2021-02-28 22:11:21 | <edwardk> | rednaZ[m]: when i throw an exception at you, what do you do then? |
| 2021-02-28 22:11:40 | <dolio> | Okay, well, checked exceptions are actually an example where duplicates are good. |
| 2021-02-28 22:11:46 | <edwardk> | i used to be more bullish on checked exceptions |
| 2021-02-28 22:11:58 | <BigLama> | tomsmeding: thanks a lot :) |
| 2021-02-28 22:12:20 | <rednaZ[m]> | edwardk: I handle it if I can. I `error` if I know it cannot happen effectively turning the exception into an unchecked one. |
| 2021-02-28 22:12:35 | <dolio> | Because there's a problem with checked exceptions and polymorphism/abstraction. |
| 2021-02-28 22:12:37 | <edwardk> | but given i can basically throw anything at any thread i've since become a bit more prosaic about the fact that checked exceptions just means the more exotic code path never gets tested and that exotic code path is super important in most concurrent programming situations |
| 2021-02-28 22:13:11 | <rednaZ[m]> | I would already be happy about checked exceptions in pure code. |
| 2021-02-28 22:13:29 | <rednaZ[m]> | instead of using `Either SomeException` or similar |
| 2021-02-28 22:14:25 | <edwardk> | same issue arises there. you wind up with an Either case for things you are manually putting in expensive boxes and then taking out and putting back in expensive boxes all the time, and 'real exceptions' which blow up your leaky abstraction and are sadly cheaper. |
| 2021-02-28 22:14:41 | <dolio> | If you have `f : (a -> b throws e) -> ...` where `f g = try ... g x ... catch { Exn1 -> ... }`, then the naive way for that to work violates the abstraction of `e`, because if `e` happens to contain `Exn1`, your handler will actually catch it. |
| 2021-02-28 22:14:51 | <edwardk> | it _galls_ me that ReaderT (IORef s) IO -- is generally cheaper/faster than StateT s IO |
| 2021-02-28 22:14:59 | × | tsrt^ quits (tsrt@ip98-184-89-2.mc.at.cox.net) () |
| 2021-02-28 22:15:01 | <edwardk> | same diff for EitherT variants |
| 2021-02-28 22:16:03 | <rednaZ[m]> | I do not care that much about performance. |
All times are in UTC.