Newest at the top
| 2025-12-04 14:16:08 +0100 | <ski> | which is confusing and not that useful |
| 2025-12-04 14:16:02 +0100 | <ski> | (a) means that, normally, if defining `Show' explicitly (rather than `deriving'), you'll normally define `showsPrec', to deal with precdedence and bracketing properly. do note that different `Show' instances are intended to work together (e.g. `instance Show a => Show (Maybe a)'), so that if you happen to use custom syntax for `T', you'll then get a mix of custom and Haskell syntax for (e.g.) `Maybe T', |
| 2025-12-04 14:14:52 +0100 | <lucabtz> | ski yeah i realized last night when i was trying to understand Read and i saw it is so much related to haskell lexicon itself |
| 2025-12-04 14:14:09 +0100 | <lucabtz> | if it was something like data BoundedNatural = { val :: Natural, bound :: Natural } then zero would not make sense because how do you pick a bound |
| 2025-12-04 14:13:47 +0100 | <tomsmeding> | (agreed with ski) |
| 2025-12-04 14:13:34 +0100 | <ski> | lucabtz : imho, (a) `Show' ought to use Haskell syntax (rather than some custom syntax format), so that its `String' output (in an appropriate environment) will evaluate to an equal value; and (b) if you also have `Read', then it ought to be able to read (finite) output generated from `Show', producing an equal value |
| 2025-12-04 14:13:22 +0100 | <lucabtz> | and i need the bound as part of the type |
| 2025-12-04 14:13:12 +0100 | fp | (~Thunderbi@2001:708:20:1406::1370) fp |
| 2025-12-04 14:13:05 +0100 | <lucabtz> | i think the check has to be kept at runtime, because i need to determine the type at runtime, however i want the type to extend another typeclass which i called PartialAdditive which supports an operator +? which may fail and a zero |
| 2025-12-04 14:12:50 +0100 | fp | (~Thunderbi@130.233.70.22) (Quit: fp) |
| 2025-12-04 14:12:22 +0100 | trickard_ | (~trickard@cpe-85-98-47-163.wireline.com.au) |
| 2025-12-04 14:12:08 +0100 | trickard_ | (~trickard@cpe-85-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-12-04 14:10:55 +0100 | <tomsmeding> | https://hackage.haskell.org/package/base-4.19.0.0/docs/GHC-TypeNats.html#t:-60--61- |
| 2025-12-04 14:10:23 +0100 | <tomsmeding> | lucabtz: while that is possible, bounds on the type level like that tend to make for very cumbersome interfaces |
| 2025-12-04 14:10:17 +0100 | <lucabtz> | i just needed a way to print the stuff to the terminal |
| 2025-12-04 14:10:05 +0100 | <lucabtz> | yeah i havent studied in detail Read/Show i find them confusing |
| 2025-12-04 14:09:29 +0100 | <ski> | (`showsPrec p (PromiseBoundedNatural n) = showParen (p > 10) $ showString "PromiseBoundedNatural " . showsPrec 11 n' is how i'd do `Show', if no `fromInteger' for `BoundedNatural bound') |
| 2025-12-04 14:09:27 +0100 | <lucabtz> | i think mkBoundedNatural should have a different signature taking the bound into account too. it should be done with SNat |
| 2025-12-04 14:09:20 +0100 | Square2 | (~Square4@user/square) Square |
| 2025-12-04 14:07:50 +0100 | <lucabtz> | i will look better into it later |
| 2025-12-04 14:07:27 +0100 | <ski> | mm, yea, that would be possible |
| 2025-12-04 14:06:48 +0100 | <ski> | (also i'd implement `fromInteger', or else i'd say that `Show' instance is incorrect) |
| 2025-12-04 14:06:45 +0100 | <tomsmeding> | oh what might be even nicer is to keep UnsafeMkBoundedNatural, but provide a pattern synonym (Mk)BoundedNatural that does a dynamic check on construction |
| 2025-12-04 14:06:16 +0100 | Typosit | (b41a81e702@2001:bc8:1210:2cd8::494) (Write error: error:80000068:system library::Connection reset by peer) |
| 2025-12-04 14:05:24 +0100 | <ski> | lucabtz : fwiw, i'd s/UnsafeMkBoundedNatural/PromiseBoundedNatural/, indicating that by using the constructor, you promise that the argument/component is bounded, and that by pattern-matching, you are being promised that the component is bounded |
| 2025-12-04 14:04:12 +0100 | Typosit | (b41a81e702@2001:bc8:1210:2cd8::494) |
| 2025-12-04 14:03:08 +0100 | PaulMartensen | (15a119e437@2001:bc8:1210:2cd8::3bc) (Ping timeout: 256 seconds) |
| 2025-12-04 14:03:03 +0100 | annamalai | (~annamalai@157.32.218.49) annamalai |
| 2025-12-04 13:59:45 +0100 | X-Scale | (~ARM@50.65.114.89.rev.vodafone.pt) X-Scale |
| 2025-12-04 13:59:07 +0100 | Ging_ | (46fea76d80@2001:bc8:1210:2cd8::470) (Ping timeout: 265 seconds) |
| 2025-12-04 13:59:07 +0100 | Typosit | (b41a81e702@2001:bc8:1210:2cd8::494) (Ping timeout: 265 seconds) |
| 2025-12-04 13:58:59 +0100 | <tomsmeding> | lucabtz: what do you mean with that? |
| 2025-12-04 13:56:38 +0100 | srazkvt | (~sarah@user/srazkvt) (Quit: Konversation terminated!) |
| 2025-12-04 13:56:09 +0100 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 250 seconds) |
| 2025-12-04 13:55:20 +0100 | PaulMartensen | (15a119e437@2001:bc8:1210:2cd8::3bc) |
| 2025-12-04 13:54:05 +0100 | Typosit | (b41a81e702@2001:bc8:1210:2cd8::494) |
| 2025-12-04 13:53:20 +0100 | Ging_ | (46fea76d80@2001:bc8:1210:2cd8::470) |
| 2025-12-04 13:47:50 +0100 | divya | (divya@140.238.251.170) divya |
| 2025-12-04 13:46:18 +0100 | lambda_gibbon | (~lambda_gi@2603:7080:ee00:37d8:313d:1898:c3f8:5287) |
| 2025-12-04 13:41:11 +0100 | img | (~img@user/img) img |
| 2025-12-04 13:41:09 +0100 | xff0x | (~xff0x@2405:6580:b080:900:d454:e7ea:27f9:454f) |
| 2025-12-04 13:39:56 +0100 | img | (~img@user/img) (Quit: ZNC 1.10.1 - https://znc.in) |
| 2025-12-04 13:39:35 +0100 | <lucabtz> | im confused on how to go from value level to type level though, if it even is possible |
| 2025-12-04 13:38:21 +0100 | <lucabtz> | yeah i might change to that |
| 2025-12-04 13:36:35 +0100 | ljdarj1 | ljdarj |
| 2025-12-04 13:36:35 +0100 | Ging_ | (46fea76d80@2001:bc8:1210:2cd8::470) (Ping timeout: 245 seconds) |
| 2025-12-04 13:36:35 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 240 seconds) |
| 2025-12-04 13:36:32 +0100 | hdggxin | (~hdggxin@2401:4900:88a9:bff0:be1a:791c:4871:3d3b) (Remote host closed the connection) |
| 2025-12-04 13:35:02 +0100 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-12-04 13:35:01 +0100 | PaulMartensen | (2c15493d69@2001:bc8:1210:2cd8::3bc) (Ping timeout: 255 seconds) |