Newest at the top
| 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 |
| 2024-09-21 12:03:18 +0200 | <ski> | the tag also needs to be distinct from the type of the contents |
| 2024-09-21 12:01:56 +0200 | <tomsmeding> | (never mind that there are umpteen other problems with std::variant, it's a mess, but it _is_ a sum type) |
| 2024-09-21 12:01:41 +0200 | <tomsmeding> | e.g. std::variant in C++ builds on the underlying support for union types to create a sum type, because its API doesn't allow letting the tag and the contents get out of sync |
| 2024-09-21 12:01:15 +0200 | <tomsmeding> | well -- the language, or the API of the sum type, if it's implemented in user space |
| 2024-09-21 12:00:29 +0200 | wagle | (~wagle@quassel.wagle.io) (Quit: http://quassel-irc.org - Chat comfortably. Anywhere.) |
| 2024-09-21 12:00:09 +0200 | <tomsmeding> | I'd call a tagged union a "sum type" when the language ensures that the tag and the union contents remain in sync |
| 2024-09-21 11:59:49 +0200 | <tomsmeding> | right |
| 2024-09-21 11:59:39 +0200 | <Inst> | tagged unions, i guess |
| 2024-09-21 11:57:28 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-21 11:57:09 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 248 seconds) |
| 2024-09-21 11:56:21 +0200 | nnm | (~nnm@79-139-162-83.dynamic.spd-mgts.ru) |
| 2024-09-21 11:52:57 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) |
| 2024-09-21 11:52:36 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-21 11:51:06 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-09-21 11:45:09 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
| 2024-09-21 11:44:45 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) |
| 2024-09-21 11:44:19 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2024-09-21 11:43:27 +0200 | <tomsmeding> | as does typescript |