Newest at the top
2024-09-21 13:26:06 +0200 | synchromesh | (~john@2406:5a00:241a:5600:3c25:ae8:512d:c1ef) (Read error: Connection reset by peer) |
2024-09-21 13:23:03 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-21 13:20:57 +0200 | Guest4 | (~Guest4@cpc122096-bmly10-2-0-cust498.2-3.cable.virginm.net) (Ping timeout: 256 seconds) |
2024-09-21 13:19:59 +0200 | paddymahoney | (~paddymaho@pool-99-250-10-137.cpe.net.cable.rogers.com) (Ping timeout: 245 seconds) |
2024-09-21 13:16:29 +0200 | Guest4 | (~Guest4@cpc122096-bmly10-2-0-cust498.2-3.cable.virginm.net) |
2024-09-21 13:14:15 +0200 | Squared | (~Square@user/square) |
2024-09-21 13:13:35 +0200 | Guest4 | (~Guest4@cpc122096-bmly10-2-0-cust498.2-3.cable.virginm.net) (Ping timeout: 256 seconds) |
2024-09-21 13:10:38 +0200 | mreh | (~matthew@host86-146-25-125.range86-146.btcentralplus.com) |
2024-09-21 13:09:38 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2024-09-21 13:05:08 +0200 | caconym | (~caconym@user/caconym) |
2024-09-21 13:01:58 +0200 | YoungFrog | (~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be) |
2024-09-21 13:01:38 +0200 | YoungFrog | (~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be) (Quit: ZNC 1.7.x-git-3-96481995 - https://znc.in) |
2024-09-21 13:00:04 +0200 | caconym | (~caconym@user/caconym) (Quit: bye) |
2024-09-21 12:58:29 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
2024-09-21 12:55:18 +0200 | Guest4 | (~Guest4@cpc122096-bmly10-2-0-cust498.2-3.cable.virginm.net) |
2024-09-21 12:53:37 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-21 12:43:17 +0200 | gvg_ | gvg |
2024-09-21 12:42:34 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
2024-09-21 12:38:53 +0200 | Guest4 | (~Guest4@cpc122096-bmly10-2-0-cust498.2-3.cable.virginm.net) (Quit: Client closed) |
2024-09-21 12:37:49 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-21 12:35:39 +0200 | driib318 | (~driib@176.57.184.141) |
2024-09-21 12:34:33 +0200 | driib318 | (~driib@vmi931078.contaboserver.net) (Quit: The Lounge - https://thelounge.chat) |
2024-09-21 12:26:57 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
2024-09-21 12:24:09 +0200 | dolio | (~dolio@130.44.140.168) |
2024-09-21 12:23:21 +0200 | connrs | (~connrs@user/connrs) |
2024-09-21 12:22:55 +0200 | mreh | (~matthew@host86-146-25-125.range86-146.btcentralplus.com) (Ping timeout: 264 seconds) |
2024-09-21 12:22:54 +0200 | dolio | (~dolio@130.44.140.168) (Ping timeout: 260 seconds) |
2024-09-21 12:22:03 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-21 12:21:38 +0200 | connrs | (~connrs@user/connrs) (Ping timeout: 265 seconds) |
2024-09-21 12:17:18 +0200 | Guest4 | (~Guest4@cpc122096-bmly10-2-0-cust498.2-3.cable.virginm.net) |
2024-09-21 12:16:30 +0200 | CiaoSen | (~Jura@2a05:5800:22d:f000:ca4b:d6ff:fec1:99da) (Ping timeout: 246 seconds) |
2024-09-21 12:15:33 +0200 | spenat_ | spenat |
2024-09-21 12:11:24 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
2024-09-21 12:10:15 +0200 | <ski> | "Supertyping Suggestion for Haskell" by jmeacham (of jhc) at <http://repetae.net/recent/out/supertyping.html> is something similar, but for type classes |
2024-09-21 12:08:36 +0200 | <ski> | (you can also refine a record/product type, by removing fields, yielding a supertype) |
2024-09-21 12:08:36 +0200 | <tomsmeding> | Lears: there are type systems that support them /shrug/ |
2024-09-21 12:08:15 +0200 | <tomsmeding> | difference in terminology, then |
2024-09-21 12:08:11 +0200 | <Lears> | "Union types" need to be debunked so people will stop expecting them to be a thing. They don't even make sense. |
2024-09-21 12:08:11 +0200 | <tomsmeding> | I see |
2024-09-21 12:07:51 +0200 | <ski> | this was described in papers before LiquidHaskell existed |
2024-09-21 12:07:25 +0200 | <ski> | you refine a variant/sum type, by removing alternatives, yielding a subtype |
2024-09-21 12:07:08 +0200 | <ski> | given `data List a = Nil | Cons a (List a)', i'd say `data EvenList a <: List a = Nil | Cons a (OddList a)' and `data OddList a <: List a = Cons a (EvenList a)' are refinement types |
2024-09-21 12:06:32 +0200 | <tomsmeding> | at the very least, liquid haskell has these things and calls them "refinement types" :) |
2024-09-21 12:06:15 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
2024-09-21 12:06:08 +0200 | <tomsmeding> | isn't "refinement type" a more general term? |
2024-09-21 12:05:39 +0200 | ski | would call those (subset) comprenesion types |
2024-09-21 12:04:50 +0200 | <ski> | yep, that's a more constructive way to phrase it |
2024-09-21 12:04:48 +0200 | <tomsmeding> | looking at the types becomes ambiguous if you have e.g. a language with refinement types, where Int and {v : Int | v > 0} are distinct types but have indistinguishable values |
2024-09-21 12:04:00 +0200 | <tomsmeding> | I would rather formulate that as "every alternative of the union should have a distinct tag" |
2024-09-21 12:03:32 +0200 | <ski> | (`A + A' should not equal `A'9 |