Logs on 2024-02-20 (liberachat/#haskell)
| 00:01:05 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 256 seconds) |
| 00:04:47 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 00:11:42 | → | rvalue joins (~rvalue@user/rvalue) |
| 00:24:51 | × | sroso quits (~sroso@user/SrOso) (Read error: Connection reset by peer) |
| 00:27:21 | <dmj`> | c_wraith: ping |
| 00:27:34 | <c_wraith> | hey, I'm around |
| 00:29:23 | → | sroso joins (~sroso@user/SrOso) |
| 00:29:58 | × | sroso quits (~sroso@user/SrOso) (Max SendQ exceeded) |
| 00:34:55 | → | werneta joins (~werneta@024-205-076-158.res.spectrum.com) |
| 00:36:34 | → | sroso joins (~sroso@user/SrOso) |
| 00:37:09 | × | sroso quits (~sroso@user/SrOso) (Max SendQ exceeded) |
| 00:38:01 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 00:42:49 | → | sroso joins (~sroso@user/SrOso) |
| 00:46:15 | × | dodoyada quits (~dodoyada@pool-71-178-11-160.washdc.fios.verizon.net) (Quit: Client closed) |
| 00:56:17 | → | puke joins (~puke@user/puke) |
| 00:59:52 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Quit: ZNC 1.8.2 - https://znc.in) |
| 01:01:48 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 01:03:49 | × | werneta quits (~werneta@024-205-076-158.res.spectrum.com) (Quit: Lost terminal) |
| 01:05:55 | × | whatsupdoc quits (uid509081@id-509081.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 01:07:37 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Remote host closed the connection) |
| 01:17:49 | → | dodoyada joins (~dodoyada@pool-71-178-11-160.washdc.fios.verizon.net) |
| 01:24:25 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 01:32:30 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 01:37:17 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 268 seconds) |
| 01:40:11 | <dmj`> | c_wraith: still thinking about recovering polymorphic recursion amidst whole program monomorphization (specializing and inlining). Thinking maybe defining a recursive AST (encoding the type cases) and a mini interpreter for it in cases where polymorphic recursion exists, could be a path forward. |
| 01:42:43 | <c_wraith> | that's close enough to what GHC does when it compiles code with polymorphic recursion. |
| 01:43:33 | <dmj`> | isn't this called "intensional type analysis" |
| 01:44:37 | <c_wraith> | I don't know the topic. a quick skim tells me it's at least related. |
| 01:45:18 | × | machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 268 seconds) |
| 01:48:13 | → | caesrmt^ joins (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 01:48:48 | <c_wraith> | but I've got a terminological nitpick. whole-program monomorphization says to me that it's finding a monomorphic type in the surface language for every expression. what you're suggesting still isn't capable of that, because it's logically inconsistent with polymorphic recursion. |
| 01:48:56 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 255 seconds) |
| 01:49:28 | <c_wraith> | what you're suggesting is a kind of rewriting of the surface language to an intermediate form where everything is monomorphic |
| 01:49:53 | <c_wraith> | which is great, but I think it needs a slightly different term. at least by my understanding |
| 01:49:55 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 268 seconds) |
| 01:50:45 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 01:51:37 | → | bilegeek joins (~bilegeek@2600:1008:b023:d9e2:9f22:5071:205d:e817) |
| 01:52:05 | × | xff0x quits (~xff0x@ai082039.d.east.v6connect.net) (Ping timeout: 268 seconds) |
| 02:01:16 | <carter> | I assume whole program monomorphization is always in the compiler ir |
| 02:01:32 | <dmj`> | Well, the surface language wouldn't be rewritten per se (I think). There would type checking, where when polymorphic recursion is encountered, a type signature would expected to exist in the typing env to allow things to infer and be decidable. But desugaring, instead of the dictionary passing, a whole program pass would analyze all call sites and provide monomorphic types for everything (all type variables get specialized). |
| 02:02:45 | <dmj`> | c_wraith: but what you're saying is correct because in order to encode the recursion we'd have to scrutinize the types and provide a mini interpreter on this type language. This seems to work well with the "pure type systems" approach where types and terms are identical. This is what JHC does. |
| 02:02:47 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 02:03:03 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.5) |
| 02:04:17 | <dmj`> | c_wraith: maybe this is the "intensional type analysis" part, in laymens terms |
| 02:07:46 | × | otto_s quits (~user@p5b044a25.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 02:08:10 | <dmj`> | layman's? |
| 02:09:28 | → | otto_s joins (~user@p4ff27fbc.dip0.t-ipconnect.de) |
| 02:15:48 | <geekosaur> | the latter |
| 02:20:15 | <dmj`> | thanks :) |
| 02:26:12 | × | jargon quits (~jargon@157.sub-174-205-162.myvzw.com) (Remote host closed the connection) |
| 02:31:10 | → | benkard joins (~mulk@p5b2dcb88.dip0.t-ipconnect.de) |
| 02:32:03 | × | mulk quits (~mulk@pd95148d1.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 02:32:03 | benkard | is now known as mulk |
| 02:32:22 | × | euphores quits (~SASL_euph@user/euphores) (Ping timeout: 260 seconds) |
| 02:41:15 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 02:51:21 | × | dodoyada quits (~dodoyada@pool-71-178-11-160.washdc.fios.verizon.net) (Quit: Client closed) |
| 02:53:08 | × | Xe quits (~cadey@perl/impostor/xe) (Ping timeout: 268 seconds) |
| 02:53:08 | → | notzmv joins (~daniel@user/notzmv) |
| 02:56:54 | → | sysadm1nH joins (~sysadm1nH@115.55.85.79.rev.sfr.net) |
| 02:56:56 | × | sysadm1nH quits (~sysadm1nH@115.55.85.79.rev.sfr.net) (Client Quit) |
| 02:59:59 | → | Xe joins (~cadey@perl/impostor/xe) |
| 03:00:33 | × | phma quits (phma@2001:5b0:211f:17e8:9781:bf89:87ee:5c) (Read error: Connection reset by peer) |
| 03:01:14 | → | phma joins (~phma@host-67-44-208-78.hnremote.net) |
| 03:01:46 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 268 seconds) |
| 03:02:15 | × | sroso quits (~sroso@user/SrOso) (Remote host closed the connection) |
| 03:02:36 | → | sroso joins (~sroso@user/SrOso) |
| 03:03:12 | × | sroso quits (~sroso@user/SrOso) (Max SendQ exceeded) |
| 03:03:20 | × | Xe quits (~cadey@perl/impostor/xe) (Excess Flood) |
| 03:03:29 | × | jbalint quits (~jbalint@071-090-119-177.res.spectrum.com) (Remote host closed the connection) |
| 03:03:37 | × | caesrmt^ quits (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 255 seconds) |
| 03:03:40 | → | jbalint joins (~jbalint@2600-6c44-117f-e98a-816a-9488-0fb1-07b7.inf6.spectrum.com) |
| 03:06:19 | → | Xe joins (~cadey@perl/impostor/xe) |
| 03:11:45 | → | sysadm1nH joins (~sysadm1nH@115.55.85.79.rev.sfr.net) |
| 03:12:05 | <sysadm1nH> | Good morning or good evening. You are welcome on https://twitter.com/PLocataire: #hacking #exploits #shellcodes #coding #OSINT #Tools #Papers :> |
| 03:13:17 | × | sysadm1nH quits (~sysadm1nH@115.55.85.79.rev.sfr.net) (K-Lined) |
| 03:18:36 | <tinjamin> | idk how y'all do it haskell is so damn hard |
| 03:19:43 | <jackdk> | tinjamin: honestly, by learning to outsource my thinking to the typechecker |
| 03:22:47 | <jackdk> | tinjamin: and by taking things one step at a time |
| 03:23:14 | × | td_ quits (~td@i53870935.versanet.de) (Ping timeout: 252 seconds) |
| 03:23:26 | <tinjamin> | Yeah, i've taken a three weeks hiatus and just got started again today |
| 03:23:40 | <tinjamin> | learning about lists and types |
| 03:24:55 | → | td_ joins (~td@i5387090B.versanet.de) |
| 03:27:05 | × | average quits (uid473595@user/average) (Quit: Connection closed for inactivity) |
| 03:27:08 | <jackdk> | There's also a bunch of tricks that you pick out along the way, like when you're starting out writing patterns, you often write one pattern for each constructor of a data type |
| 03:28:34 | → | tri joins (~tri@2607:fb90:b1a5:6d6:4df9:1a60:ef06:5b8b) |
| 03:29:16 | <jackdk> | tinjamin: This site is fun to play with, to evaluate simple-ish expressions step-by-step and see what they're doing: https://pbv.github.io/haskelite/site/index.html . I have used step-by-step eval on a notebook to understand thorny code in the past, I find it a very helpful idea |
| 03:29:50 | <jackdk> | I'm about to head out, so I'm sorry I can't give much more than platitudes. But if you have specific questions I think there will be a few other people in the channel who are awake and can help |
| 03:47:46 | <zwro> | https://www.reddit.com/r/haskell/s/Qud77rzrPo |
| 03:51:11 | → | caesrmt^ joins (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 03:58:37 | → | Lycurgus joins (~georg@user/Lycurgus) |
| 04:00:22 | × | tri quits (~tri@2607:fb90:b1a5:6d6:4df9:1a60:ef06:5b8b) (Remote host closed the connection) |
| 04:02:47 | <tinjamin> | definitely, thanks jackdk! |
| 04:08:25 | <dmj`> | tinjamin: write Semigroup, Monoid, Functor, Applicative, Monad for [], State, (,), Reader, Writer, (->), Either, Maybe (where applicable) and then implement Data.List and Control.Monad by hand. Implementing all the instances is key. O/w when you see all the overloaded functions it will always be confusing, your brain can only inline them if you've implemented the instances already |
| 04:09:24 | <jackdk> | I second the advice to write instances by hand, to see how things work |
| 04:11:39 | <jackdk> | https://github.com/system-f/fp-course can help here |
| 04:18:14 | → | dodoyada joins (~dodoyada@pool-71-178-11-160.washdc.fios.verizon.net) |
| 04:22:31 | → | rosco joins (~rosco@175.136.156.77) |
| 04:28:17 | × | euleritian quits (~euleritia@dynamic-176-006-180-132.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 04:28:34 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 04:29:19 | × | dcoutts quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Remote host closed the connection) |
| 04:29:23 | × | Katarushisu1 quits (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) (Quit: Ping timeout (120 seconds)) |
| 04:29:36 | → | dcoutts joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 04:30:49 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 04:31:37 | × | Ranhir quits (~Ranhir@157.97.53.139) (Ping timeout: 264 seconds) |
| 04:32:49 | × | m1dnight quits (~christoph@78-22-2-15.access.telenet.be) (Ping timeout: 264 seconds) |
| 04:32:49 | × | APic quits (apic@apic.name) (Ping timeout: 264 seconds) |
| 04:35:33 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 260 seconds) |
| 04:37:39 | × | aforemny quits (~aforemny@2001:9e8:6cc8:100:42ef:f733:c482:5119) (Ping timeout: 255 seconds) |
| 04:37:53 | → | aforemny_ joins (~aforemny@2001:9e8:6cec:d900:9d72:673f:b1f3:dc04) |
| 04:49:27 | → | Katarushisu1 joins (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) |
| 04:49:49 | → | heartburn joins (~gass@81.4.123.134) |
| 04:49:51 | → | igemnace joins (~ian@user/igemnace) |
| 04:52:35 | → | Ranhir joins (~Ranhir@157.97.53.139) |
| 04:52:57 | × | Katarushisu1 quits (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) (Client Quit) |
| 04:59:36 | → | m1dnight joins (~christoph@78-22-2-15.access.telenet.be) |
| 05:00:51 | × | hueso quits (~root@user/hueso) (Ping timeout: 256 seconds) |
| 05:03:07 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 05:04:31 | × | caesrmt^ quits (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Remote host closed the connection) |
| 05:08:49 | → | Katarushisu1 joins (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) |
| 05:09:05 | → | Square3 joins (~Square4@user/square) |
| 05:09:16 | → | michalz joins (~michalz@185.246.207.221) |
| 05:11:37 | × | Square quits (~Square@user/square) (Ping timeout: 256 seconds) |
| 05:14:18 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 05:14:38 | → | [_] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 05:14:55 | → | APic joins (apic@apic.name) |
| 05:17:16 | × | thegeekinside quits (~thegeekin@189.217.83.221) (Read error: Connection reset by peer) |
| 05:17:55 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 246 seconds) |
| 05:18:12 | → | actioninja8 joins (~actioninj@user/actioninja) |
| 05:19:50 | × | actioninja quits (~actioninj@user/actioninja) (Ping timeout: 252 seconds) |
| 05:19:51 | actioninja8 | is now known as actioninja |
| 05:26:17 | × | michalz quits (~michalz@185.246.207.221) (Quit: ZNC 1.8.2 - https://znc.in) |
| 05:26:38 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Quit: Leaving) |
| 05:29:04 | → | michalz joins (~michalz@185.246.207.197) |
| 05:44:25 | × | bilegeek quits (~bilegeek@2600:1008:b023:d9e2:9f22:5071:205d:e817) (Quit: Leaving) |
| 05:47:27 | × | dodoyada quits (~dodoyada@pool-71-178-11-160.washdc.fios.verizon.net) (Quit: Client closed) |
| 05:54:59 | × | Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving) |
| 06:03:35 | × | mulk quits (~mulk@p5b2dcb88.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 06:03:59 | × | Vq quits (~vq@90-225-115-195-no122.tbcn.telia.com) (Ping timeout: 268 seconds) |
| 06:05:31 | × | [_] quits (~itchyjunk@user/itchyjunk/x-7353470) (Quit: Leaving) |
| 06:10:19 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Remote host closed the connection) |
| 06:22:07 | → | mulk joins (~mulk@pd95142c7.dip0.t-ipconnect.de) |
| 06:23:15 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 06:25:23 | → | acidjnk joins (~acidjnk@p200300d6e737e723f1d9672538a89ef2.dip0.t-ipconnect.de) |
| 06:27:07 | × | mulk quits (~mulk@pd95142c7.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 06:34:12 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht) |
| 06:41:41 | <tinjamin> | thanks guys! |
| 06:41:52 | <tinjamin> | i'll definitely take a look in the morning |
| 06:53:51 | → | coot joins (~coot@89-69-206-216.dynamic.chello.pl) |
| 06:54:36 | → | bilegeek joins (~bilegeek@2600:1008:b023:d9e2:9f22:5071:205d:e817) |
| 07:00:57 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 07:18:18 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 07:22:31 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 256 seconds) |
| 07:27:48 | → | mulk joins (~mulk@pd951406a.dip0.t-ipconnect.de) |
| 07:30:19 | → | tromp joins (~textual@92.110.219.57) |
| 07:34:57 | × | mulk quits (~mulk@pd951406a.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 07:35:24 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 07:36:00 | → | bitmapper joins (uid464869@id-464869.lymington.irccloud.com) |
| 07:37:36 | → | mulk joins (~mulk@pd9514a85.dip0.t-ipconnect.de) |
| 07:55:38 | × | tromp quits (~textual@92.110.219.57) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 08:00:09 | → | fendor joins (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) |
| 08:08:30 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 08:09:41 | → | tromp joins (~textual@92.110.219.57) |
| 08:14:03 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 272 seconds) |
| 08:15:08 | → | euleritian joins (~euleritia@dynamic-176-006-187-025.176.6.pool.telefonica.de) |
| 08:23:11 | → | kuribas joins (~user@2a02:1808:80:3ece:5b45:c128:11b7:97c5) |
| 08:35:35 | × | AlexZenon quits (~alzenon@178.34.161.13) (Ping timeout: 272 seconds) |
| 08:36:13 | × | dcoutts quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 272 seconds) |
| 08:38:25 | × | euleritian quits (~euleritia@dynamic-176-006-187-025.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 08:38:42 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 08:46:16 | × | sam113101 quits (~sam@modemcable146.137-200-24.mc.videotron.ca) (Quit: WeeChat 4.1.2) |
| 08:46:53 | → | sam113101 joins (~sam@modemcable146.137-200-24.mc.videotron.ca) |
| 08:47:00 | → | enoq joins (~enoq@2a05:1141:1e6:3b00:c958:a45e:c4e0:3650) |
| 08:47:10 | → | AlexZenon joins (~alzenon@178.34.161.13) |
| 08:48:33 | <enoq> | let's say you've got a list of numbers, e.g. [1, 2, 3, 4] and you want to build a new list that adds the number to all previous numbers, e.g. [1, 3, 6, 10], what's the function called? |
| 08:48:46 | <enoq> | started with a naive implementation that has factorial runtime which is kinda bad xD |
| 08:49:40 | <enoq> | (as in: summing up all numbers to the current index) |
| 08:50:13 | <enoq> | hm, wait, kinda looks like a classic reduce? |
| 08:50:14 | <dminuoso> | > scanl (+) 0 [1..] |
| 08:50:18 | <lambdabot> | [0,1,3,6,10,15,21,28,36,45,55,66,78,91,105,120,136,153,171,190,210,231,253,2... |
| 08:50:22 | → | CiaoSen joins (~Jura@2a05:5800:2c7:500:e6b9:7aff:fe80:3d03) |
| 08:51:01 | <dminuoso> | Or, if you dont want that first element |
| 08:51:07 | <dminuoso> | > scanl1 (+) [1..] |
| 08:51:08 | <lambdabot> | [1,3,6,10,15,21,28,36,45,55,66,78,91,105,120,136,153,171,190,210,231,253,276... |
| 08:51:18 | <tomsmeding> | enoq: "prefix sums", or "a scan" |
| 08:51:29 | <enoq> | thanks! |
| 08:52:08 | <dminuoso> | enoq: Your observation that it looks "like" a reduce is quite right though, the umbrella term here is recursion schemes |
| 08:52:32 | <enoq> | it reduces to a list, not a singular value |
| 08:52:50 | <tomsmeding> | a scan is essentially a fold that remembers all the intermediate values |
| 08:53:46 | <enoq> | I remember implementing that in CUDA in university, forgot the name :) |
| 08:54:12 | → | machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 08:55:03 | <dminuoso> | enoq: how is "list" different from "singular value"? |
| 08:55:14 | <dminuoso> | Is a "list" not a "singular value"? |
| 08:55:23 | <dminuoso> | Matter of perspective, I would say. |
| 08:55:30 | <enoq> | reduce goes from a List<T> to T |
| 08:55:45 | <dminuoso> | Not quite. |
| 08:55:48 | <dminuoso> | :t foldr |
| 08:55:49 | <lambdabot> | Foldable t => (a -> b -> b) -> b -> t a -> b |
| 08:55:51 | <enoq> | scan goes from List<T> to List<T> I think |
| 08:56:00 | <dminuoso> | enoq: ^- look at that type signature. |
| 08:56:13 | <dminuoso> | enoq: Note that eventually you can take a `t a` to `b` |
| 08:56:18 | <dminuoso> | Not `t a` to `a` |
| 08:56:19 | × | kuribas quits (~user@2a02:1808:80:3ece:5b45:c128:11b7:97c5) (Ping timeout: 246 seconds) |
| 08:56:34 | <dminuoso> | > foldr (:) [] [1..] |
| 08:56:35 | <lambdabot> | [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,... |
| 08:56:39 | <dminuoso> | See, folded into a list. |
| 08:56:42 | → | gmg joins (~user@user/gehmehgeh) |
| 08:57:00 | × | tzh quits (~tzh@c-71-193-181-0.hsd1.or.comcast.net) (Quit: zzz) |
| 08:57:14 | <tomsmeding> | the "state" of the fold can be different from the element |
| 08:57:18 | <enoq> | I think Haskell's abstraction is just a bit more generic |
| 08:57:18 | <dminuoso> | enoq: A better intuition of `fold f z` is not that it "reduces/folds", but that it replaces (:) with f and [] with z in the list structure. |
| 08:57:44 | <tomsmeding> | which is different from the thing you implemented in CUDA: there you want the state to be the same type as the array element, so that the combination function can be associative, so that you can implement the fold/scan in parallel |
| 09:03:56 | → | cfricke joins (~cfricke@user/cfricke) |
| 09:04:42 | → | kuribas joins (~user@2a02:1808:80:3ece:18b4:369:3465:6cb1) |
| 09:10:13 | × | kuribas quits (~user@2a02:1808:80:3ece:18b4:369:3465:6cb1) (Ping timeout: 268 seconds) |
| 09:10:43 | → | kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be) |
| 09:11:55 | <kuribas> | tomsmeding: doing it non-locally makes much more sense IMO, then I can |
| 09:12:04 | <kuribas> | tomsmeding: doing it non-locally makes much more sense IMO, then the side effects are clear. |
| 09:12:12 | <tomsmeding> | (wrong channel?) |
| 09:12:18 | <kuribas> | right :) |
| 09:12:32 | → | NSFAF__ joins (~NSFAF@105.232.14.71) |
| 09:13:57 | × | tromp quits (~textual@92.110.219.57) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 09:16:33 | × | sam113101 quits (~sam@modemcable146.137-200-24.mc.videotron.ca) (Quit: WeeChat 4.1.2) |
| 09:19:06 | → | danse-nr3 joins (~danse@151.43.214.115) |
| 09:19:53 | → | sam113101 joins (~sam@modemcable146.137-200-24.mc.videotron.ca) |
| 09:23:50 | × | danse-nr3 quits (~danse@151.43.214.115) (Ping timeout: 256 seconds) |
| 09:28:24 | × | raym quits (~ray@user/raym) (Quit: Upgrading to FreeBSD 14.0-RELEASE-p5) |
| 09:31:52 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 09:32:11 | × | NSFAF__ quits (~NSFAF@105.232.14.71) (Ping timeout: 260 seconds) |
| 09:35:00 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 09:38:53 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 260 seconds) |
| 09:40:31 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 09:43:26 | × | ft quits (~ft@p508db2e6.dip0.t-ipconnect.de) (Quit: leaving) |
| 09:47:09 | → | dcoutts joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 09:53:27 | → | danse-nr3 joins (~danse@151.57.223.96) |
| 09:56:07 | → | NSFAF joins (~NSFAF@105.232.14.71) |
| 10:02:23 | → | lortabac joins (~lortabac@37.97.111.147) |
| 10:04:29 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 240 seconds) |
| 10:05:29 | × | sympt quits (~sympt@user/sympt) (Quit: Ping timeout (120 seconds)) |
| 10:06:23 | → | sympt joins (~sympt@user/sympt) |
| 10:07:47 | → | mmhat joins (~mmh@p200300f1c70b449eee086bfffe095315.dip0.t-ipconnect.de) |
| 10:07:58 | → | chele joins (~chele@user/chele) |
| 10:12:00 | × | NSFAF quits (~NSFAF@105.232.14.71) (Ping timeout: 255 seconds) |
| 10:12:49 | × | econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 10:17:38 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 10:23:14 | → | raym joins (~ray@user/raym) |
| 10:24:08 | → | chele joins (~chele@user/chele) |
| 10:28:02 | → | Lycurgus joins (~georg@user/Lycurgus) |
| 10:28:29 | → | ubert joins (~Thunderbi@2a02:8109:ab8a:5a00:ce61:4d12:7531:ec69) |
| 10:36:13 | → | polux6 joins (~polux@51-15-169-172.rev.poneytelecom.eu) |
| 10:36:18 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 255 seconds) |
| 10:37:15 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 10:37:17 | × | polux quits (~polux@51-15-169-172.rev.poneytelecom.eu) (Ping timeout: 240 seconds) |
| 10:37:17 | polux6 | is now known as polux |
| 10:37:48 | → | NSFAF joins (~NSFAF@105.232.14.71) |
| 10:38:16 | × | rosco quits (~rosco@175.136.156.77) (Quit: Lost terminal) |
| 10:38:35 | → | NSFAF_ joins (~NSFAF@105.232.14.71) |
| 10:39:38 | → | NSFAF__ joins (~NSFAF@105.232.14.71) |
| 10:40:12 | → | euleritian joins (~euleritia@dynamic-176-006-187-025.176.6.pool.telefonica.de) |
| 10:42:22 | × | NSFAF quits (~NSFAF@105.232.14.71) (Ping timeout: 246 seconds) |
| 10:42:31 | → | NSFAF joins (~NSFAF@105.232.14.71) |
| 10:43:25 | × | NSFAF quits (~NSFAF@105.232.14.71) (Max SendQ exceeded) |
| 10:43:25 | × | NSFAF_ quits (~NSFAF@105.232.14.71) (Ping timeout: 246 seconds) |
| 10:44:59 | × | NSFAF__ quits (~NSFAF@105.232.14.71) (Ping timeout: 260 seconds) |
| 10:45:22 | → | NSFAF joins (~NSFAF@130.185.144.25) |
| 10:45:49 | × | bilegeek quits (~bilegeek@2600:1008:b023:d9e2:9f22:5071:205d:e817) (Quit: Leaving) |
| 10:52:29 | × | [_________] quits (~oos95GWG@user/oos95GWG) (Quit: [_________]) |
| 10:54:32 | → | [_________] joins (~oos95GWG@user/oos95GWG) |
| 10:56:22 | × | NSFAF quits (~NSFAF@130.185.144.25) (Ping timeout: 246 seconds) |
| 10:59:59 | × | euleritian quits (~euleritia@dynamic-176-006-187-025.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 11:00:16 | → | euleritian joins (~euleritia@77.22.252.56) |
| 11:02:24 | × | lortabac quits (~lortabac@37.97.111.147) (Ping timeout: 255 seconds) |
| 11:07:42 | → | xff0x joins (~xff0x@ai082039.d.east.v6connect.net) |
| 11:08:42 | × | igemnace quits (~ian@user/igemnace) (Read error: Connection reset by peer) |
| 11:26:26 | → | igemnace joins (~ian@user/igemnace) |
| 11:36:45 | × | kaskal quits (~kaskal@213-147-167-18.nat.highway.webapn.at) (Quit: ZNC - https://znc.in) |
| 11:37:19 | → | kaskal joins (~kaskal@2001:4bb8:2c3:39c1:ff3f:d58:4fd9:e10c) |
| 11:40:40 | → | __monty__ joins (~toonn@user/toonn) |
| 11:43:44 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 11:45:10 | → | califax joins (~califax@user/califx) |
| 11:50:28 | → | fen78 joins (~fen@84.68.80.95) |
| 11:50:43 | <fen78> | hi, im having trouble using haskell |
| 11:50:54 | <fen78> | i cant get the things i call to be evaluated |
| 11:51:15 | <fen78> | can anyone help, thanks |
| 11:51:54 | × | m1dnight quits (~christoph@78-22-2-15.access.telenet.be) (Ping timeout: 255 seconds) |
| 11:52:11 | <danse-nr3> | maybe do some tests from the interpreter (ghci) to get acquainted with it fen78 |
| 11:52:17 | <fen78> | im thinking it might be a ghc issue, but maybe not |
| 11:52:35 | <fen78> | danse, i think ou misunderstand |
| 11:52:52 | <danse-nr3> | how long is your code? You could paste it in a pastebin and link that to us |
| 11:52:53 | <fen78> | i cant get *the things i call* to *be evaluated* |
| 11:53:01 | <fen78> | its a language issue |
| 11:53:16 | <fen78> | purelt theoretic, of course |
| 11:53:53 | <fen78> | i can use a bang pattern to ensure a bound variable is certainly evaluated |
| 11:54:05 | <fen78> | but i cant ask this condition be satisfied by an argument |
| 11:54:22 | <fen78> | i can say something has to be available via a class, but this could trigger reevaluation |
| 11:54:36 | <fen78> | idk how to express the condition within haskell |
| 11:55:58 | <fen78> | i have some random numbers that are universal, and used by many objects, i cant keep them in scope somehow without risking reevaluation, symantically its impossible, and this makes it risky, and lacking the ability to express it feels clunky |
| 11:56:41 | <fen78> | perhaps this can be acheived with linear types? |
| 11:57:20 | <fen78> | isnt that a way to annotate the type signature to ask that variables are uniquely calculated? |
| 11:57:28 | <fen78> | am i wrong to think that? |
| 11:57:32 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 11:58:18 | <fen78> | or is it that they are uniquely consumed? i forget |
| 11:58:41 | <fen78> | rrg, seems like i want a kind of opposite kind of linear types |
| 11:59:12 | <fen78> | anyone make sense of this, like formerly somehow? |
| 12:00:03 | <fen78> | basically, does it make sense about how i cannot demand of the argument that it is not going to trigger reevaluation |
| 12:01:12 | <fen78> | i was thinking there might be a hack with reflection and local instantiation somehow but i have no idea how |
| 12:02:36 | <fen78> | i think like, the fact you get to load up the class with an instance partway through the code means you can hove applied a bang pattern first! |
| 12:03:29 | → | lortabac joins (~lortabac@37.97.111.147) |
| 12:03:39 | <fen78> | ok so cool i can almost basically semantically express it, if there are these local instances involved somehow |
| 12:04:30 | <fen78> | this is basically then seems to be about not being able to put a bang pattern on a the binding in a class |
| 12:05:11 | <sprout> | haskell is lazy, just give it time until it gets out of bed |
| 12:05:48 | <sprout> | anyway, jokes aside. you shouldn't have this problem |
| 12:06:09 | <sprout> | pastebin your problem |
| 12:06:15 | <fen78> | reflection allows the binding to be made after a bang pattern is applied to a binding *not* in a class, and has to take place here rather in the class headder, in order to have the bang pattern binding preceding the class instantiation which uses it |
| 12:06:25 | <fen78> | no problem |
| 12:07:17 | × | CiaoSen quits (~Jura@2a05:5800:2c7:500:e6b9:7aff:fe80:3d03) (Ping timeout: 240 seconds) |
| 12:07:27 | <fen78> | nono, the question is about if there is understanding about this bang patterns in classes and the relevency of reflection at least in explaining it, could help thoerise a way to incorperate it into the semantics of the language properly |
| 12:07:59 | <fen78> | we already have some weird ? symbol |
| 12:08:34 | <fen78> | which i think was involved in some kind of semantics of reflection |
| 12:10:22 | <fen78> | i guess the comment is something about with this language extension that because it allows bang patterns to preceed reflectins to constraint based scope, that it solves this glitch i was describing |
| 12:11:16 | <fen78> | variables in constraints, using these ? symbols, *can* be bang pattern guarded by the user so the consumption from scope is guarantied not to cause reevaluation |
| 12:11:29 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 12:12:10 | <fen78> | ? constraints being bindable within code |
| 12:12:18 | <fen78> | but anyway, this way of expressing it sucks |
| 12:12:28 | <fen78> | and it only results from no bang patterns in classes |
| 12:12:38 | → | califax joins (~califax@user/califx) |
| 12:12:42 | × | lortabac quits (~lortabac@37.97.111.147) (Ping timeout: 256 seconds) |
| 12:13:00 | <fen78> | this must be a thing that should make sense enough to encorperate into the language in a less obscure way |
| 12:13:58 | <fen78> | i guess a code question which stems from this is how to demonstrate this in action |
| 12:14:50 | <fen78> | ? scope referencing with some way of wrapping the bang pattern guarding in some functions to make it cinvinient to load into scope these strict variables |
| 12:14:59 | → | m1dnight joins (~christoph@78-22-14-161.access.telenet.be) |
| 12:15:33 | → | lortabac joins (~lortabac@37.97.111.147) |
| 12:16:46 | <fen78> | and btw, i have no idea why this is something i have only just encountered, and is so insanely bizzare, but could be a real language niggle, that is worth contending with |
| 12:17:22 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 12:17:48 | <fen78> | as in how much this serupticiously affects us, given its obscurity in terms of langage considerations resulting in a strange paradigm |
| 12:18:13 | <fen78> | "im never sure anything is strict" |
| 12:18:48 | <danse-nr3> | anything is non-strict. You are exaggerating things, just get acquainted with the evaluation model |
| 12:18:53 | <fen78> | enormous variables you dont even realise your afraid to reference |
| 12:19:08 | <danse-nr3> | or keep on with your monologue |
| 12:19:50 | <fen78> | i was trying to say you can notionally hijack the reflection tooling to bring about a strict referencing paradigm |
| 12:20:22 | <fen78> | and i want someone to help me with these ? things cos iv never used them |
| 12:21:06 | → | califax joins (~califax@user/califx) |
| 12:21:41 | × | synchromesh quits (~synchrome@2407:7000:aa2d:4e00:59a1:9e62:4e88:7daa) (Read error: Connection reset by peer) |
| 12:21:50 | <fen78> | description was variable bound from constrait scope, having been reflected from within the main body of code (not top level constraint binding) |
| 12:22:51 | × | chele quits (~chele@user/chele) (Ping timeout: 256 seconds) |
| 12:23:11 | → | synchromesh joins (~synchrome@2407:7000:aa2d:4e00:9cf7:efcb:5efd:a99) |
| 12:23:38 | <fen78> | examination of the type of the function doing the call to the function in the constraint with the ? |
| 12:24:30 | <danse-nr3> | apologies i need to go now but if you can come up with some more down-to-earth question of example of unexpected behaviour, possibly someone else can help |
| 12:24:34 | <fen78> | this is the examination of the "could be strict" constraint as a scope |
| 12:25:06 | <fen78> | yeah, anyone online |
| 12:25:08 | × | [Leary] quits (~Leary]@user/Leary/x-0910699) (Remote host closed the connection) |
| 12:25:14 | <fen78> | danse has to go |
| 12:25:26 | → | [Leary] joins (~Leary]@user/Leary/x-0910699) |
| 12:26:17 | <fen78> | tldr ? in constraints could be strict! |
| 12:26:41 | <fen78> | and, how stupid is that as a formalism, helpf |
| 12:27:11 | <danse-nr3> | if you don't like non-strict just use ocaml by the way |
| 12:27:47 | <fen78> | i can express potentially strict... |
| 12:28:03 | <fen78> | in *this* language, thank you |
| 12:28:28 | <fen78> | as in, i mean, your welcome, somehow |
| 12:29:23 | <fen78> | ok, heres a good question. is this the only way we have of even doing anything about strictness at type level? |
| 12:29:45 | <fen78> | that, use of ?, might be strict. cos thats lame |
| 12:30:13 | <fen78> | i want, certainly is strict! |
| 12:30:16 | <fen78> | i think... |
| 12:30:35 | <__monty__> | What non-strictness is there at type level? Types are checked at compile time, they're not part of Haskell's evaluation model are they? |
| 12:30:35 | <fen78> | and linear types totally fails in this? i never got a response on that |
| 12:30:58 | <fen78> | no, not in terms of type level computation |
| 12:31:11 | <fen78> | about strictness at term level, expressed at type level |
| 12:31:38 | <__monty__> | Because your questions don't make sense. Linear types only apply within a function and you're talking about globally available random numbers. |
| 12:32:08 | <fen78> | that is that the emession of data that can only be used once? |
| 12:32:23 | <fen78> | thats like literally the opposite of what i want |
| 12:33:36 | <fen78> | bascally constraints dont serve all that well for values that *can* be strictly evaluated |
| 12:34:09 | <fen78> | like, class definitions with no arguments |
| 12:34:12 | <__monty__> | Linear types don't restrict how many times the output of a function is used. |
| 12:34:29 | × | danse-nr3 quits (~danse@151.57.223.96) (Ping timeout: 240 seconds) |
| 12:34:59 | <__monty__> | I assume you're talking about type class constraints? Can you give an example? |
| 12:35:39 | <fen78> | i think what im saying is that it should be expressible within the type semantics, to differentiate strictly bindable terms. |
| 12:36:35 | <fen78> | ie those without arguments |
| 12:36:36 | <__monty__> | What are "terms," and what is "strictly bindable?" |
| 12:36:47 | <fen78> | things at term level are terms? |
| 12:37:17 | <fen78> | strictly bindable terms can be bound using a bang pattern |
| 12:37:31 | <fen78> | cant do that on a function, doesnt make sense |
| 12:37:44 | <__monty__> | Why not? |
| 12:37:56 | <fen78> | wouldnt trigger its evaluation |
| 12:37:56 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 12:38:26 | <fen78> | some kind of totally evaluatedness of a thing that doesnt take arguments, that a thing that takes arguments quite obviously doesnt also |
| 12:38:42 | <__monty__> | You very well can want a function argument to be evaluated up to its arguments. |
| 12:39:19 | <fen78> | you cant do that# |
| 12:39:32 | <kuribas> | fen78: haskells type system doesn't track strictness |
| 12:39:39 | <fen78> | the latter arguments can appear in the computation using the previous arguments |
| 12:39:43 | <kuribas> | It doesn't track totality either. |
| 12:40:06 | <fen78> | argument provision order has nothing to do witht the inner computations partitioning |
| 12:40:18 | <kuribas> | everything is lazy by default in haskell anyway. |
| 12:40:48 | × | gentauro quits (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 12:40:49 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 268 seconds) |
| 12:40:53 | <fen78> | lazyness does not apply to function argument application |
| 12:41:04 | <__monty__> | Can't do what? You can evaluate any expression to WHNF. |
| 12:41:16 | <fen78> | not if it still requires arguments! |
| 12:41:24 | <kuribas> | fen78: idris has a "Lazy" type to designate a value lazy. |
| 12:41:29 | <fen78> | gona do like half the computation somehow |
| 12:42:06 | <__monty__> | `if True then id else const` can be evaluated to `id`. And `id` still takes an argument. |
| 12:42:37 | <fen78> | we have lazy by default but no strictness annotation in the type system unless you count ? as could be strict as actually aslmost a reasonable solution |
| 12:43:31 | <fen78> | monty: there exist functions where the lack of arguments yet to be applied will prevent the use of the arguments already applied. |
| 12:44:29 | <__monty__> | fen78: I don't see how such a function couldn't be evaluated to WHNF, which is all bang patterns do. |
| 12:44:35 | <fen78> | ou cant annotate a function type with strictness indications, because you cant stipulate about the partial completeness of any computation yet to recieve arguments |
| 12:44:41 | <haskellbridge> | <mauke> `undefined :: a -> b` requires an argument (says its type), but it still explodes if you force it |
| 12:45:31 | <fen78> | imagine a net without its neuron provided, what are you going to do with the numbers to try and do half the computation while you wait for the neuron. nothing! |
| 12:45:34 | × | m1dnight quits (~christoph@78-22-14-161.access.telenet.be) (Ping timeout: 256 seconds) |
| 12:46:14 | <fen78> | i cant have the type of my net with the neuron yet to be provided demanding the net is already evaluated |
| 12:46:53 | <fen78> | strict functions by partial application dont make any sense! |
| 12:47:07 | → | gentauro joins (~gentauro@user/gentauro) |
| 12:47:30 | → | m1dnight joins (~christoph@78-22-2-15.access.telenet.be) |
| 12:47:33 | <fen78> | the innards of the function have nothing to do with the order of the arguments |
| 12:47:43 | <__monty__> | I don't see why not. Every argument a strict function is applied to (partially or otherwise) will be evaluated first. |
| 12:47:50 | <fen78> | strictness only on value like things plz |
| 12:48:32 | <fen78> | oh thats just using the function like a bang pattern on all its arguments |
| 12:48:52 | <fen78> | and its not what im saying |
| 12:48:58 | <fen78> | your function could cause recomputation |
| 12:49:05 | <__monty__> | ELI5 |
| 12:49:12 | <fen78> | it just says that it is evaluated |
| 12:49:16 | <haskellbridge> | <mauke> `hmm :: a -> b -> b; hmm x = seq x undefined` |
| 12:49:37 | <haskellbridge> | <mauke> How strict is this function? |
| 12:50:28 | <fen78> | your version says, its evaluated, mine said, it was only ever evaluated once |
| 12:50:46 | <haskellbridge> | <mauke> Actually, make that hmm x _ = ... |
| 12:50:48 | <fen78> | strict before binding to a constraint |
| 12:51:36 | <fen78> | thats what ? allows you to do with class instantiation in the body and not in the class head where strict evaluation is precluded |
| 12:51:36 | <dminuoso> | fen78: You mentioned ? as strictness annotation in Haskell, what are you referring to? |
| 12:51:47 | <fen78> | the class reflection thing |
| 12:52:00 | <fen78> | x ? :: Int => |
| 12:52:04 | <fen78> | something like that |
| 12:52:22 | <dminuoso> | I have not seen that before |
| 12:52:34 | <dminuoso> | Which extension is that from? Or do you know of any package that uses it? |
| 12:52:53 | <fen78> | language extension i think |
| 12:53:01 | <fen78> | cant remember trying to find |
| 12:53:12 | <dminuoso> | What does ? do here? |
| 12:53:59 | × | m1dnight quits (~christoph@78-22-2-15.access.telenet.be) (Ping timeout: 272 seconds) |
| 12:54:14 | <fen78> | there is presumably some associated syntax at value level that reflects the instance up |
| 12:54:37 | <dminuoso> | Also, what does `Int =>` denote here? |
| 12:54:46 | → | danse-nr3 joins (~danse@151.43.209.161) |
| 12:55:01 | <fen78> | just that the "class instance" being reffered to in the constraint was locally instantiated and not at top level in the class head, so allowing it io be a strict reference unlike a regular constraint |
| 12:55:08 | × | danse-nr3 quits (~danse@151.43.209.161) (Remote host closed the connection) |
| 12:55:26 | <fen78> | could be: |
| 12:55:31 | → | danse-nr3 joins (~danse@151.43.209.161) |
| 12:55:33 | <fen78> | ? x :: Int => |
| 12:55:34 | <dminuoso> | I dont understand any of that. |
| 12:55:57 | <dminuoso> | Are you talking about ImplicitParams? |
| 12:56:04 | <haskellbridge> | <mauke> Implicit parameters? |
| 12:56:05 | <fen78> | costraints usually refer to instanctiations made in instance blocks at top level |
| 12:56:11 | <fen78> | in classes defined at top level |
| 12:56:15 | <fen78> | this is not the same |
| 12:56:23 | <fen78> | yes, thank you |
| 12:56:56 | <fen78> | ImplicitParams is "our" workaround for "might be strict" |
| 12:57:02 | <dminuoso> | 13:56:05 fen78 │ costraints usually refer to instanctiations made in instance blocks at top level |
| 12:57:08 | <dminuoso> | I dont even understand what that means, either. |
| 12:57:24 | <fen78> | instance Myclass where |
| 12:57:35 | <fen78> | no bang patterns here |
| 12:57:47 | <fen78> | implicitparams gives a workaround thereon |
| 12:58:01 | <dminuoso> | What do ImplicitParams have to do with typeclass instances, here? |
| 12:58:12 | <fen78> | they provide local instantiation |
| 12:58:20 | <fen78> | as well as presumably local class declaration |
| 12:59:04 | <dminuoso> | Well yes, ImplicitParams makes uses of the constraint system. |
| 12:59:11 | <fen78> | reification syntax at value level basically gives a place for tokens relating to the class function definition |
| 12:59:14 | <dminuoso> | But beyond that, I dont see any relation to strictness. |
| 12:59:55 | <fen78> | you cant have a bang pattern in an Instance binding |
| 12:59:59 | <fen78> | ! |
| 13:00:10 | <fen78> | you can reflect strict things! |
| 13:00:28 | <dminuoso> | Sorry, I fail to understand what you are saying here. |
| 13:00:55 | <fen78> | when reflection syntax is used at type level, the terms it references might be strict |
| 13:01:17 | <fen78> | while the terms referenced by regular class based constraints, do not share this property |
| 13:02:05 | <fen78> | ie the reflection syntax is actually ending up allowing us to make a statement about the increased pottentiality (from 0 to possible) of the thing being referenced being strict |
| 13:03:25 | <fen78> | the thing that related ImplicitParams to strictness, is that by allowing instantiation away from top level, that a definately no strictness, inhereted from usually constraints are instantiated at top level and so are definately not strict mindset... |
| 13:03:54 | → | NSFAF joins (~NSFAF@105.232.14.71) |
| 13:04:15 | <fen78> | is lifted... sorry garbled |
| 13:04:25 | → | NSFAF_ joins (~NSFAF@105.232.14.71) |
| 13:04:54 | <fen78> | definately no strictness is lifted when constraints might not be instantiated at top level and so be without bangpatterns |
| 13:06:07 | <fen78> | local instances allow strict reflections to constraints which nolonger only contain non-strict variables |
| 13:06:10 | × | raym quits (~ray@user/raym) (Quit: leaving) |
| 13:06:29 | × | NSFAF_ quits (~NSFAF@105.232.14.71) (Read error: Connection reset by peer) |
| 13:06:46 | → | NSFAF_ joins (~NSFAF@105.232.14.71) |
| 13:07:04 | <fen78> | i mean, sure this isnt enough to uinderstand what it might look like done properly? |
| 13:07:38 | <fen78> | bang patterns at top level is what iv got my money on |
| 13:07:47 | <fen78> | any reason why not |
| 13:07:50 | <fen78> | in instances i mean |
| 13:08:10 | <fen78> | #BangPatternInstances proposal |
| 13:08:49 | <fen78> | which im sure gives suitable motivation for strictness annotation for non function types |
| 13:08:53 | × | NSFAF quits (~NSFAF@105.232.14.71) (Ping timeout: 256 seconds) |
| 13:10:01 | <fen78> | i guess we need a different symbol to annotate strict terms |
| 13:10:31 | <fen78> | bangs in types is taken |
| 13:10:52 | <fen78> | i mean, is there any reason we *dont* have strictness annotations? |
| 13:11:00 | <fen78> | because instances have no bang patterns!? |
| 13:11:01 | × | lortabac quits (~lortabac@37.97.111.147) (Ping timeout: 256 seconds) |
| 13:11:20 | <fen78> | its a limiatation in terms of the syntax of *binding* uniform binding syntax is essential! |
| 13:11:31 | <fen78> | bang patterns didnt make it deep enough into the language |
| 13:11:51 | <fen78> | and if they did, then we would be encountering strict variables all the time! enough to bother annotating them |
| 13:12:37 | <fen78> | theres no top level strictenss at all! |
| 13:12:47 | <fen78> | presumably you could have top level strict functions? |
| 13:13:35 | <fen78> | maybe this messes with evaluation order of the program |
| 13:13:41 | <fen78> | weird! |
| 13:13:57 | <fen78> | so you kind of cant have that or it tries to compute something before you tell it to |
| 13:14:35 | <fen78> | ok then, you could have special syntax for stric reflection |
| 13:14:48 | <fen78> | like not ?, so maybe ?? |
| 13:15:10 | <fen78> | so its stronger than could be strict, and is strict, and then you get an associated strict reflector at term level |
| 13:15:28 | <fen78> | that was the code example i wanted |
| 13:15:31 | <fen78> | this strict reflector |
| 13:15:46 | <fen78> | and the type signature of the thing it interacts with |
| 13:15:47 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 13:16:01 | <fen78> | to see the ? in scope |
| 13:16:36 | <fen78> | just with some id biolerplate which uses a bang pattern or seq or whatever to make the reflected thing strict |
| 13:16:45 | → | shapr joins (~user@2603:3005:b31:e100:7e64:336c:bc17:801d) |
| 13:16:47 | <fen78> | and the language proposal would then be to make this item a language construct |
| 13:17:19 | <fen78> | you did the strict reflection, you can use the ?? symbol to ask for the strict variable for you to reference |
| 13:17:32 | <fen78> | weird how it ends up being by use of is implicit params |
| 13:17:33 | → | califax joins (~califax@user/califx) |
| 13:18:13 | × | mulk quits (~mulk@pd9514a85.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 13:18:15 | → | CiaoSen joins (~Jura@2a05:5800:2c7:500:e6b9:7aff:fe80:3d03) |
| 13:18:17 | <fen78> | basically in lew of the language extension you just have ? and this construct and have to remember if you used it or not, and have no way to actually demand that it was |
| 13:18:27 | <fen78> | so it would strictly strngthen the language in this sense |
| 13:18:57 | <fen78> | a normally reflected implicit parameter, would fail to satisfy the stronger ?? of a constraint |
| 13:19:37 | <fen78> | the type system rejecting the use of the weaker reflector, when the stronger is required |
| 13:19:52 | <fen78> | in terms of strictness |
| 13:20:31 | <fen78> | ?? in constriants would give a significantly different extra structure to the types comprising a program |
| 13:20:32 | <lambdabot> | in constriants would give a significantly different extra structure to the types comprising a program |
| 13:20:41 | → | mulk joins (~mulk@pd9514af5.dip0.t-ipconnect.de) |
| 13:20:42 | <fen78> | thanks lambdabot |
| 13:22:24 | <fen78> | it allows the program graph to propegate clauses about strictness, which equate to guarantees within functions that a valriable can be referenced without triggering recomputation |
| 13:23:09 | <danse-nr3> | you are talking by yourself. Maybe you want to write a book or an article instead |
| 13:23:15 | <fen78> | it kind of says, if your going to all the effort of ensuring something is strict with a bang pattern, why is that data not apparent also at type level |
| 13:23:31 | <fen78> | danse: maybe you coulod help me understand |
| 13:24:01 | <danse-nr3> | it seems demanding considering your ambitions, and i have got to work |
| 13:24:09 | <fen78> | currently im trying to express what a strict annotation as a constraint would indicate |
| 13:24:41 | <fen78> | its not demanding. language extensions are easy for people that are not me |
| 13:24:46 | <fen78> | i just have to convey it |
| 13:24:51 | <fen78> | and think of it! |
| 13:25:01 | <fen78> | bloody, asking me to write him a book a seccond ago! |
| 13:25:17 | → | oneeyedalien joins (~oneeyedal@user/oneeyedalien) |
| 13:25:26 | <fen78> | probably only reason implicitparams is a worthy theoretical structure at all |
| 13:25:31 | <danse-nr3> | did not write "write /me/ a book" |
| 13:25:44 | <fen78> | noqw he doenst even want the book! |
| 13:26:17 | <danse-nr3> | you might be someone who enjoys trolling subtly. I am jealous for all the time you have got to waste |
| 13:26:40 | <fen78> | im not taking book writing requests from the type of person that comissions books without then accepting reciept of the commision, that is a no commission of books scenario |
| 13:27:03 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 13:27:34 | <danse-nr3> | be careful to not make your trolling too plain |
| 13:27:36 | <fen78> | its just an extra ? its not too much to ask |
| 13:27:49 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 13:27:52 | <fen78> | cant i get some help with that though, i cant understand the implications |
| 13:27:55 | <haskellbridge> | <Jade> Why can I not write `data Foo a where X :: Foo a` using `-XGADTSyntax`? |
| 13:27:55 | <haskellbridge> | <Jade> It tells me to enable `-XGADT` |
| 13:28:11 | → | califax joins (~califax@user/califx) |
| 13:28:18 | × | euleritian quits (~euleritia@77.22.252.56) (Ping timeout: 268 seconds) |
| 13:28:39 | <fen78> | you gota have the :: |
| 13:28:56 | <fen78> | just omit X :: |
| 13:29:09 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 13:29:17 | <fen78> | erp what, no its the Foo a |
| 13:29:31 | <fen78> | and the where! |
| 13:29:31 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Read error: Connection reset by peer) |
| 13:29:59 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 13:30:14 | <fen78> | data Foo a = X (x :: Foo a) |
| 13:30:17 | <fen78> | or |
| 13:30:39 | <haskellbridge> | <Jade> yes, but those should work with `GADTSyntax` alone, right? The user guide gives the example of `newtype Down a where Down :: a -> Down a` which also doesn't work |
| 13:30:49 | <fen78> | data Foo a where X :: Foo a |
| 13:31:32 | <fen78> | dafuq |
| 13:31:42 | <fen78> | i didnt even know of this |
| 13:31:56 | <fen78> | well apparently not |
| 13:32:09 | <fen78> | maybe less maintained |
| 13:32:50 | <fen78> | i would just go ahead and use the correct extension |
| 13:33:06 | → | lortabac joins (~lortabac@37.97.111.147) |
| 13:34:19 | <fen78> | anyway, i much prefer the constraints way to eg datatypes or anything at term level for strictness |
| 13:34:28 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 268 seconds) |
| 13:34:36 | <haskellbridge> | <Jade> I figured out my mistake ... I wrote `-XGADTSyntax -XNoGADTs` and the latter disabled `-XGADTSyntax` ... |
| 13:34:46 | <fen78> | i dont care if your functions output strict values, or your datatypes have strict values in their fancy constructors, or anything. |
| 13:34:52 | <haskellbridge> | <Jade> I think there's an open ticket for flags interferring with each other |
| 13:35:10 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 13:35:18 | <fen78> | pointless to me if a function somewhere inside makes a strict call with a bang pattern. |
| 13:35:50 | <fen78> | now, you reflect something up as an argument, and now i know its strict cos its not supplied *as a function argument* anymopre |
| 13:35:56 | <fen78> | now you have my attention |
| 13:36:10 | → | califax joins (~califax@user/califx) |
| 13:37:02 | <fen78> | this means you could basically prefix an arrow with a ?, but via the constraints it becomes order independent which is sometimes nice |
| 13:37:51 | <fen78> | ah, right, thats why implicit params binds the variable name at the type level, because there is no place to bind it when its not an argument |
| 13:38:06 | × | targetdisk quits (~daemonchi@45-33-4-162.ip.linodeusercontent.com) (Remote host closed the connection) |
| 13:38:58 | <fen78> | so, if you have a function argument that *is* strict, instead, supply it as an implicit parameter, this way using the syntax as a placeholder for strictness indicatiopn |
| 13:39:08 | <lortabac> | fen78: if I understand correctly you want to express strictness in types via constraints on argument names |
| 13:39:12 | <fen78> | this should be way more of a thing than it is! |
| 13:40:49 | <fen78> | lortabec: yeah. the syntax is like fun :: ? x :: Int,y~Int => y, instead of fun :: (x~Int,y~Int) => x -> y -> ... |
| 13:41:14 | <fen78> | fun :: ? x :: Int,y~Int => y -> ... |
| 13:41:22 | <fen78> | fun :: (x~Int,y~Int) => x -> y -> ... |
| 13:41:46 | <fen78> | fun :: (? x :: Int,y~Int) => y -> ... |
| 13:42:04 | <fen78> | and that also says that x appears bound at term level |
| 13:42:12 | <fen78> | like if the class function was called x |
| 13:42:23 | <fen78> | and existed vian an instance as indicated in the constraint |
| 13:42:46 | <lortabac> | maybe you can start from some library like 'named' |
| 13:42:50 | <lortabac> | @hackage named |
| 13:42:50 | <lambdabot> | https://hackage.haskell.org/package/named |
| 13:43:01 | <lortabac> | and add support for strictness constraints |
| 13:44:22 | <lortabac> | to be honest it doesn't look like a simple task, but with enough effort it may be doable |
| 13:45:11 | <fen78> | i think that relies on singletons |
| 13:45:14 | <fen78> | my way doesnt |
| 13:45:21 | <fen78> | no weird text coversion |
| 13:45:36 | <fen78> | actually i have no idea how it tries to bind variables to scope by their name |
| 13:45:43 | <fen78> | but implicait parameters does it perfectly |
| 13:45:48 | <lortabac> | what do you mean by "my way"? do you already have a library that does this? |
| 13:46:02 | <fen78> | implicit parameters presumbaly exists for this reason |
| 13:46:29 | <fen78> | i was working on it ages ago with some unsafecoece thing |
| 13:46:39 | <fen78> | the original reflection stuff |
| 13:46:42 | <lortabac> | oh ok |
| 13:46:47 | <fen78> | but the only reason for the syntax is the theory |
| 13:46:58 | <lortabac> | today you don't need unsafeCoerce anymore for that kind of reflection |
| 13:47:04 | <lortabac> | there is withDict |
| 13:47:16 | <fen78> | im on about the richness it brings to the syntax |
| 13:47:28 | <lortabac> | https://hackage.haskell.org/package/base-4.19.0.0/docs/GHC-Exts.html#t:WithDict |
| 13:47:30 | <fen78> | indicating instantiation occurs away from top level allows for strictness to have occured |
| 13:47:38 | <lortabac> | withDict allows you to create local instances |
| 13:47:52 | <fen78> | yes this is the way id go |
| 13:47:54 | → | m1dnight joins (~christoph@82.146.125.185) |
| 13:47:59 | <fen78> | that with the strictness |
| 13:48:12 | <lortabac> | the problem with this kind of reflection is that you can't override the local instances |
| 13:48:15 | <fen78> | but the implicit parameters basically replaces that, and id go for the language proposal really |
| 13:48:57 | <fen78> | i think there could be a lot of good theory work done on how these strictness guaranties percolating on the types gives users assurances such as costless databasing |
| 13:49:30 | <lortabac> | I'm pretty sure there is already a lot of literature on strictness annotations in types |
| 13:49:40 | <fen78> | lortabac: iirc you have to pass around the scope in which the instances hold |
| 13:49:43 | <lortabac> | there may even be something on Hackage |
| 13:50:04 | <fen78> | ahh, yes, it was constraint continuations |
| 13:50:18 | <fen78> | ((a->b)->b) encodes a |
| 13:50:45 | <fen78> | ((? _ :: a=>b)->b) encodes a |
| 13:51:36 | <fen78> | give me a function which needs an a |
| 13:51:55 | <lortabac> | ah nice |
| 13:52:12 | <lortabac> | this may solve a problem that I have with one of my projects :) |
| 13:52:28 | <fen78> | ((?? x :: a=>b)->b) encodes !x :: a |
| 13:53:43 | <fen78> | i guess since the ? at term level, then you could use !? |
| 13:54:06 | <fen78> | !? x :: a=> |
| 13:55:13 | × | shapr quits (~user@2603:3005:b31:e100:7e64:336c:bc17:801d) (Ping timeout: 256 seconds) |
| 13:57:09 | <fen78> | so at term level its like let ?x :: a = ... |
| 13:57:30 | <fen78> | so you could have ??x :: a or !?x :: a |
| 14:00:45 | <fen78> | you could use ?? for linear types that are locally instantiated but not nesacarily strict |
| 14:01:14 | <fen78> | destroy after using anywhere variables are guarantied not to be used anywhere else |
| 14:01:43 | <fen78> | if they were strictly created, ie the point where there started being a linear object that can only be used once |
| 14:02:12 | <fen78> | reflection serves as a great point to interject information about strictness and linearness |
| 14:02:58 | <fen78> | i think there is actually a redundancy between linear and strict |
| 14:03:09 | <fen78> | i dont really care if you have computed it or not if its linear |
| 14:03:17 | <fen78> | because i will be the only place that uses it |
| 14:03:25 | <fen78> | doesnt matter when its computed so |
| 14:03:45 | <fen78> | normally you care if something is strict before it gets to you because of copies |
| 14:03:57 | <fen78> | linear types circumvents this, sionce there are no copies |
| 14:04:03 | → | thegeekinside joins (~thegeekin@189.217.83.221) |
| 14:04:16 | <fen78> | i think linear types in the way it relates to strictness like this, again pips us to the post |
| 14:04:35 | <fen78> | by bypassing strictness concerns completely! |
| 14:04:46 | <fen78> | so lazy! |
| 14:04:51 | × | CiaoSen quits (~Jura@2a05:5800:2c7:500:e6b9:7aff:fe80:3d03) (Ping timeout: 256 seconds) |
| 14:05:26 | <fen78> | i guess in that way a linearity declaratin basically makes a statement equivalent to strictness, but the other way round by making it redundant that its not strict |
| 14:05:48 | <fen78> | renders stric meaningless as an annotation is what we opted for *facepalm* |
| 14:06:31 | <fen78> | in which case i think its a shame that linear types didnt go for the reflection syntax based approach |
| 14:06:45 | <fen78> | a function arrow is kind of crap |
| 14:06:46 | × | thegeekinside quits (~thegeekin@189.217.83.221) (Read error: Connection reset by peer) |
| 14:07:04 | <fen78> | i mean, there is always going to be both options, via constraint or argument |
| 14:07:23 | <fen78> | variables in scope by constraint environment or function argument provision |
| 14:08:01 | <fen78> | does linear haskell have linear constraints? |
| 14:11:04 | <fen78> | !(A ⊸ B) ⇒!A ⊸!B |
| 14:12:39 | × | troydm quits (~troydm@user/troydm) (Ping timeout: 260 seconds) |
| 14:12:44 | <fen78> | Linear types and uniqueness types are, at their core, dual: whereas a linear type is a contract that |
| 14:12:44 | <fen78> | a function uses its argument exactly once even if the call’s context can share a linear argument as |
| 14:12:45 | <fen78> | many times as it pleases, a uniqueness type ensures that the argument of a function is not used |
| 14:12:45 | <fen78> | anywhere else in the expression’s context even if the callee can work with the argument as it pleases. |
| 14:12:49 | <fen78> | i got that wrong... |
| 14:15:23 | <fen78> | aha! so the linear types paper discusses this |
| 14:15:37 | <fen78> | basically, they opted for a linear type system because linear logic exists |
| 14:15:42 | <fen78> | and uniquesness types are hard |
| 14:16:02 | <fen78> | what i was saying is that when you have strictness maybe you dont care so much about uniqueness |
| 14:16:10 | <fen78> | you have uniquesness of evlauation, so thats ok |
| 14:16:21 | × | mmhat quits (~mmh@p200300f1c70b449eee086bfffe095315.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
| 14:16:40 | <fen78> | both idioms permit copying |
| 14:16:52 | <fen78> | linear types can be copied but are consumed once each |
| 14:17:21 | <fen78> | uniquesness type preclude copying, but strictness permits it, all thats unique is the computation |
| 14:17:28 | <fen78> | copying then infact is favoured |
| 14:17:53 | <fen78> | dont use uniquesness, use strictness, then you can copy as much as you like |
| 14:20:45 | × | fen78 quits (~fen@84.68.80.95) (Quit: Connection closed) |
| 14:21:47 | → | thegeekinside joins (~thegeekin@189.217.83.221) |
| 14:22:08 | → | oneeyedalien_ joins (~oneeyedal@user/oneeyedalien) |
| 14:22:32 | × | NSFAF_ quits (~NSFAF@105.232.14.71) (Read error: Connection reset by peer) |
| 14:25:01 | × | oneeyedalien quits (~oneeyedal@user/oneeyedalien) (Ping timeout: 264 seconds) |
| 14:25:55 | × | szkl quits (uid110435@uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 14:29:51 | → | mmhat joins (~mmh@p200300f1c70b44daee086bfffe095315.dip0.t-ipconnect.de) |
| 14:35:27 | × | lortabac quits (~lortabac@37.97.111.147) (Ping timeout: 256 seconds) |
| 14:36:42 | → | chele joins (~chele@user/chele) |
| 14:50:25 | × | myxos quits (~myxos@065-028-251-121.inf.spectrum.com) (Remote host closed the connection) |
| 14:50:37 | × | actioninja quits (~actioninj@user/actioninja) (Quit: Ping timeout (120 seconds)) |
| 14:50:41 | → | Square joins (~Square@user/square) |
| 14:51:00 | → | actioninja joins (~actioninj@user/actioninja) |
| 14:52:50 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Ping timeout: 255 seconds) |
| 14:53:23 | × | Square3 quits (~Square4@user/square) (Ping timeout: 264 seconds) |
| 14:53:23 | → | myxos joins (~myxos@065-028-251-121.inf.spectrum.com) |
| 14:53:40 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 14:54:02 | × | Maxdamantus quits (~Maxdamant@user/maxdamantus) (Ping timeout: 252 seconds) |
| 14:54:41 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 14:54:59 | → | Maxdamantus joins (~Maxdamant@user/maxdamantus) |
| 14:58:20 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 268 seconds) |
| 14:59:51 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 15:00:35 | × | danse-nr3 quits (~danse@151.43.209.161) (Remote host closed the connection) |
| 15:01:30 | → | danse-nr3 joins (~danse@151.43.209.161) |
| 15:03:21 | → | shapr joins (~user@c-24-218-186-89.hsd1.ma.comcast.net) |
| 15:04:16 | → | lortabac joins (~lortabac@37.97.111.147) |
| 15:06:25 | × | lortabac quits (~lortabac@37.97.111.147) (Client Quit) |
| 15:07:07 | × | lottaquestions_ quits (~nick@2607:fa49:503d:b200:a224:6171:dcbc:3474) (Quit: Konversation terminated!) |
| 15:16:40 | → | CiaoSen joins (~Jura@2a05:5800:2c7:500:e6b9:7aff:fe80:3d03) |
| 15:30:53 | × | mulk quits (~mulk@pd9514af5.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 15:31:54 | → | mulk joins (~mulk@pd95147b3.dip0.t-ipconnect.de) |
| 15:34:05 | × | xff0x quits (~xff0x@ai082039.d.east.v6connect.net) (Ping timeout: 240 seconds) |
| 15:34:12 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 15:35:45 | → | Vq joins (~vq@2001:2043:1c58:ea00:ca7f:54ff:fe6a:fd48) |
| 15:36:20 | → | xff0x joins (~xff0x@178.255.149.135) |
| 15:38:31 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 260 seconds) |
| 15:41:11 | × | xff0x quits (~xff0x@178.255.149.135) (Ping timeout: 256 seconds) |
| 15:41:52 | × | CiaoSen quits (~Jura@2a05:5800:2c7:500:e6b9:7aff:fe80:3d03) (Ping timeout: 255 seconds) |
| 15:42:07 | × | danse-nr3 quits (~danse@151.43.209.161) (Ping timeout: 268 seconds) |
| 15:42:39 | → | xff0x joins (~xff0x@ai082039.d.east.v6connect.net) |
| 15:45:57 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 15:47:39 | → | danse-nr3 joins (~danse@151.43.209.161) |
| 15:49:35 | → | todi joins (~todi@p4fd1a2f5.dip0.t-ipconnect.de) |
| 15:52:01 | → | euphores joins (~SASL_euph@user/euphores) |
| 15:52:36 | × | danse-nr3 quits (~danse@151.43.209.161) (Ping timeout: 268 seconds) |
| 15:54:06 | × | oneeyedalien_ quits (~oneeyedal@user/oneeyedalien) (Quit: Leaving) |
| 15:54:27 | × | Square quits (~Square@user/square) (Ping timeout: 255 seconds) |
| 15:55:32 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 15:55:49 | → | danse-nr3 joins (~danse@151.43.209.161) |
| 15:59:58 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 264 seconds) |
| 16:00:07 | × | ubert quits (~Thunderbi@2a02:8109:ab8a:5a00:ce61:4d12:7531:ec69) (Remote host closed the connection) |
| 16:02:13 | × | danse-nr3 quits (~danse@151.43.209.161) (Ping timeout: 264 seconds) |
| 16:11:12 | <tinjamin> | geez fen78 really had a monologue |
| 16:14:14 | → | danse-nr3 joins (~danse@151.43.209.161) |
| 16:15:58 | <shapr> | srk: nice to see activity on haskellEmbedded! |
| 16:20:44 | <tinjamin> | very vague and common question but like in general, what is haskell specialized for? Like C and Rust are good for systems programming, but idk what haskell is good for |
| 16:22:30 | × | cfricke quits (~cfricke@user/cfricke) (Ping timeout: 268 seconds) |
| 16:25:00 | <sm> | tinjamin: it's a language good for many things but people usually get most benefit when you need high quality/high assurance; high expressiveness for implementing complex logic; and/or high maintainability for medium/large codebases over medium/long term |
| 16:26:36 | <sm> | currently it's often seen in fintech, as the backend for web apps, and for implementing/processing languages |
| 16:27:11 | <sm> | also, of course, it's very good for teaching and research |
| 16:29:03 | <sm> | some people learn it early but I think it is most appreciated by experienced software developers |
| 16:32:36 | <EvanR> | are C and rust really good for systems programming |
| 16:33:12 | <EvanR> | C was originally for programming in a more abstract way when you weren't worried about numeric performance and didn't want fortran |
| 16:33:26 | <EvanR> | like ruby might be used for today |
| 16:33:46 | <EvanR> | haskell describes itself as a general purpose language |
| 16:34:13 | → | euleritian joins (~euleritia@dynamic-176-006-199-015.176.6.pool.telefonica.de) |
| 16:34:34 | × | euleritian quits (~euleritia@dynamic-176-006-199-015.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 16:34:57 | → | euleritian joins (~euleritia@77.22.252.56) |
| 16:37:01 | × | ski quits (~ski@ext-1-033.eduroam.chalmers.se) (Ping timeout: 260 seconds) |
| 16:37:18 | <haskellbridge> | <sm> "an expressive, powerful language for building high quality long lasting software at low cost" |
| 16:38:44 | <EvanR> | the long lasting part is interesting |
| 16:38:52 | <tinjamin> | sm: so if I want to get more into systems programming is it worth it to study haskell? don't get me wrong, ik it's worth it to study haskell because it's a new perspective and extraordinarily elegant but I wanna do some systems programming and wonder if haskell is the right tool. |
| 16:40:11 | <haskellbridge> | <sm> "as long as the sponsors and spare time volunteers work to keep old GHC versions and deps building on your platform".... |
| 16:41:26 | <sm> | tinjamin: got an example of the kind of systems programming you have in mind ? Rust is used in linux kernel these days and Zig is also a fun place to be |
| 16:43:39 | → | ski joins (~ski@ext-1-033.eduroam.chalmers.se) |
| 16:44:15 | <tinjamin> | sm: not in particular since I am a noob lol but I like writing shell scripts and want to write my own http-server with aspirations of learning OS stuff from Operating System Three Easy Pieces which is in C but i wanna do it in a more modern language |
| 16:44:28 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 16:45:17 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 16:45:27 | <tinjamin> | My gut tells me rust might be better and actually help get my hands dirty but haskell is so elegant and foreign |
| 16:45:30 | <sm> | cool. For shell scripting you just can't beat shell, it's designed for that. I recommend oil shell which will replace bash. |
| 16:45:51 | <sm> | for experimenting with a http server haskell is good, but go is also designed for that |
| 16:46:23 | <tinjamin> | yeah i talked to some of my folks at uni and the talk revolved around go vs rust |
| 16:47:59 | × | igemnace quits (~ian@user/igemnace) (Quit: WeeChat 4.2.1) |
| 16:48:32 | <sm> | write something small in all of them and see how it goes ? |
| 16:48:42 | <sm> | perhaps the same thing |
| 16:51:50 | <tinjamin> | hmm I think I am just not mature enough programming wise yet to see the benefits of haskell. |
| 16:53:46 | <sm> | people often say that knowing a little haskell helps them think/program more clearly in any language |
| 16:54:56 | × | danse-nr3 quits (~danse@151.43.209.161) (Read error: Connection reset by peer) |
| 16:55:49 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 16:56:05 | <sm> | that's true for me certainly. Haskell is perhaps the best place to learn the functional programming style |
| 16:56:09 | → | danse-nr3 joins (~danse@151.43.160.252) |
| 16:56:44 | × | euleritian quits (~euleritia@77.22.252.56) (Ping timeout: 268 seconds) |
| 16:57:18 | → | euleritian joins (~euleritia@dynamic-176-006-199-015.176.6.pool.telefonica.de) |
| 16:57:58 | × | Maxdamantus quits (~Maxdamant@user/maxdamantus) (Ping timeout: 268 seconds) |
| 16:58:40 | → | Maxdamantus joins (~Maxdamant@user/maxdamantus) |
| 17:01:11 | × | jjhoo quits (~jahakala@user/jjhoo) (Ping timeout: 264 seconds) |
| 17:03:57 | <kuribas> | tinjamin: haskell is quite far from system programming, as it tries to abstract away from the hardware. Still, it offers enough tools for allowing low level code. |
| 17:05:28 | <kuribas> | If "systems programming" means low level drivers, network protocols, or embedded hardware, then probably haskell is not a good choice. |
| 17:05:57 | <kuribas> | Though a lot of "embedded hardware" is powerful enough for haskell these days (raspberry pi's etc...) |
| 17:06:35 | × | enoq quits (~enoq@2a05:1141:1e6:3b00:c958:a45e:c4e0:3650) (Remote host closed the connection) |
| 17:06:35 | <EvanR> | garbage collector in your drivers would be "interesting" |
| 17:07:33 | → | ulthuan23456 joins (~ulthuan23@2a09:bac3:3116:191::28:90) |
| 17:10:01 | × | ulthuan23456 quits (~ulthuan23@2a09:bac3:3116:191::28:90) (Client Quit) |
| 17:10:23 | × | kaskal quits (~kaskal@2001:4bb8:2c3:39c1:ff3f:d58:4fd9:e10c) (Quit: ZNC - https://znc.in) |
| 17:10:31 | <geekosaur> | there's always https://github.com/dls/house |
| 17:10:37 | × | danse-nr3 quits (~danse@151.43.160.252) (Ping timeout: 264 seconds) |
| 17:11:28 | → | kaskal joins (~kaskal@2001:4bb8:2c3:39c1:ff3f:d58:4fd9:e10c) |
| 17:12:49 | → | jjhoo joins (jahakala@user/jjhoo) |
| 17:16:49 | × | machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 272 seconds) |
| 17:18:19 | × | jjhoo quits (jahakala@user/jjhoo) (Ping timeout: 268 seconds) |
| 17:18:33 | × | euleritian quits (~euleritia@dynamic-176-006-199-015.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 17:18:51 | → | euleritian joins (~euleritia@77.22.252.56) |
| 17:20:37 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 17:22:05 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 17:24:06 | × | kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection) |
| 17:24:54 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 255 seconds) |
| 17:27:34 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 268 seconds) |
| 17:28:14 | → | penteract joins (~penteract@cpc80271-blbn12-2-0-cust449.10-1.cable.virginm.net) |
| 17:29:16 | <mauke> | <EvanR> garbage collector in your drivers would be "interesting" <- that would rule out Go as well (re: <tinjamin> yeah i talked to some of my folks at uni and the talk revolved around go vs rust) |
| 17:31:00 | × | Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving) |
| 17:32:34 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 255 seconds) |
| 17:33:37 | <probie> | EvanR: Avoid garbage collection by just not allocating |
| 17:33:57 | <EvanR> | in haskell? I heard this can happen |
| 17:34:18 | <mauke> | avoid garbage collection by introducing space leaks |
| 17:34:22 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 17:35:29 | <EvanR> | each call into the driver spawns a process which never reclaims memory, and provably dies and completes mission before it runs out of memory xD |
| 17:39:55 | → | rvalue joins (~rvalue@user/rvalue) |
| 17:40:27 | <monochrom> | JHC didn't have garbage collection for a long time. >:D |
| 17:40:52 | <monochrom> | (That's right, it simply let space leak happen.) |
| 17:42:01 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 17:48:00 | → | tzh joins (~tzh@c-71-193-181-0.hsd1.or.comcast.net) |
| 17:52:41 | <EvanR> | move fast, brk instruction |
| 17:54:02 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 17:54:03 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 17:57:07 | <noctux> | where is the problem in gc-ing in kernel space? |
| 17:58:05 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 240 seconds) |
| 17:59:09 | <noctux> | I mean, at the end of the day, there is your allocator, and there are your kernel stacks and your globals. as long as you can identify all those, there shouldn't be to much difference between kernel and userspace probably? |
| 18:05:16 | × | penteract quits (~penteract@cpc80271-blbn12-2-0-cust449.10-1.cable.virginm.net) (Ping timeout: 250 seconds) |
| 18:09:36 | <geekosaur> | interrupt handlers and near-realtime-response drivers |
| 18:10:08 | <noctux> | so don't gc in time-sensitive codepatha |
| 18:10:20 | <noctux> | *codepaths |
| 18:10:28 | <geekosaur> | the former are a problem even in normal kernels, for example linux's network interrupt handlers keep around preallocated buffers |
| 18:11:11 | <noctux> | so do so with your gc as well? |
| 18:12:56 | <geekosaur> | the problem with this is your compiler needs to generate different code for those paths. ghc, for example, assumes allocation and gc is always cheap (which it usually is because of the nursery) |
| 18:13:03 | <noctux> | that's more of a latency (and consistency/synchronisation, in case of concurrent alloc in the handler) issue... not so much a fundamental problem |
| 18:15:01 | <noctux> | a, sure, and potentially you want to tune your gc a bit... there was a bit of research into realtime-compatible GCs from the real-time java crowd |
| 18:15:42 | <noctux> | (back when java was a thing) |
| 18:16:08 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 18:23:35 | × | son0p quits (~ff@167.0.172.211) (Ping timeout: 252 seconds) |
| 18:23:47 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 18:30:14 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 18:30:33 | <EvanR> | my desktop is running like windows 95, better open up the hood and tune my gc |
| 18:30:47 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 18:35:44 | × | synchromesh quits (~synchrome@2407:7000:aa2d:4e00:9cf7:efcb:5efd:a99) (Read error: Connection reset by peer) |
| 18:36:35 | <noctux> | :D |
| 18:36:57 | → | synchromesh joins (~synchrome@2407:7000:aa2d:4e00:9cf7:efcb:5efd:a99) |
| 18:37:01 | → | julie_pilgrim joins (~julie_pil@user/julie-pilgrim/x-1240752) |
| 18:37:40 | × | ski quits (~ski@ext-1-033.eduroam.chalmers.se) (Remote host closed the connection) |
| 18:40:02 | → | cfricke joins (~cfricke@user/cfricke) |
| 18:43:49 | → | ski joins (~ski@ext-1-033.eduroam.chalmers.se) |
| 18:52:45 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 18:54:26 | × | Taneb quits (~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0) (Quit: I seem to have stopped.) |
| 18:57:09 | → | Taneb joins (~Taneb@runciman.hacksoc.org) |
| 19:06:12 | × | julie_pilgrim quits (~julie_pil@user/julie-pilgrim/x-1240752) (Remote host closed the connection) |
| 19:07:55 | → | target_i joins (~target_i@217.175.14.39) |
| 19:11:08 | × | oo_miguel quits (~Thunderbi@78-11-181-16.static.ip.netia.com.pl) (Quit: oo_miguel) |
| 19:11:56 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 19:15:28 | → | derpyxdhs joins (~Thunderbi@user/derpyxdhs) |
| 19:17:32 | × | derpyxdhs quits (~Thunderbi@user/derpyxdhs) (Client Quit) |
| 19:19:48 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 19:21:35 | → | danse-nr3 joins (~danse@151.43.155.200) |
| 19:22:36 | × | gabriel_sevecek quits (~gabriel@188-167-229-200.dynamic.chello.sk) (Quit: WeeChat 4.1.1) |
| 19:24:14 | → | gabriel_sevecek joins (~gabriel@188-167-229-200.dynamic.chello.sk) |
| 19:24:44 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht) |
| 19:24:54 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 19:27:40 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 19:28:30 | <srk> | shapr: <3, finally got a bit unstuck \o/ |
| 19:32:39 | × | ski quits (~ski@ext-1-033.eduroam.chalmers.se) (Remote host closed the connection) |
| 19:32:48 | → | ski joins (~ski@ext-1-033.eduroam.chalmers.se) |
| 19:33:43 | × | dcoutts quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 260 seconds) |
| 19:35:02 | × | euleritian quits (~euleritia@77.22.252.56) (Read error: Connection reset by peer) |
| 19:35:22 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 19:37:14 | × | ulvarref` quits (~user@188.124.56.153) (Remote host closed the connection) |
| 19:52:23 | × | Vq quits (~vq@2001:2043:1c58:ea00:ca7f:54ff:fe6a:fd48) (Ping timeout: 260 seconds) |
| 19:54:07 | → | Vq joins (~vq@81-231-76-8-no600.tbcn.telia.com) |
| 19:54:23 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 19:55:03 | × | sam113101 quits (~sam@modemcable146.137-200-24.mc.videotron.ca) (Read error: Connection reset by peer) |
| 19:56:45 | → | sam113101 joins (~sam@modemcable146.137-200-24.mc.videotron.ca) |
| 19:58:49 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 255 seconds) |
| 19:59:28 | × | sam113101 quits (~sam@modemcable146.137-200-24.mc.videotron.ca) (Read error: Connection reset by peer) |
| 19:59:52 | → | sam113101 joins (~sam@modemcable146.137-200-24.mc.videotron.ca) |
| 20:00:55 | × | sam113101 quits (~sam@modemcable146.137-200-24.mc.videotron.ca) (Remote host closed the connection) |
| 20:01:23 | → | sam113101 joins (~sam@modemcable146.137-200-24.mc.videotron.ca) |
| 20:02:50 | × | sam113101 quits (~sam@modemcable146.137-200-24.mc.videotron.ca) (Read error: Connection reset by peer) |
| 20:03:11 | → | sam113101 joins (~sam@modemcable146.137-200-24.mc.videotron.ca) |
| 20:03:39 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 4.1.2) |
| 20:04:01 | × | sam113101 quits (~sam@modemcable146.137-200-24.mc.videotron.ca) (Read error: Connection reset by peer) |
| 20:04:25 | → | sam113101 joins (~sam@modemcable146.137-200-24.mc.videotron.ca) |
| 20:04:52 | × | sam113101 quits (~sam@modemcable146.137-200-24.mc.videotron.ca) (Remote host closed the connection) |
| 20:05:15 | → | sam113101 joins (~sam@modemcable146.137-200-24.mc.videotron.ca) |
| 20:06:43 | × | fendor quits (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) (Remote host closed the connection) |
| 20:15:20 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 20:15:40 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 20:20:54 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 20:25:15 | → | euphores joins (~SASL_euph@user/euphores) |
| 20:27:06 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 20:31:39 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 255 seconds) |
| 20:34:28 | → | son0p joins (~ff@167.0.172.211) |
| 20:38:26 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 20:42:59 | → | ft joins (~ft@p508db2e6.dip0.t-ipconnect.de) |
| 20:46:09 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 20:57:04 | × | danse-nr3 quits (~danse@151.43.155.200) (Read error: Connection reset by peer) |
| 20:57:39 | → | danse-nr3 joins (~danse@151.57.200.9) |
| 20:59:01 | <shapr> | ski: yay! |
| 20:59:17 | <shapr> | ski: what were you stuck on? |
| 20:59:26 | <shapr> | oops, misreply |
| 20:59:31 | <shapr> | srk: what were you stuck on? |
| 20:59:35 | shapr | facepalms |
| 20:59:58 | <mauke> | I don't know that combinator |
| 21:00:05 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 21:01:09 | → | califax joins (~califax@user/califx) |
| 21:01:45 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 21:08:11 | → | julie_pilgrim joins (~julie_pil@user/julie-pilgrim/x-1240752) |
| 21:14:44 | <shapr> | :-P |
| 21:15:21 | × | target_i quits (~target_i@217.175.14.39) (Quit: leaving) |
| 21:19:11 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:21:01 | × | phma quits (~phma@host-67-44-208-78.hnremote.net) (Read error: Connection reset by peer) |
| 21:22:25 | → | phma joins (phma@2001:5b0:211c:c1d8:e754:54f0:2658:655) |
| 21:23:34 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 21:27:11 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 21:28:11 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Remote host closed the connection) |
| 21:28:15 | → | gorignak joins (~gorignak@user/gorignak) |
| 21:28:44 | × | shapr quits (~user@c-24-218-186-89.hsd1.ma.comcast.net) (Remote host closed the connection) |
| 21:30:45 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 21:35:48 | → | euphores joins (~SASL_euph@user/euphores) |
| 21:36:29 | × | danse-nr3 quits (~danse@151.57.200.9) (Ping timeout: 272 seconds) |
| 21:37:10 | → | fen53 joins (~fen@84.68.80.95) |
| 21:37:54 | fen53 | is now known as fen_ |
| 21:38:10 | <fen_> | i can give a code example |
| 21:38:24 | <fen_> | its of the random numbers thing |
| 21:38:31 | <fen_> | global strict scope |
| 21:38:43 | <fen_> | which i want help a workaround with |
| 21:40:03 | <fen_> | https://paste.tomsmeding.com/Ty2UIMmo |
| 21:40:24 | × | euphores quits (~SASL_euph@user/euphores) (Client Quit) |
| 21:40:45 | <fen_> | newRough :: Parametric a init => Int -> [Double] -> init -> Rough a init |
| 21:41:02 | <fen_> | data Rough a init where |
| 21:41:03 | <fen_> | Rough :: Parametric a init |
| 21:41:03 | <fen_> | => (Seed,Length) |
| 21:41:04 | <fen_> | -> (Length,Length) |
| 21:41:04 | <fen_> | -> [[Double]] |
| 21:41:05 | <fen_> | -> [Double] |
| 21:41:05 | <fen_> | -> a |
| 21:41:06 | <fen_> | -> Rough a init |
| 21:41:22 | <fen_> | [[Double]] is the random numbers |
| 21:42:03 | → | euphores joins (~SASL_euph@user/euphores) |
| 21:42:47 | <fen_> | lengths pertain to the length of a random mask given from the seed |
| 21:43:19 | <[exa]> | fen_: please do not copypaste to here, it gets very ugly on cellphones etc. |
| 21:43:26 | <fen_> | erp sorry |
| 21:43:29 | <[exa]> | np |
| 21:43:32 | <fen_> | it reads ok on my screen |
| 21:43:53 | <fen_> | length of the parameters of the parametric object etc. |
| 21:44:27 | <EvanR> | @where paste |
| 21:44:27 | <lambdabot> | Help us help you: please paste full code, input and/or output at e.g. https://paste.tomsmeding.com |
| 21:44:47 | <fen_> | so there is no guarantee that these randoms are not recualculated in different values of this datatype |
| 21:45:04 | <[exa]> | fen_: where's the Parametric from? |
| 21:45:09 | → | miumiu joins (~miumiu@45-181-100-129.plugartelecom.net.br) |
| 21:45:10 | <fen_> | EvanR: the paste above is https://paste.tomsmeding.com/Ty2UIMmo |
| 21:46:03 | × | julie_pilgrim quits (~julie_pil@user/julie-pilgrim/x-1240752) (Remote host closed the connection) |
| 21:46:05 | × | miumiu quits (~miumiu@45-181-100-129.plugartelecom.net.br) (Client Quit) |
| 21:46:08 | <fen_> | parametric; https://paste.tomsmeding.com/tLezIM9t |
| 21:47:00 | <fen_> | support: https://paste.tomsmeding.com/EHQtfCha |
| 21:47:00 | → | miumiu joins (~miumiu@45-181-100-129.plugartelecom.net.br) |
| 21:47:10 | <fen_> | (that algo is nuts btw, never been checked!) |
| 21:47:31 | <fen_> | binary tree with a random hack to make it one item extendible |
| 21:47:56 | <fen_> | all the parametric objects get convinient random support coefs of any length |
| 21:48:11 | <fen_> | now, what i want to do, is ensure these random numbers are never recalculated |
| 21:48:29 | <fen_> | there is a slight issue with offsets in composite parametric objects... |
| 21:48:54 | × | miumiu quits (~miumiu@45-181-100-129.plugartelecom.net.br) (Client Quit) |
| 21:49:05 | <fen_> | so maybe it wants to have this handled specifically, so lists of parameteric objects have associated lists of random supports eg with different seeds |
| 21:49:27 | <EvanR> | to avoid recalculation there's memoization |
| 21:49:37 | <EvanR> | memocombinators? |
| 21:49:51 | <fen_> | im going to be using implicit params |
| 21:50:00 | <fen_> | they allow strict binding of local instances |
| 21:50:23 | <fen_> | and a semantic placeholder for strict variables under assumption of use of a strictly binding reflector |
| 21:50:26 | <fen_> | i want to write that |
| 21:50:37 | <[exa]> | fen_: so the overall goal of the thing is like, distributing the entropy around? |
| 21:50:56 | <fen_> | its basically wishing the random numbers could be declared at top level and be strict |
| 21:51:22 | <fen_> | they have to be evaluated and then strictly bound away from top level |
| 21:51:33 | <fen_> | so a local instance, or a regular variable |
| 21:51:50 | <fen_> | local instance here makes it apparent at type level |
| 21:51:50 | <[exa]> | oic, and ideally without pulling a monad through everything. |
| 21:52:07 | → | machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 21:52:10 | → | julie_pilgrim joins (~julie_pil@user/julie-pilgrim/x-1240752) |
| 21:52:17 | <fen_> | its a constraint, and yeah, other approaches to scoping would need a propegation structure which is likely monadic |
| 21:52:32 | <[exa]> | tbh I'm a bit lost in the code |
| 21:53:07 | <fen_> | can you get it to compile? |
| 21:53:18 | <[exa]> | cellphone :) |
| 21:53:28 | → | dcoutts joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 21:53:30 | <[exa]> | (man I wish I had ghci on the cellphone) |
| 21:53:58 | <fen_> | https://paste.tomsmeding.com/j4CWgC50 |
| 21:54:12 | <fen_> | thats my prolude module which youd need for complication for people on machines with compilers |
| 21:54:31 | <fen_> | basically the support algorithm implements a binary tree |
| 21:54:38 | <fen_> | you could just have regular coefs |
| 21:54:43 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 21:55:03 | <fen_> | but this way is good for learning, as it has extra variables dealing with hierarchical grouping |
| 21:55:10 | <fen_> | the n=2 case of the btree is the optimal |
| 21:55:21 | <fen_> | and has this weird hack to make it one object extensible |
| 21:55:28 | <fen_> | like a regular coefecient list is |
| 21:56:06 | <fen_> | you just grow this btree ass you keep adding support coefecients |
| 21:56:34 | <fen_> | can be ignored, can just consider the extensibility of a regular coefecient vector |
| 21:56:42 | <fen_> | these are coefs to random vectors |
| 21:56:47 | <fen_> | (at the leafs of the btree) |
| 21:56:56 | <[exa]> | aren't there skippable RNGs that kinda make sure you don't need the support tree here? |
| 21:57:15 | <fen_> | which are superposed to give any (but a specified) length of supported vector, then used to reparametrize the object |
| 21:57:23 | × | thegeekinside quits (~thegeekin@189.217.83.221) (Ping timeout: 272 seconds) |
| 21:57:36 | <fen_> | the rngs are these vectors that are random that can be precomputed |
| 21:57:48 | <fen_> | so they should be global |
| 21:57:56 | <fen_> | but also very much not being recomputed |
| 21:58:22 | <fen_> | these could appear at eveery one of a deep neuronal nets neurons as the encoding of a nonlinear parametric deep transfer object |
| 21:58:44 | <fen_> | fractal complexity does not lend well to not having memoised a huge common piece of data |
| 21:58:54 | → | thegeekinside joins (~thegeekin@189.217.83.221) |
| 21:59:00 | <EvanR> | sounds deep |
| 21:59:03 | <[exa]> | yap. |
| 21:59:05 | <EvanR> | ak chopra |
| 21:59:06 | <fen_> | true dat |
| 21:59:19 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 260 seconds) |
| 21:59:21 | <[exa]> | nvm guys have to sleep, good luck |
| 21:59:40 | <fen_> | chow |
| 22:00:11 | <fen_> | tbh i am lost in the code also |
| 22:00:26 | × | coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 22:00:35 | <fen_> | anyway. sorry i just had to clear up something for someone |
| 22:01:17 | <fen_> | so nrmally like at the neurons, you would have this rough object, with the random numbers there in the Rough datatype |
| 22:01:52 | <fen_> | which is really at risk of recomputation, esp, given that the different positions the rough objects appear at, might be of different sizes, and invoke different rng calculations |
| 22:02:22 | <fen_> | so it needs a standard approach, and i would like to (but am not sure how to) use implicit params for the strictness indication at type level |
| 22:02:43 | <fen_> | i wouldnt bring it to ask the comunity if it wasnt in this new idiom |
| 22:02:56 | <fen_> | which is kind of what i feel as though is worth asking for colaberation o |
| 22:03:14 | <fen_> | like "we" kind of need to know how to do this, so could do it together |
| 22:03:28 | <fen_> | given all the machinery for it and justification already exists |
| 22:03:36 | <fen_> | just a case opf putting together a code example |
| 22:04:18 | <fen_> | ... |
| 22:04:29 | <probie> | Why implicit params and not just something like the reader monad? |
| 22:04:45 | <fen_> | eg im looking for answers like "isnt what you need just a constraint in the datatype constructors signature?" |
| 22:05:20 | <fen_> | probie: compositionality algebra of the context being via constraints |
| 22:05:48 | <fen_> | and also that the iomplicit parameter is to be specifically used to annotate possible strictness |
| 22:05:52 | <fen_> | which it literally does |
| 22:06:02 | <fen_> | other constraints are sure not to be strict |
| 22:06:30 | <fen_> | arguments could be either, there is no different syntax |
| 22:07:17 | <fen_> | like what does the code doing this actually look like? |
| 22:07:47 | <fen_> | implicit params in GADT constructor signatures |
| 22:08:27 | <fen_> | with the existence of a strict reflection technique |
| 22:08:43 | <fen_> | which i think is just a double let binding |
| 22:08:56 | <fen_> | one for the !, one for the ? |
| 22:09:45 | <fen_> | (i was proposing a new constructor that merged the two `!?' such that certain strictness could be indicated using a form of implicit params) |
| 22:10:01 | <fen_> | and in order to return something |
| 22:10:15 | <fen_> | like, because it wants to be encapsulated in a function, so we seek a return type |
| 22:10:28 | <fen_> | this is an environment in which the reflected data can be used |
| 22:11:05 | <fen_> | which i think is a constraint continuation of the form ((? _ :: a => b) -> b) |
| 22:11:09 | <fen_> | this is what i have to go off |
| 22:11:42 | <fen_> | like, to use the datatype, the constraint has to be satisfied |
| 22:12:23 | <fen_> | so you need one of these environments to actually perform computations using that datatype when it accesses those variables |
| 22:12:44 | <fen_> | such an environment is normally constructed using ? in a let binding |
| 22:13:04 | <fen_> | but if that scope is to be returned, then something like a constrant continuation is required |
| 22:13:59 | <fen_> | ((? randomNumbers :: [[Double]] => Rough Object) -> Rough Object) |
| 22:14:34 | <fen_> | where data Rough has a constructor of type Rough :: ? randomNumbers :: [[Double]] => ... |
| 22:14:55 | <fen_> | iv never seen anyone use implicit params in a datatype |
| 22:15:45 | <fen_> | the syntax i propose would allow for datatype constructors to have signatures of the form Rough :: !? randomNumbers :: [[Double]] => ... |
| 22:17:16 | <fen_> | indicating the implicit params are strctly bound by a ! let binding, before being bound to implicit parameter scope by a ? let binding, overall returning an environment where the datatype can be used "by having had its construction completed" |
| 22:17:34 | <fen_> | which is a really strange notion, which constraints add to datatypes |
| 22:18:03 | <fen_> | that even a completed datatype might essentially still be missing arguments provided by the constraint |
| 22:19:12 | <fen_> | aka. provision of implicit parameters to the datatype constructor, requires handling of the scope in which these references are satisfiable |
| 22:19:47 | <fen_> | less so than with instances declared at top level which as an all encompasing scope |
| 22:20:19 | <fen_> | you just havent defined an instance yet and its essentially a type error in terms of missing top level global definitions |
| 22:21:20 | <fen_> | ie you would get a missing instance, having written the constraint properly, with the constraint at the function using the datatype having to subsume that of the datatypes used within the functions definition |
| 22:21:44 | <fen_> | but with it away from top level, these implicit parameters do not have such a global type error |
| 22:21:59 | <fen_> | and the handling of the restricted scope is required |
| 22:22:05 | × | a51 quits (a51@gateway/vpn/protonvpn/a51) (Quit: WeeChat 4.2.1) |
| 22:22:06 | <fen_> | its a new requirewment that appears |
| 22:22:35 | <fen_> | types containing local data, not mimicking a lack of top level strictness |
| 22:23:12 | <fen_> | such that to work with stricness at type level, we begin having to handle restricted scopes |
| 22:23:22 | <fen_> | with me so far? |
| 22:23:33 | <fen_> | im asking that we should together write such an example |
| 22:24:17 | <fen_> | can anyone understand about the constraints in the continuations and the restricted scope enough to write what i described? |
| 22:25:05 | → | yoo joins (~yo0O0o@104.28.194.104) |
| 22:28:42 | → | danse-nr3 joins (~danse@151.57.200.9) |
| 22:31:13 | × | julie_pilgrim quits (~julie_pil@user/julie-pilgrim/x-1240752) (Remote host closed the connection) |
| 22:31:27 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 22:32:25 | <geekosaur> | fen_, do you think you could not take over the channel? |
| 22:34:09 | <fen_> | is there a wrong answer to this? |
| 22:34:20 | <fen_> | appologies |
| 22:34:53 | <fen_> | ill just assume anyone capable would rather mod me |
| 22:35:33 | <fen_> | i have a language extension relavent theoretic development |
| 22:35:48 | <fen_> | i want a least working example as a comunity effort, hang me |
| 22:36:15 | <geekosaur> | IRC is not the place for extended, involved discussions like that. there is reddit, there is the discourse |
| 22:36:20 | <fen_> | i dont find it helpful when mods essentially preclude from the outcome |
| 22:36:30 | <fen_> | its not like im writing gibberish |
| 22:36:54 | <fen_> | its a place i can find people actually capable of things like comunity development |
| 22:37:06 | <fen_> | of the language. we have done this extensively over the years |
| 22:37:16 | <fen_> | your claims seem gripey |
| 22:37:22 | <c_wraith> | then read it as "you're probably not going to get engagement here if your idea doesn't fit in one or two lines" |
| 22:37:26 | <sm> | fen_ it's still preferred by everyone here not to see a wall of text. Try to wait and get a dialog going. You can always post longer writing on discourse or reddit and link it here. |
| 22:37:27 | <mauke> | <fen_> its not like im writing gibberish <- debatable |
| 22:37:32 | <sm> | Get along with folks here or you won't last |
| 22:37:49 | <fen_> | its a good proposal, it has reasonably interesting associated theoretical considerations, there has been discussion |
| 22:38:03 | × | michalz quits (~michalz@185.246.207.197) (Quit: ZNC 1.8.2 - https://znc.in) |
| 22:38:08 | <fen_> | sm: no, your being encouraged by a mod not to read |
| 22:38:10 | <sm> | I would be interested to read it as a single post somehwere suitable |
| 22:38:14 | × | yoo quits (~yo0O0o@104.28.194.104) (Ping timeout: 260 seconds) |
| 22:38:45 | <fen_> | mauke: not like that debate is as fruitfull as the non-giberish. its sound theory |
| 22:39:07 | <fen_> | sm: i dont have that capability. the mod attitude would prevent the material seeing the light of day |
| 22:39:16 | <mauke> | as someone said 10 hours ago, "you are talking by yourself. Maybe you want to write a book or an article instead" |
| 22:39:24 | <sm> | not interested in this argument, let's discuss haskell in a friendly way eh |
| 22:39:52 | <fen_> | you would prefer it was something you could say you had not seen, this is always the case of general attitudes of a censor. i actually study it btw now i work in a social media company, and im often put in mind of unhelpful modding in irc |
| 22:40:01 | × | machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 264 seconds) |
| 22:40:23 | <fen_> | basically as soon as a mod has to contend with a flood, then its a "yoursing your words again are we", which totally i agree, is a detraction |
| 22:40:54 | <mauke> | that's not what censorship is |
| 22:41:15 | <fen_> | mauke: this kind of cometary! where he is like, go write a book, or save it for your blog howard, wheree the intension is so they *dont* have to read it. its simply rude! |
| 22:41:17 | <geekosaur> | apparently we users of #haskell do not have the right to decide what is reasonable use of our channel? |
| 22:41:27 | <mauke> | fen_: wrong |
| 22:41:49 | <mauke> | demanding your words to be read, no matter what, is rude |
| 22:42:04 | <fen_> | im saying that its always an option to mod rather than engaging, but half the best users are mods, and they are just sick of seeing words, which is such an unhelpful attitude fort them to promote |
| 22:42:37 | <fen_> | my bad for using too many words sure, but the save it for your blog comments are really detrimental to how people end up engaging |
| 22:42:49 | <fen_> | we are fine to talk about moding, but not the topic at hand |
| 22:43:06 | <fen_> | in this case i think i have a reasonable excuse. its important to haskell |
| 22:43:14 | <mauke> | there is no "topic at hand" |
| 22:43:18 | <haskellbridge> | <sm> fen_: there's an art and etiquette to getting a conversation going here. |
| 22:43:19 | <fen_> | more than your desire not to have that be the case... |
| 22:43:43 | <fen_> | mauke: look at this interjection!! now i wasnt even saying *anything*. absurdity. no place for these digressions really |
| 22:43:56 | <mauke> | you've been talking non-stop |
| 22:43:58 | <fen_> | common enough, but super counterproductive |
| 22:44:36 | <haskellbridge> | <sm> would you like to move on and re-introduce your topic in a sentence or two ? |
| 22:45:10 | <fen_> | but if instead of interjecting, with like, ok, i see what your getting at, hows about this. if its "ok just stop writing now" this puts a total kybosh on proceedings, and disencourages pottential engagement, so i think its really not great that the mods have to do this because of my flood, which i appologise for |
| 22:45:19 | <fen_> | sm: thanks |
| 22:45:19 | × | synchromesh quits (~synchrome@2407:7000:aa2d:4e00:9cf7:efcb:5efd:a99) (Read error: Connection reset by peer) |
| 22:45:32 | <haskellbridge> | <sm> there's nothing wrong with rambling on a bit but don't attack people when they ask you to do it differently |
| 22:45:41 | <haskellbridge> | <sm> we mean no harm |
| 22:45:45 | <fen_> | i was describing a situation where a language extension building on implicit parameters allows consideration of strictness at type level |
| 22:45:51 | → | segfaultfizzbuzz joins (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 22:46:20 | → | masterbuilder joins (~quassel@user/masterbuilder) |
| 22:46:22 | <fen_> | !? mimicking ? in basically every way, but also appearing like a bang patern in the binding of the implicit parameter |
| 22:46:41 | <mauke> | what is your goal? |
| 22:46:50 | → | synchromesh joins (~synchrome@2407:7000:aa2d:4e00:9cf7:efcb:5efd:a99) |
| 22:46:57 | <fen_> | and then how to give this in a least working example using the existing but more clunky two let bindings for the strictness and implicitness seperately |
| 22:46:59 | <segfaultfizzbuzz> | foo : Int -> ???? i want the type of foo 101 to be Int and foo 102 to be String ,... can that be done? |
| 22:47:23 | <mauke> | segfaultfizzbuzz: I don't think so |
| 22:47:31 | × | tomsmeding quits (~tomsmedin@2a01:4f8:c0c:5e5e::2) (Quit: ZNC 1.8.2 - https://znc.in) |
| 22:47:44 | <ncf> | if you can tolerate the type of both 101 and 102 being Either Int String, then yes. otherwise, it's called dependent types |
| 22:47:44 | <fen_> | mauke: a working example demonstraiting both the double let binding, handling of the scope resulting, such as with implicit parameter constraint continuations |
| 22:48:04 | → | tomsmeding joins (~tomsmedin@static.21.109.88.23.clients.your-server.de) |
| 22:48:16 | <int-e> | segfaultfizzbuzz: The basic answer is no; ???? needs to be a known type. It's quite fundamental to the type system. |
| 22:48:22 | <segfaultfizzbuzz> | right so the type must be known at compile time |
| 22:48:28 | <mauke> | fen_: then what do you need us for? |
| 22:48:38 | <fen_> | seg: you can use big eithers |
| 22:48:49 | <segfaultfizzbuzz> | functions have static types in other words |
| 22:48:57 | <fen_> | mauke: to write the example |
| 22:49:09 | <fen_> | or talk about it if you need me to write it, or however that works |
| 22:49:29 | <fen_> | in the first instance just to get what im saying and why bothering to do this is worth doing |
| 22:49:34 | <mauke> | what is my motivation for writing code for you? |
| 22:49:37 | <int-e> | segfaultfizzbuzz: The usual thing people do is to use a sum type like Either Int String, as ncf mentioned. Or more elaborate things involving existential types and type classes (notably the Typeable class) |
| 22:49:52 | <segfaultfizzbuzz> | right but the sum type is statically known |
| 22:49:55 | <fen_> | like, in possible leadup to any !? olanguage proposal, which again, would require someone that isnt me to do it |
| 22:50:40 | <fen_> | mauke: as part of the haskell comunity, you might be interested in the implications. certainly from my perspective i need to engage other users if a language extension were to result |
| 22:51:25 | <fen_> | i think that in the position of having developed the theory, and being in a position to engage the comunity, that the colaberation to construct the least working demonstrative example is a good goal |
| 22:51:32 | <mauke> | I have no idea how to write a language extension |
| 22:52:06 | <fen_> | me neither! bt someone here does, and if we can get it to work using the existing syntax, this pesky requirement to use 2 let bindings, and also do the scope ahndling |
| 22:52:06 | <mauke> | so if your working example requires a language extension, your target audience is probably pretty small |
| 22:52:38 | <fen_> | nono, the motivating example for the language extension just uses implict parameters and bangpatterns seperately |
| 22:52:44 | <fen_> | the extension combines those |
| 22:53:12 | <fen_> | and it sets up this formalism of scope handling |
| 22:53:20 | <fen_> | which i think is what i want input on |
| 22:53:29 | <fen_> | i kind of cant call the shots on how we do that |
| 22:53:35 | → | yoo joins (~yo0O0o@104.28.194.105) |
| 22:53:45 | <fen_> | maybe people dont like constraint continuations and can think of a better way for example |
| 22:54:04 | <haskellbridge> | <sm> fen_: I for one don't see your idea clearly. A mini proposal, with examples/mockups etc., will make this clear to more of us and attract more feedback. |
| 22:54:13 | × | danse-nr3 quits (~danse@151.57.200.9) (Ping timeout: 246 seconds) |
| 22:54:24 | × | acidjnk quits (~acidjnk@p200300d6e737e723f1d9672538a89ef2.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 22:54:33 | <fen_> | we have to bind using let, and return a type that serves as a context in which a constraint is satisfied |
| 22:54:51 | <fen_> | previously i have done this using constraint continuations, but this is complicated and might not be the best way to introduce it |
| 22:55:18 | <fen_> | sm: whats unclear? |
| 22:55:29 | <haskellbridge> | <sm> your proposal |
| 22:55:35 | <fen_> | this is how we get some idea about strictness at type level using existing machinery |
| 22:55:41 | <fen_> | the proposal strengthens that |
| 22:56:19 | <fen_> | implicit parameters are not instantiated at top level and so "might be strict" as indicated by a ? in a constraint |
| 22:57:04 | <fen_> | the proposal would alow use of !? instead, also indicating not just "maybe strictness" (unlike, certainly not strict of other constraints, instantiated at top level) but actual strictness |
| 22:57:38 | <haskellbridge> | <sm> I have things to do, so I don't want to work hard to understand your idea from a stream of comments. It needs a proper description. |
| 22:57:40 | <fen_> | the idea of the working example hahaviving to cocontetwith hohow this sc is handled is what im coconceceed about |
| 22:57:47 | <fen_> | sorry my keyboard is wireless |
| 22:57:55 | <haskellbridge> | <sm> maybe someone else is getting it though. Good luck. |
| 22:58:07 | <int-e> | segfaultfizzbuzz: Maybe it's worth pointing out that GHC erases type information... the program that runs only has values, without knowing their types. Values are usually pointers... and code that takes such a pointer will just assume that the value has the right type. (In fact this is crucial for being able to pass values on without evaluating them, as required for lazy evaluation.) |
| 22:58:23 | <segfaultfizzbuzz> | interesting |
| 22:58:27 | <fen_> | certainly i have described that adequately |
| 22:59:24 | <segfaultfizzbuzz> | is there a "systems" meaning of type then? like, if i have a pointer and i know its type, then i can index into it or something? |
| 22:59:54 | <fen_> | sm: do you understand how using ? at type level indicated information about pottential strictness, as opposed to regular constraints, by virtue of the local instantiation allowing for a strict variable to be reflected, which is impossible as you cant use bang patterns in class instances, to do in the normal top level scope. and how this indicates |
| 22:59:55 | <fen_> | we have scope handling considerations that result |
| 23:01:05 | <fen_> | you get how this handling localness of instance gives rise to these considerations of strictness that motivate strengthening ? to !? |
| 23:01:10 | <fen_> | and then you get the proposal |
| 23:01:23 | <fen_> | and why i want to see these local scopes in action in an example |
| 23:01:33 | <fen_> | does anyone actually want to help me write it? |
| 23:02:56 | <fen_> | like, possibly, depending on if constraint continuations are the best way to do this, there could be a syntax for it also? |
| 23:03:10 | <fen_> | i cant really understand it enough at that point |
| 23:03:31 | <fen_> | im not used to constraint continuations, and cant even work with them enough to write the example |
| 23:03:41 | <fen_> | i guess thats really what im needing help with |
| 23:04:00 | <fen_> | other people here are much more experienced using continuations |
| 23:04:45 | <fen_> | the stumbling block im having is that constraint continuations are the only way i know how to do this handling of local scope, and i dont know how to use them properly to write it |
| 23:05:13 | <fen_> | maybe if someone that could understand what the constraint continuation was doing there, could propose an alternative that i could actually work with# |
| 23:06:10 | <mauke> | I'm not convinced this actually means anything |
| 23:06:19 | <fen_> | f g x = let !y = g x in let ?z = y in ... return the continuation... |
| 23:06:37 | <fen_> | mauke: im not convinced your not generating averse commentary |
| 23:06:45 | <mauke> | correct |
| 23:06:59 | <fen_> | confirmed |
| 23:07:06 | <mauke> | the alternative is silence |
| 23:07:23 | <fen_> | how do you work with continuations normally, like how do you return one? |
| 23:07:40 | <mauke> | what do you mean by continuations? |
| 23:07:51 | <fen_> | (a->b)->b |
| 23:07:56 | <fen_> | is a continuation which encodes a |
| 23:08:30 | <fen_> | ou need an a to make a b so you must somehow have an a if you can make a b from a function making a from b |
| 23:08:36 | <fen_> | b from a* |
| 23:08:44 | <mauke> | that's the type of a function, which is a value, which is returned like any other value. ? |
| 23:08:58 | <fen_> | i mean, how do you make that? |
| 23:09:19 | <mauke> | are you asking how to write functions in haskell? |
| 23:09:20 | <fen_> | f g x = let !y = g x in let ?z = y in \fz -> fz z |
| 23:09:42 | <fen_> | % :t \g x = let !y = g x in let ?z = y in \fz -> fz z |
| 23:09:42 | <yahb2> | <interactive>:1:6: error: parse error on input ‘=’ |
| 23:09:51 | <mauke> | -> |
| 23:09:52 | <fen_> | % :t \g x -> let !y = g x in let ?z = y in \fz -> fz z |
| 23:09:52 | <yahb2> | <interactive>:1:29: error: parse error on input ‘?’ |
| 23:10:06 | <fen_> | % :t \g x -> let !y = g x in let !z = y in \fz -> fz z |
| 23:10:06 | <yahb2> | \g x -> let !y = g x in let !z = y in \fz -> fz z ; :: forall {p} {t1} {t2}. (p -> t1) -> p -> (t1 -> t2) -> t2 |
| 23:10:26 | × | sudden quits (~cat@user/sudden) (Ping timeout: 268 seconds) |
| 23:10:41 | <fen_> | ((t1 -> t2) -> t2) is the returned constraint continuation |
| 23:10:50 | <fen_> | how do you get it to turn on implicit params? |
| 23:11:22 | <fen_> | % -XImplicitParams |
| 23:11:22 | <yahb2> | <interactive>:223:2: error: ; • Data constructor not in scope: XImplicitParams ; • Perhaps you meant one of these: ; ‘ImplicitParams’ (imported from Language.Haskell.TH), ; ... |
| 23:11:40 | <mauke> | % :set -XImplicitParams |
| 23:11:40 | <yahb2> | <no output> |
| 23:11:47 | <fen_> | % :t \g x = let !y = g x in let ?z = y in \fz -> fz z |
| 23:11:47 | <yahb2> | <interactive>:1:6: error: parse error on input ‘=’ |
| 23:11:52 | <fen_> | % :t \g x -> let !y = g x in let ?z = y in \fz -> fz z |
| 23:11:53 | <yahb2> | <interactive>:1:49: error: Variable not in scope: z |
| 23:12:12 | <fen_> | argh! |
| 23:12:22 | <mauke> | % :t \g x -> let !y = g x in let ?z = y in \fz -> fz ?z |
| 23:12:22 | <yahb2> | \g x -> let !y = g x in let ?z = y in \fz -> fz ?z ; :: forall {p} {t1} {t2}. (p -> t1) -> p -> (t1 -> t2) -> t2 |
| 23:12:44 | <fen_> | you cant even capture the let bound variable as a returned output |
| 23:12:51 | <fen_> | since it cant appear at term level after reflection |
| 23:13:26 | <fen_> | % :t \g x -> let !y = g x in let ?z = y in \(fz :: ?z -> a) -> fz |
| 23:13:26 | <yahb2> | <interactive>:1:50: error: parse error on input ‘->’ |
| 23:13:46 | <fen_> | % :t \g x -> let !y = g x in let ?z = y in \(fz :: ?z => a) -> fz |
| 23:13:46 | <yahb2> | <interactive>:1:50: error: parse error on input ‘=>’ |
| 23:13:47 | × | yoo quits (~yo0O0o@104.28.194.105) (Ping timeout: 264 seconds) |
| 23:13:55 | <fen_> | fucks sake |
| 23:14:09 | <fen_> | that would have been it |
| 23:15:57 | <mauke> | % :t \g x -> \fz -> fz ?z |
| 23:15:57 | <yahb2> | \g x -> \fz -> fz ?z ; :: forall {t1} {p1} {p2} {t2}. ; (?z::t1) => ; p1 -> p2 -> (t1 -> t2) -> t2 |
| 23:16:34 | <fen_> | % :t ((\g x -> let !y = g x in let ?z = y in fz -> fz) :: (a->b) -> a -> ((?z::b=>c)->c)) |
| 23:16:34 | <yahb2> | <interactive>:1:76: error: parse error on input ‘=>’ |
| 23:16:55 | <fen_> | hmm, that might just be yahb |
| 23:17:35 | <geekosaur> | if yahb doesn't like it then ghci doesn't like it |
| 23:17:55 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 23:22:00 | → | yoo joins (~yo0O0o@104.28.194.105) |
| 23:22:05 | <geekosaur> | pretty sure you need a "forall" (or the implicit "forall" at the start of a type) to introduce a constraint |
| 23:22:31 | <fen_> | f g x = (let !y = g x in let ?z = y in \fz -> fz) :: (a->b) -> a ->((?z::b=>c)->c) |
| 23:22:36 | <fen_> | does not work |
| 23:22:57 | <mauke> | if you intend ?z to stay open in the result, why are you binding it? |
| 23:23:11 | <fen_> | the place its used |
| 23:23:16 | <fen_> | its not with it defined |
| 23:23:22 | <mauke> | huh? |
| 23:23:25 | <fen_> | its usable if it can be provided |
| 23:23:44 | <fen_> | the user writing a function awaits its arguments creation and does say nothing about its existence |
| 23:24:18 | <fen_> | z does get used in the eval of fz btw |
| 23:24:28 | <fen_> | thats why im trying to add this type sig |
| 23:24:42 | <fen_> | it doesnt like constraints at lambdas apparently |
| 23:24:53 | <fen_> | which is just great since these continuations everywhere with constraints |
| 23:25:38 | → | sudden joins (~cat@user/sudden) |
| 23:25:49 | <mauke> | none of that makes any sense to me |
| 23:26:09 | <mauke> | % :t ?x |
| 23:26:09 | <yahb2> | ?x :: forall {t}. (?x::t) => t |
| 23:26:13 | → | mud joins (~mud@user/kadoban) |
| 23:26:20 | <mauke> | here ?x is open, so it appears as a constraint in the type signature |
| 23:26:29 | <mauke> | % :t let ?x = 42 in ?x |
| 23:26:29 | <yahb2> | let ?x = 42 in ?x :: forall {p}. Num p => p |
| 23:26:42 | <fen_> | right, the place we use the variable has it open, like a function argument, thats what i was saying |
| 23:26:52 | <mauke> | here ?x is bound internally, so it doesn't show up in the type |
| 23:27:08 | <fen_> | we want to return a place where the bound implicit param can be used |
| 23:27:24 | <fen_> | (?z::b=>c)->c |
| 23:27:26 | <mauke> | in your code you bind ?z, but you also want it to appear in the type somehow? |
| 23:27:34 | <fen_> | it has to |
| 23:27:40 | <fen_> | its not an argument to fz |
| 23:27:44 | <fen_> | its an implicit param |
| 23:27:48 | <mauke> | ? |
| 23:27:53 | <fen_> | the type of fz has to read; |
| 23:28:07 | × | yoo quits (~yo0O0o@104.28.194.105) (Ping timeout: 256 seconds) |
| 23:28:08 | <fen_> | fz :: (?z::b=>c)->c |
| 23:28:17 | <mauke> | that's not a type |
| 23:28:30 | <fen_> | sure it is |
| 23:28:42 | <mauke> | % :t undefined :: (?z::b=>c)->c |
| 23:28:42 | <yahb2> | <interactive>:1:20: error: parse error on input ‘=>’ |
| 23:28:54 | <fen_> | yeah i know yahb doesnt like it |
| 23:29:01 | <mauke> | because it's a syntax error |
| 23:29:08 | <fen_> | we wouldnt have gotten very far with constraint continuations if you couldnt write that |
| 23:29:19 | <mauke> | what, syntax errors? |
| 23:29:40 | <fen_> | honestly it worked we did huge amounts... theres pastes that went down with the old pastebin |
| 23:30:03 | <mauke> | % :t undefined :: (?z :: b) => (b -> c) -> c |
| 23:30:03 | <yahb2> | undefined :: (?z :: b) => (b -> c) -> c ; :: forall b c. (?z::b) => (b -> c) -> c |
| 23:30:27 | <mauke> | % :t ($ ?z) |
| 23:30:27 | <yahb2> | ($ ?z) :: forall {a} {b}. (?z::a) => (a -> b) -> b |
| 23:30:40 | <fen_> | this is no good |
| 23:30:46 | <fen_> | a is not a term level argument |
| 23:31:20 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 23:31:42 | <fen_> | % :t undefined :: (forall a b. Bool a => b) |
| 23:31:42 | <yahb2> | <interactive>:1:27: error: ; • Expected kind ‘k0 -> Constraint’, but ‘Bool’ has kind ‘*’ ; • In an expression type signature: (forall a b. Bool a => b) ; In the expression: undefined ... |
| 23:31:52 | <fen_> | % :t undefined :: (forall a b. Either a => b) |
| 23:31:52 | <yahb2> | <interactive>:1:27: error: ; • Expecting one more argument to ‘Either a’ ; Expected a constraint, but ‘Either a’ has kind ‘* -> *’ ; • In an expression type signature: (forall a b. Ei... |
| 23:32:06 | <fen_> | % :t undefined :: (forall a b. Ord a => b) |
| 23:32:06 | <yahb2> | <interactive>:1:14: error: ; • Could not deduce (Ord a0) ; arising from a type ambiguity check for ; an expression type signature ; from the context: Ord a ; bound... |
| 23:32:13 | × | liskin quits (~liskin@xmonad/liskin) (Ping timeout: 264 seconds) |
| 23:32:40 | <fen_> | % :t undefined :: forall a. Ord a => (forall b. Ord a => b) |
| 23:32:40 | <yahb2> | <interactive>:1:14: error: ; • Could not deduce (Ord a0) ; arising from a type ambiguity check for ; an expression type signature ; from the context: Ord a ; bound... |
| 23:32:52 | <fen_> | what a load of shit |
| 23:34:00 | <fen_> | can we use dictionaries? |
| 23:34:34 | <fen_> | https://kseo.github.io/posts/2017-02-06-reified-dictionaries.html |
| 23:36:49 | <fen_> | % data D a b where D :: ?z::a => b -> D a b |
| 23:36:49 | <yahb2> | <interactive>:265:29: error: parse error on input ‘=>’ |
| 23:37:05 | <fen_> | % data D a b where D :: (?z::a) => b -> D a b |
| 23:37:05 | <yahb2> | <no output> |
| 23:38:17 | <fen_> | % :t \g x -> let !y = g x in let ?z = y in \(fz :: (?z::b) => a) -> fz |
| 23:38:17 | <yahb2> | <interactive>:1:39: error: ; • Couldn't match expected type ‘p1’ ; with actual type ‘((?z::t) => a) -> a’ ; Cannot equate type variable ‘p1’ ; with a type involvin... |
| 23:39:35 | <fen_> | % :t ((\g x -> let !y = g x in let ?z = y in fz -> fz) :: (a->b) -> a -> (((?z::b)=>c)->c)) |
| 23:39:35 | <yahb2> | <interactive>:1:3: error: ; View pattern in expression context: ; \ g x -> let !y = ... in let ?z = y in fz -> fz |
| 23:40:06 | <fen_> | i dont know what its complaining about now |
| 23:40:34 | → | liskin joins (~liskin@xmonad/liskin) |
| 23:40:54 | <fen_> | % :t ((\g x -> let !y = g x in let ?z = y in D) |
| 23:40:54 | <yahb2> | <interactive>:1:43: error: ; parse error (possibly incorrect indentation or mismatched brackets) |
| 23:41:02 | <fen_> | % :t (\g x -> let !y = g x in let ?z = y in D) |
| 23:41:02 | <yahb2> | (\g x -> let !y = g x in let ?z = y in D) ; :: forall {p} {a} {b}. (p -> a) -> p -> b -> D a b |
| 23:41:25 | <fen_> | huh, it loses track of the implict parameter constrint because of the dictionary |
| 23:41:30 | × | Raito_Bezarius quits (~Raito@wireguard/tunneler/raito-bezarius) (Read error: Connection reset by peer) |
| 23:42:03 | <fen_> | but presumably that dictionary now contains the correctly strictly bound reflected data |
| 23:42:17 | <fen_> | so it looks like this double let binding appears in smart constructors for now |
| 23:42:29 | → | Raito_Bezarius joins (~Raito@wireguard/tunneler/raito-bezarius) |
| 23:42:31 | <fen_> | of weird implicit dictionary datatype entries |
| 23:42:36 | <fen_> | whew, this was a slog |
| 23:42:42 | <fen_> | thanks for everyones patience |
| 23:43:08 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 23:43:27 | <fen_> | annoyingly though, this means there are many pottential different versions |
| 23:43:38 | <fen_> | the scope itself would restrict that to one |
| 23:44:11 | <fen_> | like, constructors are the worst place to put them! |
| 23:44:21 | <fen_> | if you want everything constructed to use the same data |
| 23:44:53 | <fen_> | so suggest making the constructor take a strict implicit dictionary |
| 23:45:10 | <fen_> | that way this can be passed around to all the constructors |
| 23:45:22 | <fen_> | unsuring the universal computed data is already evaluated |
| 23:47:00 | <fen_> | ie rather than making the copnstructor implicity constrained |
| 23:47:24 | <fen_> | you just have a datatype entry which is a strictly constructed implicit dictionary |
| 23:47:29 | <fen_> | im proud of that |
| 23:48:05 | <fen_> | thanks for the help yo, there is no way i could have imagined that on my own |
| 23:48:18 | <fen_> | i swear. sorry i consist of a deluge |
| 23:48:50 | <fen_> | anyway, bring on the !? extension |
| 23:50:28 | → | yoo joins (~yo0O0o@104.28.194.104) |
| 23:53:07 | × | mmhat quits (~mmh@p200300f1c70b44daee086bfffe095315.dip0.t-ipconnect.de) (Quit: WeeChat 4.2.1) |
All times are in UTC on 2024-02-20.