2023-12-11 00:04:01 +0100 | <jackdk> | I don't know about cabal but I believe that the linker must be invoked with all the necessary `-l` arguments. So I would expect a tool like cabal to have to propagate them to whatever ends up actually calling the linker |
2023-12-11 00:04:17 +0100 | urdh | (~urdh@user/urdh) (Ping timeout: 256 seconds) |
2023-12-11 00:05:55 +0100 | aztex | (~aztex@178.197.239.241) |
2023-12-11 00:06:28 +0100 | <aztex> | Hey I have a Haskell project and I would like to trace the function calls that are made |
2023-12-11 00:06:45 +0100 | <aztex> | could you point me to some documentation on this |
2023-12-11 00:07:01 +0100 | <EvanR> | you can use Debug.Trace pretty easily to trace what expressions are evaluated |
2023-12-11 00:07:22 +0100 | <aztex> | I am thinking about runtime tracing |
2023-12-11 00:07:25 +0100 | <EvanR> | me too |
2023-12-11 00:07:28 +0100 | <idgaen> | Hecate: debian shipped their haskell libraries with .a (and not .so) |
2023-12-11 00:07:40 +0100 | <aztex> | where the programmer doesn't need to manually call "trace" |
2023-12-11 00:08:05 +0100 | <aztex> | I think with Debug.Trace the programmer has to annotate the information that they are tracing |
2023-12-11 00:08:23 +0100 | <EvanR> | yes it prints something out what a selected expression is evaluated |
2023-12-11 00:08:24 +0100 | <aztex> | what I am wondering is whether the RTS has some information on the function calls being made |
2023-12-11 00:08:27 +0100 | <EvanR> | when* |
2023-12-11 00:08:40 +0100 | <aztex> | like some kind of profiling |
2023-12-11 00:09:13 +0100 | <monochrom> | Well then you read the GHC User's Guide for its debugger. |
2023-12-11 00:09:47 +0100 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
2023-12-11 00:09:52 +0100 | <haskellbridge> | 12<Celestial> how is trace implemented? Is it just an `unsafePerformIO . putStrLn`? |
2023-12-11 00:10:22 +0100 | <monochrom> | Yeah. In fact it calls a C function, so as not to disturb RTS's stdout and stderr. :) |
2023-12-11 00:10:48 +0100 | <aztex> | https://hackage.haskell.org/package/base-4.19.0.0/docs/src/Debug.Trace.html#trace |
2023-12-11 00:10:58 +0100 | <EvanR> | unsafePerformIO . debugBelch xD |
2023-12-11 00:13:23 +0100 | aztex | (~aztex@178.197.239.241) (Quit: Client closed) |
2023-12-11 00:14:27 +0100 | nate4 | (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
2023-12-11 00:16:16 +0100 | <idgaen> | Oh! I'm wrong, in debian there is also .so files. |
2023-12-11 00:17:59 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
2023-12-11 00:18:22 +0100 | acidjnk_new | (~acidjnk@p200300d6e72b93299103c78233b0ca81.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
2023-12-11 00:19:28 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-12-11 00:19:58 +0100 | nate4 | (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 255 seconds) |
2023-12-11 00:21:09 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d128:ce35:54e1:65e2) (Remote host closed the connection) |
2023-12-11 00:24:54 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) (Quit: peterbecich) |
2023-12-11 00:25:12 +0100 | idgaen | (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.1.1) |
2023-12-11 00:25:34 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) |
2023-12-11 00:27:34 +0100 | <tri> | hi folks, * -> * is considered a higher-kinded type right? And iirc, it's called first-order type |
2023-12-11 00:27:53 +0100 | <dibblego> | it's the notation of the type of a higher-kinded type |
2023-12-11 00:29:08 +0100 | <tri> | so Person a = Person a is a higher kinded type |
2023-12-11 00:29:40 +0100 | <tri> | so then, F# and C# do have HKT with generic, just that they stop at the first-order type |
2023-12-11 00:30:22 +0100 | <dibblego> | No. |
2023-12-11 00:30:30 +0100 | <dibblego> | the type of Person is * -> * |
2023-12-11 00:30:41 +0100 | <dibblego> | also called "the kind of Person" |
2023-12-11 00:30:54 +0100 | <dibblego> | the kind of Maybe is * -> * |
2023-12-11 00:31:02 +0100 | <dibblego> | you could find this out in ghci with :kind Maybe |
2023-12-11 00:31:28 +0100 | <tri> | right, but didn't you just said it's the notation of the type of a HKT? |
2023-12-11 00:31:30 +0100 | <geekosaur> | a higher-kinded type is something like `data Foo f = Foo (f Int)`, which means `f` has kind * -> * |
2023-12-11 00:31:49 +0100 | <dibblego> | yes, * -> * will be the result, it is notating the kind of Maybe back to you |
2023-12-11 00:32:22 +0100 | <dibblego> | here is another example: https://i.imgur.com/I0XFRWf.png |
2023-12-11 00:33:37 +0100 | <tri> | dibblego: i understand the kind of Maybe and Person is * -> * |
2023-12-11 00:33:47 +0100 | <tri> | but isn't * -> * HKT? |
2023-12-11 00:34:33 +0100 | <dibblego> | not exactly, since I could say, write the Maybe type in C#, and it would have that kind, but that is not to say C# permits HKT |
2023-12-11 00:34:37 +0100 | <tri> | geekosaur: sorry that just went over my head |
2023-12-11 00:35:01 +0100 | <dibblego> | @type \a b -> const a <$> b |
2023-12-11 00:35:02 +0100 | <lambdabot> | Functor f => b1 -> f b2 -> f b1 |
2023-12-11 00:35:10 +0100 | <tri> | geekosaur: i understand your example, but at the same time kinda confused as i have never seen it before |
2023-12-11 00:35:10 +0100 | <dibblego> | I cannot write the type of this function in C# |
2023-12-11 00:35:10 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
2023-12-11 00:35:14 +0100 | <dibblego> | it does not have HKT |
2023-12-11 00:37:26 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 245 seconds) |
2023-12-11 00:38:13 +0100 | <tri> | dibblego: yea that example just went over my head. I know const drop the second argument and return the first one. But you applied 3 args there, and the fact that you used fmap as a second arg just blew my mind |
2023-12-11 00:38:34 +0100 | <tri> | welp, i will just re-read HKT again |
2023-12-11 00:38:46 +0100 | [_] | (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 256 seconds) |
2023-12-11 00:38:52 +0100 | <dibblego> | I don't have a C# compiler handy, but what is the type of this expression? (a, b) => from _ <- b; select a; |
2023-12-11 00:39:10 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3140-cd78-e0d9-a0e2-1a64-1fd2.rev.sfr.net) (Ping timeout: 250 seconds) |
2023-12-11 00:39:45 +0100 | <tri> | i dont think from _ <-b is a valid c# syntax, what are you trying to do there? |
2023-12-11 00:39:55 +0100 | <dibblego> | yeah it is |
2023-12-11 00:40:06 +0100 | <dibblego> | (a, b) => b.Select(_ => a); |
2023-12-11 00:40:07 +0100 | <tri> | is that linq? i never use linq sql like that |
2023-12-11 00:40:09 +0100 | <dibblego> | same thing ^^ |
2023-12-11 00:40:09 +0100 | <tri> | oh ok |
2023-12-11 00:40:21 +0100 | <dibblego> | what is its type? |
2023-12-11 00:40:23 +0100 | <tri> | yea sorry never write linq that way in my life, ok let me read that again |
2023-12-11 00:40:45 +0100 | <tri> | so b must be an IEnumerable |
2023-12-11 00:40:50 +0100 | <dibblego> | must it? |
2023-12-11 00:40:55 +0100 | <tri> | cuz of Select |
2023-12-11 00:41:05 +0100 | <tri> | and a could be anythign |
2023-12-11 00:41:08 +0100 | <dibblego> | what about the other things that have Select, but are not IEnumerable? |
2023-12-11 00:41:25 +0100 | <tri> | hm idk off the top of my head |
2023-12-11 00:41:36 +0100 | <dibblego> | well, is it the type of those things as well? |
2023-12-11 00:41:37 +0100 | <tri> | oh |
2023-12-11 00:41:48 +0100 | <dibblego> | I know quite a few things that have Select, but are not IEnumerable |
2023-12-11 00:41:51 +0100 | <tri> | IQueryable |
2023-12-11 00:41:54 +0100 | <dibblego> | can it be those as well? |
2023-12-11 00:42:30 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d128:ce35:54e1:65e2) |
2023-12-11 00:42:31 +0100 | <tri> | ok so your point is, b and a could be many things |
2023-12-11 00:42:38 +0100 | <dibblego> | yes, but not just anything |
2023-12-11 00:42:48 +0100 | <tri> | b is limited to interfaces/classes that have select |
2023-12-11 00:42:50 +0100 | <dibblego> | more specifically, "b can be anything that as Select" |
2023-12-11 00:42:53 +0100 | <dibblego> | right |
2023-12-11 00:42:55 +0100 | <tri> | while a could be anything |
2023-12-11 00:42:56 +0100 | <dibblego> | now write that interface |
2023-12-11 00:43:02 +0100 | <dibblego> | you will need HKT to do this |
2023-12-11 00:43:16 +0100 | <dibblego> | did you do it with C# ? |
2023-12-11 00:43:22 +0100 | Tuplanolla | (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) (Ping timeout: 255 seconds) |
2023-12-11 00:43:43 +0100 | <tri> | no i didn't but i guess it would not let me |
2023-12-11 00:43:56 +0100 | <tri> | but if i were to write it in Haskell |
2023-12-11 00:44:01 +0100 | <tri> | that could probably look like |
2023-12-11 00:44:02 +0100 | <dibblego> | it might, if C# had HKT |
2023-12-11 00:44:09 +0100 | <dibblego> | we could try... |
2023-12-11 00:44:34 +0100 | <tri> | Selectable b => a -> b -> a |
2023-12-11 00:44:46 +0100 | <dibblego> | that's not quite right is it |
2023-12-11 00:44:51 +0100 | <dibblego> | also, you need to write Selectable |
2023-12-11 00:45:08 +0100 | <tri> | yea the return is not right, since b is of a "collection" tyope |
2023-12-11 00:45:21 +0100 | <dibblego> | here is an invented of C#, with a slight change |
2023-12-11 00:45:39 +0100 | <dibblego> | Selectable<F<_>> => a -> F<b> -> F<a> |
2023-12-11 00:45:55 +0100 | <dibblego> | this is not real syntax of course |
2023-12-11 00:46:05 +0100 | <dibblego> | it's maybe what it might look like, if C# had HKT |
2023-12-11 00:46:18 +0100 | <dibblego> | Selectable exists in Haskell, because Haskell has HKT |
2023-12-11 00:46:21 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
2023-12-11 00:46:22 +0100 | <dibblego> | its name is different though |
2023-12-11 00:46:26 +0100 | <dibblego> | it's called Functor instead |
2023-12-11 00:46:34 +0100 | <dibblego> | @type \a b -> const a <$> b |
2023-12-11 00:46:35 +0100 | <lambdabot> | Functor f => b1 -> f b2 -> f b1 |
2023-12-11 00:46:54 +0100 | <tri> | oh i remember someone said that * -> * -> * is like generics of T<A,B>, which .NET can support |
2023-12-11 00:47:10 +0100 | <dibblego> | * -> * -> * is notation for the type of T |
2023-12-11 00:47:17 +0100 | <tri> | but .NET can't support (* -> *) -> * which is T<A<B>>, which is what you just did right |
2023-12-11 00:47:24 +0100 | <tri> | im just parroting what i remember |
2023-12-11 00:47:28 +0100 | <dibblego> | but we cannot use anything with that type, unless it is fully applied, because C# (and F#) do not have HKT |
2023-12-11 00:47:55 +0100 | <dibblego> | "IEnumerable" has a type, and that type is, "given a type, return a type" |
2023-12-11 00:48:07 +0100 | <tri> | yea that's generic, *->* |
2023-12-11 00:48:09 +0100 | <dibblego> | but we cannot use that thing, we cannot express it |
2023-12-11 00:48:21 +0100 | <glguy> | tri: assuming A takes one type parameter, (* -> *) -> * would be like: T<A> where A's types are not provided |
2023-12-11 00:48:28 +0100 | <dibblego> | more practically, we cannot write this type: |
2023-12-11 00:48:29 +0100 | <dibblego> | @type \a b -> const a <$> b |
2023-12-11 00:48:30 +0100 | <lambdabot> | Functor f => b1 -> f b2 -> f b1 |
2023-12-11 00:49:14 +0100 | <glguy> | type T c = (c Int, c Bool) -- like if you wanted to T to be parameterized by a container type and then use that container to contain two different kinds of elements |
2023-12-11 00:49:40 +0100 | <tri> | I still can't wrap my head over const a <$> b. I always think that const only take 2 args. 3 args there throws me off |
2023-12-11 00:50:20 +0100 | <glguy> | <$> isn't an argument to const |
2023-12-11 00:50:33 +0100 | <dibblego> | @type \a b -> fmap (const a) b -- same thing |
2023-12-11 00:50:34 +0100 | <lambdabot> | Functor f => b1 -> f b2 -> f b1 |
2023-12-11 00:51:01 +0100 | <tri> | oh ok, i need some time to read these again |
2023-12-11 00:52:57 +0100 | <tri> | @kind \a b -> const a <$> b |
2023-12-11 00:52:58 +0100 | <lambdabot> | error: parse error on input ‘\’ |
2023-12-11 00:53:48 +0100 | <glguy> | @type \a b -> const a <$> b |
2023-12-11 00:53:49 +0100 | <lambdabot> | Functor f => b1 -> f b2 -> f b1 |
2023-12-11 00:55:20 +0100 | <probie> | > const (*2) (+1) 5 -- Although, `const` can have "3 args", depending on how you count arguments |
2023-12-11 00:55:21 +0100 | <lambdabot> | 10 |
2023-12-11 00:56:13 +0100 | <tri> | ok............ |
2023-12-11 00:56:23 +0100 | <tri> | i gotta re-read HKT |
2023-12-11 00:56:39 +0100 | <tri> | thank you everyone |
2023-12-11 00:58:33 +0100 | <EvanR> | const takes 1 args |
2023-12-11 00:58:50 +0100 | <tri> | btw thanks probie and EvnR |
2023-12-11 01:01:57 +0100 | alp_ | (~alp@2001:861:e3d6:8f80:7092:9744:337:b98c) (Ping timeout: 256 seconds) |
2023-12-11 01:22:48 +0100 | Volt_ | (~Volt_@c-73-47-181-152.hsd1.ma.comcast.net) (Quit: ) |
2023-12-11 01:36:30 +0100 | juri_ | (~juri@79.140.117.38) |
2023-12-11 01:37:39 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 256 seconds) |
2023-12-11 01:39:41 +0100 | juri____ | (~juri@79.140.117.56) (Ping timeout: 268 seconds) |
2023-12-11 01:59:06 +0100 | skyres_ | (~skyres@176.254.244.83) |
2023-12-11 02:01:42 +0100 | <hexology> | hc: i believe the classic exponential time example is recursive fibonacci without memoization |
2023-12-11 02:01:47 +0100 | skyres | (~skyres@176.254.244.83) (Ping timeout: 264 seconds) |
2023-12-11 02:03:45 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.5) |
2023-12-11 02:06:21 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
2023-12-11 02:08:18 +0100 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 256 seconds) |
2023-12-11 02:10:08 +0100 | [_] | (~itchyjunk@user/itchyjunk/x-7353470) |
2023-12-11 02:13:54 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 268 seconds) |
2023-12-11 02:20:31 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) |
2023-12-11 02:21:32 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) |
2023-12-11 02:21:54 +0100 | waleee | (~waleee@176.10.144.38) (Ping timeout: 256 seconds) |
2023-12-11 02:22:49 +0100 | emmanuelux_ | (~emmanuelu@user/emmanuelux) (Ping timeout: 276 seconds) |
2023-12-11 02:26:20 +0100 | <Axman6> | tri: `const a <$> b` is `(const a) <$> b` (or, `(<$>) (const a) b` if you like to move infix functions to prefix) |
2023-12-11 02:27:01 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d128:ce35:54e1:65e2) (Remote host closed the connection) |
2023-12-11 02:27:33 +0100 | <ski> | @type (<$) |
2023-12-11 02:27:34 +0100 | <lambdabot> | Functor f => a -> f b -> f a |
2023-12-11 02:28:05 +0100 | <ski> | `const a <$> fb' is `a <$ fb' |
2023-12-11 02:28:36 +0100 | <ski> | tri,dibblego,geekosaur : i don't particularly like the term "higher-kinded type" at all, i think it's unnecessary and confusing. `chr :: Int -> Char' is a first-order function, `interact :: (String -> String) -> IO ()' is a second-order (therefore higher-order) function, because it takes a (first-order) function as input |
2023-12-11 02:28:49 +0100 | <ski> | `Either :: * -> * -> *' and `ReadS :: * -> *' (the former being a type constructor, while the latter being a type synonym of arity `1') are (first-order) type functions, while `MaybeT :: (* -> *) -> * -> *' is a second-order (therefore higher-order) type function (type constructor), and `Alternative :: (* -> *) -> Constraint' is a second-order type function (type class) |
2023-12-11 02:29:07 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 255 seconds) |
2023-12-11 02:39:45 +0100 | <hexology> | HLS style suggestions are really useful. i'm learning about a lot of nice utility functions i might not have found otherwise |
2023-12-11 02:41:36 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
2023-12-11 02:43:14 +0100 | <jackdk> | Are they the same ones that come from hlint? |
2023-12-11 02:44:41 +0100 | <hexology> | i wouldn't know |
2023-12-11 02:44:48 +0100 | <geekosaur> | they are |
2023-12-11 02:45:25 +0100 | <dibblego> | ski: I agree. |
2023-12-11 02:47:15 +0100 | <geekosaur> | tri, you missed from https://ircbrowse.tomsmeding.com/browse/lchaskell?id=1166072#trid1166072 |
2023-12-11 02:47:31 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 268 seconds) |
2023-12-11 02:47:35 +0100 | <geekosaur> | sigh |
2023-12-11 02:48:13 +0100 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) |
2023-12-11 02:57:28 +0100 | machinedgod | (~machinedg@93-136-52-133.adsl.net.t-com.hr) (Ping timeout: 255 seconds) |
2023-12-11 02:58:28 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
2023-12-11 02:59:27 +0100 | machinedgod | (~machinedg@93-136-135-211.adsl.net.t-com.hr) |
2023-12-11 02:59:49 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d128:ce35:54e1:65e2) |
2023-12-11 03:01:31 +0100 | <ski> | tri : are you there ? |
2023-12-11 03:04:28 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d128:ce35:54e1:65e2) (Ping timeout: 268 seconds) |
2023-12-11 03:05:34 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
2023-12-11 03:05:52 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d128:ce35:54e1:65e2) |
2023-12-11 03:06:04 +0100 | <jackdk> | that's cool. I learned a lot from the hlint suggestiosn |
2023-12-11 03:06:14 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
2023-12-11 03:06:16 +0100 | <jackdk> | Not spelling, admittedly, but a lot of other things |
2023-12-11 03:16:11 +0100 | <ski> | tri,dibblego,geekosaur : the, imho, bad term "higher-kinded types" refers to (a) being able to have polymorphic operations that are polymorphic in type functions, e.g. `empty :: Alternative f => f a'; .. |
2023-12-11 03:16:23 +0100 | <ski> | .. and (b) being able to parameterize type functions (including type classes) over other type functions, e.g. `newtype MaybeT m a = MaybeT (m (Maybe a))' and `class Applicative i => Alternative i where empty :: i a; ...', iow higher-order type functions |
2023-12-11 03:16:39 +0100 | <dibblego> | I also agree! |
2023-12-11 03:17:08 +0100 | <ski> | most other languages with parametric polymorphism and parameterized types ("generics") only allow the universally (and existentially, in case of Mercury) quantified variables in type signatures, as well as the type variable parameters in definitions of parameterized data types (iow type functions) to be of "concrete" kind, .. |
2023-12-11 03:17:16 +0100 | <ski> | .., iow in Haskell terms of kind `*'/`Type' (or other concrete kinds, like unboxed stuff), rather than of a kind of shape `... -> ...', iow a type function having a function kind |
2023-12-11 03:21:02 +0100 | <ski> | a type like `Map Integer [Integer]' (perhaps used to keep track of which other nodes each node in a graph is connected to) is a "template", with the "holes" filled by the types `Integer' (type of keys) and `[Integer]' (type of values). in some other language, this might be written as `Map<Integer,List<Integer>>' |
2023-12-11 03:21:19 +0100 | jle` | (~jle`@2603-8001-3b02-84d4-bd21-edb6-1dc1-99d4.res6.spectrum.com) (Ping timeout: 260 seconds) |
2023-12-11 03:22:06 +0100 | <ski> | most languages supporting such generics / parameterized types / "templates", though only allow "concrete" types to be parameters of the "templates", not allow other "templates" to be passed as parameters. Haskell does. templates in C++ also allows this, afaiui |
2023-12-11 03:34:15 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 252 seconds) |
2023-12-11 03:44:30 +0100 | <iqubic> | Does anyone here use Emacs? I have an LSP set up, but I'm wondering if it's possible to get inline evaluation working. Like, I type a comment of the form "-- >>> 1+2" and then hit a key combo and the code is evaluated and the result is put in the buffer. |
2023-12-11 03:47:16 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
2023-12-11 03:50:39 +0100 | ski | looks at tri |
2023-12-11 03:51:33 +0100 | <iqubic> | Why? |
2023-12-11 03:52:17 +0100 | maars | (uid160334@id-160334.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
2023-12-11 03:52:20 +0100 | <ski> | because i was trying to reply to them, but they keep disconnecting and reconnecting, and doesn't appear to be noticing IRC at the moment, for whatever reason |
2023-12-11 03:52:46 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 246 seconds) |
2023-12-11 03:52:54 +0100 | <ski> | (see ?) |
2023-12-11 03:53:16 +0100 | Pixi | (~Pixi@user/pixi) (Quit: Leaving) |
2023-12-11 03:53:32 +0100 | <iqubic> | I see. |
2023-12-11 03:56:35 +0100 | qqq | (~qqq@92.43.167.61) (Quit: leaving) |
2023-12-11 03:57:47 +0100 | <iqubic> | Basically, the emacs package Dante has this feature, and I want to see if I can have that done without installing a whole plugin for this. https://github.com/jyp/dante#reploid |
2023-12-11 03:59:40 +0100 | mrmr15533 | (~mrmr@user/mrmr) (Ping timeout: 276 seconds) |
2023-12-11 04:00:16 +0100 | <iqubic> | I want to see if I can have that done with just the plugins I have. |
2023-12-11 04:01:47 +0100 | YoungFrog | (~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be) (Ping timeout: 264 seconds) |
2023-12-11 04:02:31 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) |
2023-12-11 04:02:46 +0100 | hsw | (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) (Ping timeout: 256 seconds) |
2023-12-11 04:04:32 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
2023-12-11 04:05:45 +0100 | finn_elija | (~finn_elij@user/finn-elija/x-0085643) |
2023-12-11 04:05:45 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
2023-12-11 04:05:45 +0100 | finn_elija | FinnElija |
2023-12-11 04:05:51 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Quit: Leaving) |
2023-12-11 04:08:25 +0100 | urdh | (~urdh@user/urdh) |
2023-12-11 04:10:26 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 260 seconds) |
2023-12-11 04:12:43 +0100 | Pixi | (~Pixi@user/pixi) |
2023-12-11 04:15:31 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
2023-12-11 04:15:55 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
2023-12-11 04:16:12 +0100 | nate4 | (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
2023-12-11 04:20:05 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
2023-12-11 04:21:10 +0100 | nate4 | (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 255 seconds) |
2023-12-11 04:30:07 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 240 seconds) |
2023-12-11 04:30:11 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
2023-12-11 04:33:09 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
2023-12-11 04:33:56 +0100 | [_] | (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 256 seconds) |
2023-12-11 04:36:51 +0100 | machinedgod | (~machinedg@93-136-135-211.adsl.net.t-com.hr) (Ping timeout: 256 seconds) |
2023-12-11 04:37:36 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) () |
2023-12-11 04:37:46 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
2023-12-11 04:38:56 +0100 | hsw | (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) |
2023-12-11 04:39:33 +0100 | ski | glances in the general direction of tri |
2023-12-11 04:40:09 +0100 | [_] | (~itchyjunk@user/itchyjunk/x-7353470) |
2023-12-11 04:40:12 +0100 | renzhi | (~xp@2607:fa49:6500:b100::3ce6) (Quit: WeeChat 3.0) |
2023-12-11 04:43:41 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 245 seconds) |
2023-12-11 04:46:24 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 256 seconds) |
2023-12-11 04:46:32 +0100 | pagnol | (~user@2a02:a210:a3c:b00:87aa:b531:d3b2:73fa) (Ping timeout: 268 seconds) |
2023-12-11 04:46:39 +0100 | nate4 | (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
2023-12-11 04:49:44 +0100 | Feuermagier_ | (~Feuermagi@user/feuermagier) |
2023-12-11 04:49:44 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) (Killed (calcium.libera.chat (Nickname regained by services))) |
2023-12-11 04:49:45 +0100 | Feuermagier_ | Feuermagier |
2023-12-11 05:00:00 +0100 | Taneb | (~Taneb@runciman.hacksoc.org) (Quit: I seem to have stopped.) |
2023-12-11 05:00:10 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
2023-12-11 05:00:32 +0100 | Square | (~Square@user/square) (Ping timeout: 256 seconds) |
2023-12-11 05:01:07 +0100 | Taneb | (~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0) |
2023-12-11 05:02:19 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
2023-12-11 05:03:41 +0100 | [_] | (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 240 seconds) |
2023-12-11 05:04:44 +0100 | trev | (~trev@user/trev) |
2023-12-11 05:22:43 +0100 | hgolden | (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) (Remote host closed the connection) |
2023-12-11 05:24:30 +0100 | hgolden | (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) |
2023-12-11 05:28:35 +0100 | johnw | (~johnw@69.62.242.138) (Quit: ZNC - http://znc.in) |
2023-12-11 05:29:23 +0100 | hgolden | (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) (Remote host closed the connection) |
2023-12-11 05:31:27 +0100 | hgolden | (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) |
2023-12-11 05:39:56 +0100 | aforemny_ | (~aforemny@2001:9e8:6cdd:be00:6f70:eeee:fde4:e2c7) |
2023-12-11 05:41:16 +0100 | aforemny | (~aforemny@2001:9e8:6cf6:8a00:1295:f852:5f8f:52b5) (Ping timeout: 255 seconds) |
2023-12-11 05:48:53 +0100 | nate4 | (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
2023-12-11 05:50:36 +0100 | jargon | (~jargon@32.sub-174-238-226.myvzw.com) (Remote host closed the connection) |
2023-12-11 06:02:45 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
2023-12-11 06:03:02 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) |
2023-12-11 06:05:09 +0100 | [_] | (~itchyjunk@user/itchyjunk/x-7353470) |
2023-12-11 06:08:51 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 268 seconds) |
2023-12-11 06:14:22 +0100 | <brettgilio> | evening all |
2023-12-11 06:16:06 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
2023-12-11 06:16:19 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) |
2023-12-11 06:24:30 +0100 | pastly | (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
2023-12-11 06:24:53 +0100 | pastly | (~pastly@gateway/tor-sasl/pastly) |
2023-12-11 06:24:53 +0100 | gabriel_sevecek | (~gabriel@188-167-229-200.dynamic.chello.sk) (Ping timeout: 268 seconds) |
2023-12-11 06:34:24 +0100 | gabriel_sevecek | (~gabriel@188-167-229-200.dynamic.chello.sk) |
2023-12-11 06:50:35 +0100 | YoungFrog | (~youngfrog@2a02:a03f:ca07:f900:85cf:2f10:75d0:1ac9) |
2023-12-11 06:56:56 +0100 | <ski> | ello |
2023-12-11 07:01:35 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
2023-12-11 07:01:54 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2023-12-11 07:05:02 +0100 | bilegeek | (~bilegeek@2600:1008:b05f:7f4e:ace3:2d9c:d35a:2195) |
2023-12-11 07:09:40 +0100 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
2023-12-11 07:13:07 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
2023-12-11 07:13:39 +0100 | euleritian | (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) |
2023-12-11 07:22:34 +0100 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
2023-12-11 07:28:41 +0100 | Maeda | (~Maeda@91-161-10-149.subs.proxad.net) |
2023-12-11 07:30:10 +0100 | bilegeek | (~bilegeek@2600:1008:b05f:7f4e:ace3:2d9c:d35a:2195) (Quit: Leaving) |
2023-12-11 07:31:03 +0100 | igemnace | (~ian@user/igemnace) |
2023-12-11 07:31:29 +0100 | rosco | (~rosco@175.136.152.56) |
2023-12-11 07:40:45 +0100 | tornato | (uid197568@id-197568.tinside.irccloud.com) |
2023-12-11 07:43:26 +0100 | pastly | (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
2023-12-11 07:43:48 +0100 | pastly | (~pastly@gateway/tor-sasl/pastly) |
2023-12-11 07:48:13 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
2023-12-11 07:48:56 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
2023-12-11 07:58:19 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 268 seconds) |
2023-12-11 07:59:19 +0100 | <hc> | hexology: ah, makes sense |
2023-12-11 08:00:11 +0100 | johnw | (~johnw@69.62.242.138) |
2023-12-11 08:03:33 +0100 | phma | (~phma@2001:5b0:211c:d608:d6b3:ddaf:3415:a75) (Read error: Connection reset by peer) |
2023-12-11 08:04:38 +0100 | phma | (~phma@2001:5b0:2172:9948:cd8c:ca14:f1db:8548) |
2023-12-11 08:06:09 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-12-11 08:09:35 +0100 | CrunchyFlakes | (~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds) |
2023-12-11 08:12:48 +0100 | CrunchyFlakes | (~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de) |
2023-12-11 08:18:22 +0100 | shriekingnoise | (~shrieking@186.137.175.87) (Ping timeout: 276 seconds) |
2023-12-11 08:24:06 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
2023-12-11 08:31:16 +0100 | pagnol | (~user@i159006.upc-i.chello.nl) |
2023-12-11 08:32:59 +0100 | acidjnk_new | (~acidjnk@p200300d6e72b9326b4dc018a2c6658c2.dip0.t-ipconnect.de) |
2023-12-11 08:34:47 +0100 | alp_ | (~alp@2001:861:e3d6:8f80:c12e:3d55:b6:f405) |
2023-12-11 08:38:38 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) |
2023-12-11 08:39:12 +0100 | gdown | (~gavin@h69-11-149-109.kndrid.broadband.dynamic.tds.net) (Remote host closed the connection) |
2023-12-11 08:39:22 +0100 | chiselfuse | (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
2023-12-11 08:39:35 +0100 | Pixi | (~Pixi@user/pixi) (Ping timeout: 264 seconds) |
2023-12-11 08:39:54 +0100 | chiselfuse | (~chiselfus@user/chiselfuse) |
2023-12-11 08:43:26 +0100 | ricardo1 | (~ricardo@84.16.179.218) (Read error: Connection reset by peer) |
2023-12-11 08:44:57 +0100 | Guest65 | (~Guest16@136.169.59.60) |
2023-12-11 08:45:35 +0100 | Guest65 | (~Guest16@136.169.59.60) (Client Quit) |
2023-12-11 08:45:45 +0100 | Guest61 | (~Guest16@136.169.59.60) |
2023-12-11 08:48:21 +0100 | Guest61 | (~Guest16@136.169.59.60) (Client Quit) |
2023-12-11 08:50:33 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
2023-12-11 08:51:23 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
2023-12-11 08:56:11 +0100 | Pixi | (~Pixi@user/pixi) |
2023-12-11 08:58:18 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
2023-12-11 08:58:27 +0100 | euleritian | (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
2023-12-11 08:58:44 +0100 | euleritian | (~euleritia@77.22.252.56) |
2023-12-11 09:03:52 +0100 | dcoutts | (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 276 seconds) |
2023-12-11 09:10:10 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
2023-12-11 09:14:07 +0100 | [_] | (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 260 seconds) |
2023-12-11 09:14:27 +0100 | gmg | (~user@user/gehmehgeh) |
2023-12-11 09:15:49 +0100 | akegalj | (~akegalj@78-3-59-204.adsl.net.t-com.hr) |
2023-12-11 09:17:13 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 256 seconds) |
2023-12-11 09:20:17 +0100 | Guest18 | (~Guest18@41.73.1.72) |
2023-12-11 09:20:18 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) |
2023-12-11 09:23:25 +0100 | euleritian | (~euleritia@77.22.252.56) (Ping timeout: 268 seconds) |
2023-12-11 09:23:47 +0100 | euleritian | (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) |
2023-12-11 09:36:20 +0100 | ricardo1 | (~ricardo@84.16.179.218) |
2023-12-11 09:39:14 +0100 | <haskellbridge> | 12<Celestial> The IORef worked perfectly, thanks again ski, monochrom and EvanR. |
2023-12-11 09:39:15 +0100 | <haskellbridge> | 12<Celestial> The only problem I now have is that I can't access the value of it in my renderer as it's not in any monad transformer with IO. I could store the value in the state manually but that would be annoying to keep track of |
2023-12-11 09:42:02 +0100 | <[exa]> | Celestial: can you do with some other kind of shared var? (TVar?) |
2023-12-11 09:42:22 +0100 | <[exa]> | (TVars don't require IO, just "any" kind of STM) |
2023-12-11 09:43:28 +0100 | <[exa]> | anyway if the renderer doesn't modify the variable, just smash an extra Reader to the monad stack. :] |
2023-12-11 09:43:38 +0100 | <haskellbridge> | 12<Celestial> the `appDraw` context is merely `ApplicationState -> [Widget ()]` |
2023-12-11 09:45:16 +0100 | <[exa]> | okay with that type it can't work very easily |
2023-12-11 09:46:42 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d128:ce35:54e1:65e2) (Remote host closed the connection) |
2023-12-11 09:49:17 +0100 | fendor | (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) |
2023-12-11 09:49:52 +0100 | CiaoSen | (~Jura@2a05:5800:285:a500:ca4b:d6ff:fec1:99da) |
2023-12-11 09:50:15 +0100 | danza | (~danza@151.19.241.170) |
2023-12-11 09:52:01 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
2023-12-11 09:52:28 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
2023-12-11 09:54:12 +0100 | <tomsmeding> | if you don't have any side effects, you'll need the functional approach to state, which is, unsurprisingly, State |
2023-12-11 09:54:52 +0100 | <tomsmeding> | ah but even that wouldn't work |
2023-12-11 10:03:22 +0100 | td_ | (~td@i5387090E.versanet.de) |
2023-12-11 10:07:34 +0100 | danza | (~danza@151.19.241.170) (Ping timeout: 276 seconds) |
2023-12-11 10:10:59 +0100 | aku | (~aku@65.108.245.241) (Remote host closed the connection) |
2023-12-11 10:11:57 +0100 | aku | (~aku@65.108.245.241) |
2023-12-11 10:12:20 +0100 | <ski> | why not ? |
2023-12-11 10:13:43 +0100 | chele | (~chele@user/chele) |
2023-12-11 10:19:23 +0100 | <tomsmeding> | because the type is ApplicationState -> [Widget ()] :p |
2023-12-11 10:19:30 +0100 | <tomsmeding> | there be no returned state in there |
2023-12-11 10:19:52 +0100 | <tomsmeding> | oh, unless you're only reading here and the rest of the code does use the State monad with ApplicationState |
2023-12-11 10:21:49 +0100 | <[Leary]> | They probably are, looks like brick to me: https://hackage.haskell.org/package/brick-2.1.1/docs/Brick-Main.html#v:appDraw |
2023-12-11 10:23:29 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d128:ce35:54e1:65e2) |
2023-12-11 10:24:26 +0100 | myxos | (~myxos@065-028-251-121.inf.spectrum.com) (Remote host closed the connection) |
2023-12-11 10:25:09 +0100 | myxos | (~myxos@065-028-251-121.inf.spectrum.com) |
2023-12-11 10:25:31 +0100 | danza | (~danza@151.37.255.204) |
2023-12-11 10:26:20 +0100 | ski | was thinking the current `IORef' contents could be part of `ApplicationState', perhaås |
2023-12-11 10:29:15 +0100 | ft | (~ft@p3e9bc784.dip0.t-ipconnect.de) (Quit: leaving) |
2023-12-11 10:31:18 +0100 | tzh | (~tzh@c-71-193-181-0.hsd1.or.comcast.net) (Quit: zzz) |
2023-12-11 10:31:46 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Ping timeout: 246 seconds) |
2023-12-11 10:33:50 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
2023-12-11 10:34:47 +0100 | tornato | (uid197568@id-197568.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
2023-12-11 10:39:07 +0100 | __monty__ | (~toonn@user/toonn) |
2023-12-11 10:39:16 +0100 | danza | (~danza@151.37.255.204) (Ping timeout: 268 seconds) |
2023-12-11 10:40:19 +0100 | Luj | (~Luj@mail.julienmalka.me) (Quit: Ping timeout (120 seconds)) |
2023-12-11 10:40:35 +0100 | Luj | (~Luj@2a01:e0a:5f9:9681:cb3c:6a2b:179a:30d3) |
2023-12-11 10:43:29 +0100 | euleritian | (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
2023-12-11 10:43:47 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2023-12-11 10:48:26 +0100 | danse-nr3 | (~danse@151.37.255.204) |
2023-12-11 10:58:22 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
2023-12-11 10:58:49 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2023-12-11 11:01:38 +0100 | Guest18 | (~Guest18@41.73.1.72) (Quit: Ping timeout (120 seconds)) |
2023-12-11 11:16:05 +0100 | machinedgod | (~machinedg@93-136-135-211.adsl.net.t-com.hr) |
2023-12-11 11:16:28 +0100 | machinedgod | (~machinedg@93-136-135-211.adsl.net.t-com.hr) (Client Quit) |
2023-12-11 11:17:34 +0100 | machinedgod | (~machinedg@93-136-135-211.adsl.net.t-com.hr) |
2023-12-11 11:18:11 +0100 | idgaen | (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
2023-12-11 11:18:44 +0100 | not_reserved | (~not_reser@45.88.222.248) (Quit: Client closed) |
2023-12-11 11:19:06 +0100 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) |
2023-12-11 11:19:40 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 256 seconds) |
2023-12-11 11:20:03 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-12-11 11:21:04 +0100 | <dminuoso_> | Say I have a tree of labels, and a tree of patterns - now I have a notion of testing whether the PatTree matches a given LabelTree (by just checking whether they have the same shape and whether each pattern matches is structurally matching label. |
2023-12-11 11:21:46 +0100 | <dminuoso_> | Labels themselves are Text, and a pattern could be either a literal "foo" (which is just a Text, that I would match against the label by equality), or a wildcard. |
2023-12-11 11:22:04 +0100 | Lord_of_Life_ | Lord_of_Life |
2023-12-11 11:24:35 +0100 | <dminuoso_> | Now sometimes a LabelTree and a PatTree share some structural similarity (but not straight up equality), where a PatTree is somehow larger than a LabelTree - but when you lay them ontop of each other, in the intersection they do match. |
2023-12-11 11:24:39 +0100 | <dminuoso_> | What would you call this sort of relationship? |
2023-12-11 11:25:21 +0100 | <dminuoso_> | I really want to call this a sort of "subtree"/"supertree" (in the sense of a subset/superset) |
2023-12-11 11:25:40 +0100 | <dminuoso_> | Though that name seems to be used for branches inside a given tree already |
2023-12-11 11:26:18 +0100 | <danse-nr3> | also depends on what are your plans. Will the patterns always be either literals or wildcards? Sounds unlikely. That intersection, it would be interesting to know better what it means |
2023-12-11 11:27:08 +0100 | <dminuoso_> | danse-nr3: There's also the notion of a globstar (a recursive wildcard, where any "subtree" in the traditional sense is allowed). |
2023-12-11 11:27:18 +0100 | <dminuoso_> | There is no plan for other patterns. |
2023-12-11 11:34:27 +0100 | mikess | (~sam@user/mikess) (Ping timeout: 268 seconds) |
2023-12-11 11:36:35 +0100 | <danse-nr3> | i am not sure whether this is a matter of naming the relationship or thinking about the code structure. If patterns do not completely match labels, what does one do with the rest? Also, i would expect a tree to mostly match from the root up. If this is not the case, it becomes more interesting |
2023-12-11 11:39:55 +0100 | forell | (~forell@user/forell) (Ping timeout: 255 seconds) |
2023-12-11 11:39:56 +0100 | jinsun_ | (~jinsun@user/jinsun) |
2023-12-11 11:39:56 +0100 | jinsun | Guest9536 |
2023-12-11 11:39:57 +0100 | Guest9536 | (~jinsun@user/jinsun) (Killed (silver.libera.chat (Nickname regained by services))) |
2023-12-11 11:39:57 +0100 | jinsun_ | jinsun |
2023-12-11 11:40:29 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-12-11 11:40:42 +0100 | forell | (~forell@user/forell) |
2023-12-11 11:42:29 +0100 | <dminuoso_> | Okay let me rephrase: is there a particular name for a subtree ST or T that (necessarily) shares the root of T? |
2023-12-11 11:43:39 +0100 | <danse-nr3> | do subtrees always share the root? Good question |
2023-12-11 11:44:12 +0100 | <danse-nr3> | no |
2023-12-11 11:45:37 +0100 | <danse-nr3> | and did not find interesting results via a quick "root sharing subtree" search |
2023-12-11 11:45:38 +0100 | hgolden_ | (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) |
2023-12-11 11:46:30 +0100 | <danse-nr3> | but it sounds like an useful abstraction, probably existent, maybe try #math |
2023-12-11 11:47:05 +0100 | <ski> | "but when you lay them ontop of each other, in the intersection they do match" -- elaborate ? |
2023-12-11 11:47:16 +0100 | nate4 | (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
2023-12-11 11:47:22 +0100 | lawt | (~lawt@2603:c024:c008:d000:5b4f:1ef2:fed2:ef3d) (Ping timeout: 246 seconds) |
2023-12-11 11:47:31 +0100 | hgolden | (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) (Read error: Connection reset by peer) |
2023-12-11 11:47:36 +0100 | <danse-nr3> | label tree is a subset of pattern tree including the root |
2023-12-11 11:47:55 +0100 | lawt | (~lawt@2603:c024:c008:d000:5b4f:1ef2:fed2:ef3d) |
2023-12-11 11:48:05 +0100 | <danse-nr3> | a subtree to be more precise |
2023-12-11 11:48:44 +0100 | <ski> | "a subtree ST or T that (necessarily) shares the root of T" -- sounds maybe related to the notion of "bar" |
2023-12-11 11:49:14 +0100 | <danse-nr3> | a more searchable term? "tree bar"? |
2023-12-11 11:49:16 +0100 | <ski> | dminuoso_ ^ |
2023-12-11 11:51:24 +0100 | <ski> | Brouwer's "bar induction/recursion" is about having a tree with all branches infinite, but each path from the root eventually becomes constant (the elements in the nodes), and so there's a "bar", crossing every path from the root, so that after the bar, each path is definitely constant |
2023-12-11 11:51:39 +0100 | <danse-nr3> | cheers |
2023-12-11 11:52:00 +0100 | nate4 | (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 252 seconds) |
2023-12-11 11:52:40 +0100 | <ski> | (so, you can represent such an infinite tree with a finite tree, down to the bar, and in the leaves you put the element that repeats forever from there .. and you can also put some "result" for every path through that leaf) |
2023-12-11 11:53:11 +0100 | <dminuoso_> | ski: Take any given tree, call it T, it has the root R. Now, T may have a number of subtrees ST. But Im not interested in every subtree, but precisely those subtrees that have the same root R that T has. |
2023-12-11 11:54:09 +0100 | <danse-nr3> | yes that does seem to relate to bars |
2023-12-11 11:54:55 +0100 | <dminuoso_> | If I flip the relationship around, I might call T an extension of ST maybe. |
2023-12-11 11:54:58 +0100 | <ski> | specifically, a (computable) function from `Stream Bool'/`Nat -> Bool' to some finite datatype (e.g. `Bool') could be argued to only look at a finite prefix of its input stream, before deciding on its output (because otherwise it would require looking at infinite information in finite time). and so, we can visualize such a function as an infinite tree, with a bar, with leaves indicating the finite result |
2023-12-11 11:55:04 +0100 | <ski> | value for each path passing through that leaf (corresponding to a bar node) |
2023-12-11 11:55:04 +0100 | <ski> | this is related to |
2023-12-11 11:55:07 +0100 | <ski> | @where impossible |
2023-12-11 11:55:08 +0100 | <lambdabot> | <http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/>,<http://math.andrej.com/2008/11/21/a-haskell-monad-for-infinite-search-in-finite-time/> |
2023-12-11 11:55:56 +0100 | <ski> | (you could take streams of other types as input, getting a different branching factor in the trees) |
2023-12-11 11:56:44 +0100 | <ski> | dminuoso_ : i'm still wondering about the "intersection" part, what you mean by that |
2023-12-11 11:57:02 +0100 | <ski> | was that about the "globstar" patterns, or something else ? |
2023-12-11 11:57:14 +0100 | <dminuoso_> | Okay, so let me reduce the problem slightly. |
2023-12-11 11:57:27 +0100 | ncf | . o O ( uniform continuity ) |
2023-12-11 11:58:09 +0100 | <dminuoso_> | Say I have domain names. Domain names are lists of labels ["www", "google", "de"]. Now I may want to specify on what domain names one may operator by describing a pattern [Glob, Lit "google", Lit "de"] |
2023-12-11 11:58:20 +0100 | ski | would possibly also parameterize, so `LabelTree = Tree Label' and `PatTree = Tree Pat' .. or maybe something with zippers for the latter, due to "globstar" |
2023-12-11 11:58:22 +0100 | <dminuoso_> | Instead of trees, this is lists now. |
2023-12-11 11:58:59 +0100 | <ski> | you want to build like tries ? |
2023-12-11 11:59:22 +0100 | <dminuoso_> | I do build a lot of tries at the end, yes. |
2023-12-11 11:59:37 +0100 | <dminuoso_> | So given this simplified version, in some situations I might pose the question "is the pattern *.google.de something inside the google.de zone" |
2023-12-11 12:00:12 +0100 | <dminuoso_> | Which becomes just checking whether the domain is a suffix of the pattern |
2023-12-11 12:01:17 +0100 | <ski> | hm, maybe the terms "crop" or "extend" could be useful, wrt these trees |
2023-12-11 12:01:37 +0100 | <ski> | one tree being a cropped/pruned version of the other, or the other being an extended version of the first |
2023-12-11 12:03:00 +0100 | <danse-nr3> | it would be interesting to check which terms Brouwer used, maybe there is already a "pruned" |
2023-12-11 12:03:01 +0100 | <dminuoso_> | ski: cropped/pruned doesnt sound all too bad. Or maybe I should just do the math thing and make something up, like "rooted subtree", define it in a note somewhere, and put a bunch of "See Note [Rooted Subtree]" all over the place. |
2023-12-11 12:04:52 +0100 | <ski> | data Tree b e a = Leaf a | Node e (b (Tree b e a)) |
2023-12-11 12:05:20 +0100 | <ski> | type LabelTree e a = Tree (Map Text) e a |
2023-12-11 12:06:10 +0100 | <dminuoso_> | But yeah, Im beginning to see the similarity to Brouwers work here. |
2023-12-11 12:06:32 +0100 | <ski> | type PatTree e a = Tree (Map (Maybe (Either Label Text))) e (Either Label a) |
2023-12-11 12:06:39 +0100 | <ski> | something along those lines, maybe |
2023-12-11 12:07:30 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
2023-12-11 12:07:34 +0100 | <ski> | (`a' for making it a `Monad') |
2023-12-11 12:08:10 +0100 | euleritian | (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) |
2023-12-11 12:08:33 +0100 | euleritian | (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
2023-12-11 12:08:50 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2023-12-11 12:11:10 +0100 | <ski> | hm |
2023-12-11 12:11:38 +0100 | <ski> | type PatTree e = Tree (Map (Maybe (Either Label Text))) e Label -- perhaps instead |
2023-12-11 12:12:15 +0100 | <ski> | then doing `patTree >>= subst' replaces the `Label' leaves according to `subst :: Label -> PatTree e' |
2023-12-11 12:12:16 +0100 | Joao003 | (~Joao003@190.108.99.32) |
2023-12-11 12:14:29 +0100 | kritzefitz_ | (~kritzefit@debian/kritzefitz) |
2023-12-11 12:15:09 +0100 | kritzefitz | (~kritzefit@debian/kritzefitz) (Ping timeout: 256 seconds) |
2023-12-11 12:15:55 +0100 | gabriel_sevecek | (~gabriel@188-167-229-200.dynamic.chello.sk) (Ping timeout: 255 seconds) |
2023-12-11 12:19:21 +0100 | kritzefitz_ | kritzefitz |
2023-12-11 12:20:32 +0100 | gabriel_sevecek | (~gabriel@188-167-229-200.dynamic.chello.sk) |
2023-12-11 12:22:43 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 246 seconds) |
2023-12-11 12:25:41 +0100 | yaroot_ | (~yaroot@2400:4052:ac0:d901:1cf4:2aff:fe51:c04c) |
2023-12-11 12:25:45 +0100 | yaroot | (~yaroot@p2987138-ipngn7501souka.saitama.ocn.ne.jp) (Read error: Connection reset by peer) |
2023-12-11 12:25:46 +0100 | yaroot_ | yaroot |
2023-12-11 12:29:47 +0100 | <danse-nr3> | my ADA doubled in value since november |
2023-12-11 12:31:46 +0100 | <ski> | you're coding Ada ? |
2023-12-11 12:32:54 +0100 | <danse-nr3> | no, unfortunately blockchain tech is not easy to approach without previous experience, and i have heard that doing that in haskell is not the easiest. I just bought a small amount of them |
2023-12-11 12:32:55 +0100 | pastly | (~pastly@gateway/tor-sasl/pastly) (Ping timeout: 240 seconds) |
2023-12-11 12:33:28 +0100 | <ski> | mhm |
2023-12-11 12:34:29 +0100 | pastly | (~pastly@gateway/tor-sasl/pastly) |
2023-12-11 12:34:29 +0100 | machinedgod | (~machinedg@93-136-135-211.adsl.net.t-com.hr) (Ping timeout: 240 seconds) |
2023-12-11 12:40:29 +0100 | phma | (~phma@2001:5b0:2172:9948:cd8c:ca14:f1db:8548) (Read error: Connection reset by peer) |
2023-12-11 12:41:16 +0100 | phma | (~phma@host-67-44-208-181.hnremote.net) |
2023-12-11 12:41:39 +0100 | cfricke | (~cfricke@user/cfricke) |
2023-12-11 12:44:28 +0100 | eayus | (~eayus@8afbc74e.st-andrews.ac.uk) |
2023-12-11 12:48:19 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
2023-12-11 12:49:31 +0100 | <eayus> | Using Data.Data/Data.Typeable, is it possible to `cast` to a polymorphic type (introducing some existential type variables perhaps). |
2023-12-11 12:49:32 +0100 | <eayus> | For example, suppose I wanted to transform all `Maybe`s in a term to `Nothing`, regardless of what type `Maybe` is instantiated with. Does anyone know how I might acheive this? |
2023-12-11 12:51:14 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
2023-12-11 12:51:49 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2023-12-11 12:52:21 +0100 | <dminuoso_> | :t Nothing |
2023-12-11 12:52:22 +0100 | <lambdabot> | Maybe a |
2023-12-11 12:52:25 +0100 | <dminuoso_> | eayus: It's already builtin. |
2023-12-11 12:52:37 +0100 | <dminuoso_> | That is, Nothing *is* already polymorphic. |
2023-12-11 12:52:51 +0100 | <dminuoso_> | Keep in mind that a "polymorphic type" means something else, namely one that is polymorphic in its kind. |
2023-12-11 12:53:12 +0100 | <dminuoso_> | (You probably meant to say quantified type instead) |
2023-12-11 12:53:38 +0100 | <dminuoso_> | eayus: The bigger question I have is what you mean by "transform" and "term" exactly. |
2023-12-11 12:56:33 +0100 | xdej | (~xdej@quatramaran.salle-s.org) (Remote host closed the connection) |
2023-12-11 12:57:36 +0100 | <ski> | (a universal type (a `forall'-type) is also quite distinct from an existential type (an `exists'-type)) |
2023-12-11 12:57:54 +0100 | <ski> | (but perhaps by "existential type variables", you really meant "meta-variables" or something ..) |
2023-12-11 12:58:00 +0100 | <eayus> | Perhaps I misexplained my problem. Using Data.Data and Data.Typeable, I can generically transform any data type which implements those classes. For example I could increment all `Int`s using `gmapT`, and `cast`, without knowing what type I am working on. I want to make a similar generic function which turns all `Maybe`s into `Nothing`s. |
2023-12-11 12:58:01 +0100 | <eayus> | The issue is that `cast` requires a concrete type, but I want to transform any `Maybe` regardless of what type it is instantiated with |
2023-12-11 12:58:33 +0100 | <eayus> | By existential type variables I mean a variable which is "forall" quantified with a constructor |
2023-12-11 12:58:36 +0100 | <dminuoso_> | :t cast |
2023-12-11 12:58:37 +0100 | <lambdabot> | (Typeable a, Typeable b) => a -> Maybe b |
2023-12-11 12:58:46 +0100 | <ski> | @type gcast |
2023-12-11 12:58:47 +0100 | <lambdabot> | forall k (a :: k) (b :: k) (c :: k -> *). (Typeable a, Typeable b) => c a -> Maybe (c b) |
2023-12-11 12:59:44 +0100 | <ski> | eayus : that would be a universal type variable, then. (`forall' means universal quantification. `exists' means existential quantification) |
2023-12-11 13:00:41 +0100 | <lortabac> | well, forall in Haskell syntax also means existential quantification |
2023-12-11 13:00:59 +0100 | <ski> | .. but if you mean `data SomeFoo = forall a. Cxt a => WrapFoo (Foo a)', then `WrapFoo' is polymorphic, having type `forall a. Cxt a => Foo a -> SomeFoo', but that's equivalent to `(exists a. Cxt a *> Foo a) -> SomeFoo', so `SomeFoo' amounts to `exists a. Cxt a *> Foo a' here |
2023-12-11 13:01:08 +0100 | <ski> | lortabac : it doesn't |
2023-12-11 13:01:53 +0100 | <ski> | `WrapFoo' is polymorphic, has a universally quantified type. it's not "abstract(ed)". its *argument* could be said to be abstract(ed) (as in abstract data types) |
2023-12-11 13:02:58 +0100 | <ski> | (also, imho, the extension name `ExistentialQuantification' is a misnomer. a better (more accurate) name might be perhaps `ExistentialConstructors' .. i'd want to reserve `ExistentialQuantification' for if we ever get an actual `exists' syntax (distinct from the aforementioned extension)) |
2023-12-11 13:03:39 +0100 | <ski> | (also, that extension isn't the only way to encode existentials. the other way is using `Rank2Types', as `forall o. (forall a. Cxt a => Foo a -> o) -> o') |
2023-12-11 13:05:30 +0100 | <ski> | (if you're saying the `forall' there at `WrapFoo' means existentials, you could also say the `forall' in `length :: forall a. [a] -> Int' means existentials, because this is equivalent to `length :: (exists a. [a]) -> Int'. saying that for any type `a', `length' can take a list of `a's and returns an `Int', is the same as saying that `length' returns an `Int', as long as there exists some type `a' such that |
2023-12-11 13:05:36 +0100 | <ski> | you apply `length' to a list of `a's) |
2023-12-11 13:05:45 +0100 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
2023-12-11 13:11:28 +0100 | <lortabac> | I see what you mean |
2023-12-11 13:12:46 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds) |
2023-12-11 13:13:00 +0100 | <lortabac> | I was trying to understand what eayus said. It seems they are referring to ExistentialQuantification |
2023-12-11 13:13:32 +0100 | euleritian | (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) |
2023-12-11 13:13:43 +0100 | <eayus> | I was referring to the use of a forall in a type constructor, as described here: https://wiki.haskell.org/Existential_type |
2023-12-11 13:13:56 +0100 | <eayus> | I.e. pattern matching introduces a type variable |
2023-12-11 13:17:04 +0100 | <Joao003> | can i ask for context? |
2023-12-11 13:18:55 +0100 | danse-nr3 | (~danse@151.37.255.204) (Ping timeout: 255 seconds) |
2023-12-11 13:23:19 +0100 | <eayus> | I want to find all free variables in an AST. Rather than write the recursion manually introducing a lot of boiler plate, it makes sense to do a generic traversal. |
2023-12-11 13:23:20 +0100 | <eayus> | The idea is to introduce a `Binder` type used whenever a avariable is bound. This can be identified by the generic traversal to make sure that variable is not classified as free. |
2023-12-11 13:23:20 +0100 | <eayus> | If `Binder` has kind `*`, I can use `cast` to tell whether im looking at a binder. However, sometimes I'm binding different things of different type, so `Binder` needs to be of type `* -> *`. |
2023-12-11 13:23:21 +0100 | <eayus> | This is what causes the problem, as I can no longer use `cast` to tell whether I'm looking at a `Binder` |
2023-12-11 13:23:27 +0100 | euleritian | (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
2023-12-11 13:23:44 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2023-12-11 13:24:37 +0100 | pagnol | (~user@i159006.upc-i.chello.nl) (Remote host closed the connection) |
2023-12-11 13:24:54 +0100 | <eayus> | Here is an example with a non polymorphic binder: https://paste.tomsmeding.com/wf5s1TQj |
2023-12-11 13:25:47 +0100 | Joao003 | (~Joao003@190.108.99.32) (Read error: Connection reset by peer) |
2023-12-11 13:26:07 +0100 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 256 seconds) |
2023-12-11 13:29:05 +0100 | <dminuoso_> | "free variables in an AST" |
2023-12-11 13:30:20 +0100 | <dminuoso_> | eayus: Mind my asking, any particular reason you arent using say unbound? |
2023-12-11 13:34:03 +0100 | Joao003 | (~Joao003@190.108.99.207) |
2023-12-11 13:35:48 +0100 | <eayus> | It's an option though it seems using bound/unbound would limit my generic programming to only variable related stuff. I might want to also do a generic traversal when normalising terms for example |
2023-12-11 13:38:04 +0100 | <ski> | hm. sounds like you want something like `someCast :: (Typeable a,Typeable f) => a -> Maybe (Some f)' |
2023-12-11 13:38:14 +0100 | <eayus> | yeah exactly |
2023-12-11 13:39:56 +0100 | <ski> | (so, you don't want to cast to a universal type (getting a polymorphic value), but you do want to cast to an existential type (getting an abstracted value)) |
2023-12-11 13:40:24 +0100 | ski | decides to try using "abstracted" for these, for a while |
2023-12-11 13:42:49 +0100 | danse-nr3 | (~danse@151.19.230.254) |
2023-12-11 13:48:00 +0100 | <eayus> | Another approach I've considered is using the Functor/Fix pattern. |
2023-12-11 13:48:01 +0100 | <eayus> | Perhaps defining the AST as a type like |
2023-12-11 13:48:01 +0100 | <eayus> | `data ExprF ( binder :: ( * -> * ) -> * ) ( expr :: * )`. |
2023-12-11 13:48:02 +0100 | <eayus> | `data Binder ( f :: * -> * ) = Binder Name (f Expr)` |
2023-12-11 13:48:02 +0100 | <eayus> | `type Expr = Fix (ExprF Binder)` |
2023-12-11 13:48:24 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3341-aec3-516d-6fbd-7275-d6e8.rev.sfr.net) |
2023-12-11 13:49:18 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-12-11 13:50:23 +0100 | <eayus> | For `ExprF` i can derive functor, though I would have to write something like this manually maybe |
2023-12-11 13:50:24 +0100 | <eayus> | `f :: (forall f. Functor f => Binder f -> Binder f) -> ExprF binder expr -> ExprF binder expr` |
2023-12-11 13:51:39 +0100 | <eayus> | That's incorrect actually, this instead: |
2023-12-11 13:51:40 +0100 | <eayus> | `_ :: (forall f. Functor f => binder f -> binder f) -> ExprF binder expr -> ExprF binder expr` |
2023-12-11 13:54:22 +0100 | <poscat> | Anyone using the ghc package provided by fedora? Why I'm I unable to use the :doc command? (it says "Try re-compiling with '-haddock'.") |
2023-12-11 13:57:23 +0100 | <danse-nr3> | could be that ghc was not compiled with -haddock, although i think it refers to the specific haskell package you want to query the docs about, therefore it should not matter that you are using a fedora ghc package |
2023-12-11 14:03:47 +0100 | Joao003 | (~Joao003@190.108.99.207) (Remote host closed the connection) |
2023-12-11 14:03:58 +0100 | dcoutts | (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
2023-12-11 14:04:11 +0100 | Joao003 | (~Joao003@190.108.99.207) |
2023-12-11 14:08:20 +0100 | eayus70 | (~eayus@8afbc74e.st-andrews.ac.uk) |
2023-12-11 14:09:04 +0100 | eayus | (~eayus@8afbc74e.st-andrews.ac.uk) (Ping timeout: 250 seconds) |
2023-12-11 14:11:58 +0100 | CiaoSen | (~Jura@2a05:5800:285:a500:ca4b:d6ff:fec1:99da) (Ping timeout: 276 seconds) |
2023-12-11 14:12:19 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
2023-12-11 14:16:53 +0100 | hamster | (~ham@user/ham) |
2023-12-11 14:18:50 +0100 | ircbrowse_tom | (~ircbrowse@2a01:4f8:1c1c:9319::1) |
2023-12-11 14:18:56 +0100 | Server | +Cnt |
2023-12-11 14:27:20 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-12-11 14:27:31 +0100 | <eayus70> | Ok, for anyone curious, I think i've managed to find a solution to my earlier problem. The idea is to not have an explicit binder type, but use the structure of the AST to encode where a variable is bound. |
2023-12-11 14:27:32 +0100 | <eayus70> | Everything to the right of a binding name in the AST will have that name in scope. A function such as free variable computation can be implemented by folding over the constructors arguments |
2023-12-11 14:27:33 +0100 | sawilagar | (~sawilagar@user/sawilagar) |
2023-12-11 14:28:00 +0100 | bonaogeto | (~bonaogeto@105.163.158.10) |
2023-12-11 14:29:47 +0100 | <Joao003> | is there any function to clear the terminal output? |
2023-12-11 14:30:01 +0100 | <danse-nr3> | C-l? |
2023-12-11 14:30:35 +0100 | bonaogeto | (~bonaogeto@105.163.158.10) (Client Quit) |
2023-12-11 14:30:44 +0100 | <Joao003> | wdym? |
2023-12-11 14:31:00 +0100 | <danse-nr3> | press Control and l at the same time |
2023-12-11 14:31:18 +0100 | <eayus70> | `clearScreen` from ansi-terminal package maybe |
2023-12-11 14:31:24 +0100 | <Joao003> | i want a haskell function to clear terminal output, bruh |
2023-12-11 14:35:09 +0100 | <ncf> | putStr "\ESC[H\ESC[2J" |
2023-12-11 14:35:20 +0100 | <ncf> | (not portable) |
2023-12-11 14:40:43 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
2023-12-11 14:43:05 +0100 | <ski> | % System.Cmd.system "tput clear" |
2023-12-11 14:43:05 +0100 | <yahb2> | tput: No value for $TERM and no -T specified ; ExitFailure 2 |
2023-12-11 14:43:37 +0100 | <Joao003> | this isn't really portable |
2023-12-11 14:45:22 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 256 seconds) |
2023-12-11 14:45:52 +0100 | <Rembane> | Joao003: Which platforms do you need to support? |
2023-12-11 14:46:16 +0100 | <Joao003> | i just want the most reliable way to clear screen, Rembane |
2023-12-11 14:46:43 +0100 | <exarkun> | There is not one uniform "terminal" though. It is completely true that there is no one single way to clear any arbitrary terminal. |
2023-12-11 14:46:52 +0100 | <Joao003> | true |
2023-12-11 14:46:59 +0100 | <Joao003> | i use windows tho |
2023-12-11 14:47:21 +0100 | <exarkun> | Windows isn't a terminal. It isn't even a terminal emulator. ;) |
2023-12-11 14:47:43 +0100 | <Joao003> | yes ik, but for cmd.exe, what is a reliable tool to clear its console? |
2023-12-11 14:48:10 +0100 | <exarkun> | "cls" |
2023-12-11 14:48:11 +0100 | <Rembane> | Joao003: print "cls\n" and see what happens. :) |
2023-12-11 14:48:42 +0100 | <Joao003> | just prints cls |
2023-12-11 14:49:02 +0100 | <eayus70> | I think powershell and console apps are ANSI compatible if you dont mind using them instead of the old command prompt |
2023-12-11 14:49:20 +0100 | <Joao003> | yeah, cmd.exe is 30 yrs old |
2023-12-11 14:49:44 +0100 | <eayus70> | Maybe `system "cls"` |
2023-12-11 14:49:47 +0100 | <eayus70> | https://hackage.haskell.org/package/process-1.0.1.3/docs/System-Cmd.html |
2023-12-11 14:50:45 +0100 | <mauke> | putStr (replicate 9999 '\n') |
2023-12-11 14:51:34 +0100 | <Joao003> | works, but slow |
2023-12-11 14:51:50 +0100 | <Joao003> | maybe a 150 is enough |
2023-12-11 14:51:58 +0100 | <Joao003> | or even just 100 |
2023-12-11 14:52:07 +0100 | rvalue | (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
2023-12-11 14:52:26 +0100 | rvalue | (~rvalue@user/rvalue) |
2023-12-11 14:52:58 +0100 | <Joao003> | afaik, most people don't have 9999-line high monitors |
2023-12-11 14:53:59 +0100 | <eayus70> | I belive this wont put the cursor at the top however |
2023-12-11 14:54:15 +0100 | <eayus70> | so it is different to "cls" functionally |
2023-12-11 14:54:19 +0100 | <Joao003> | yeah |
2023-12-11 14:54:28 +0100 | <Joao003> | i just tested it |
2023-12-11 14:55:32 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
2023-12-11 14:55:43 +0100 | thegeekinside | (~thegeekin@189.217.90.224) |
2023-12-11 14:55:43 +0100 | igemnace | (~ian@user/igemnace) (Read error: Connection reset by peer) |
2023-12-11 14:55:49 +0100 | shriekingnoise | (~shrieking@186.137.175.87) |
2023-12-11 14:55:57 +0100 | euleritian | (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) |
2023-12-11 14:59:05 +0100 | <ski> | eayus70 : did you try `system' ? |
2023-12-11 14:59:28 +0100 | <Joao003> | <interactive>:9:1: error: Variable not in scope: system |
2023-12-11 14:59:43 +0100 | <Joao003> | % system "clear" |
2023-12-11 14:59:43 +0100 | <yahb2> | <interactive>:45:1: error: ; Variable not in scope: system :: String -> t |
2023-12-11 14:59:48 +0100 | <Joao003> | lol |
2023-12-11 14:59:55 +0100 | <eayus70> | You neen to add the "process" package |
2023-12-11 14:59:55 +0100 | <ski> | <ski> % System.Cmd.system "tput clear" |
2023-12-11 15:00:20 +0100 | <Joao003> | how? using cabal? i don't like using package managers |
2023-12-11 15:00:37 +0100 | <eayus70> | Yeah using cabal |
2023-12-11 15:01:05 +0100 | <ski> | Joao003 : `:set -package process' in GHCi |
2023-12-11 15:01:34 +0100 | <Joao003> | still same error |
2023-12-11 15:01:36 +0100 | <ski> | (or `ghci -package process', when you start it, also works) |
2023-12-11 15:01:48 +0100 | <ski> | you also need to qualify the module path |
2023-12-11 15:01:55 +0100 | <ski> | (or import the module) |
2023-12-11 15:02:10 +0100 | <ski> | % System.Cmd.system "cls" |
2023-12-11 15:02:10 +0100 | <yahb2> | /bin/sh: 1: cls: not found ; ExitFailure 127 |
2023-12-11 15:02:15 +0100 | <ski> | % System.Cmd.system "tput clear" |
2023-12-11 15:02:15 +0100 | <yahb2> | tput: No value for $TERM and no -T specified ; ExitFailure 2 |
2023-12-11 15:06:09 +0100 | <Joao003> | have you ever used (,,) |
2023-12-11 15:07:21 +0100 | eayus | (~eayus@8afbc74e.st-andrews.ac.uk) |
2023-12-11 15:07:30 +0100 | <danse-nr3> | yeah |
2023-12-11 15:07:46 +0100 | <Joao003> | i imagine it being used for a 3d point |
2023-12-11 15:07:59 +0100 | <Joao003> | what about a (,,,) |
2023-12-11 15:08:17 +0100 | <danse-nr3> | the longer, the worse |
2023-12-11 15:08:21 +0100 | <Joao003> | lol |
2023-12-11 15:08:30 +0100 | <Joao003> | ghc supports (,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,) |
2023-12-11 15:08:40 +0100 | <Joao003> | aka a 64-plet |
2023-12-11 15:08:46 +0100 | <ski> | % :ǃ uname -a |
2023-12-11 15:08:46 +0100 | <yahb2> | Linux play-haskell 6.6.2-arch1-1 #1 SMP PREEMPT_DYNAMIC Mon, 20 Nov 2023 23:18:21 +0000 x86_64 x86_64 x86_64 GNU/Linux |
2023-12-11 15:09:15 +0100 | <Joao003> | % :q |
2023-12-11 15:09:15 +0100 | <yahb2> | <bye> |
2023-12-11 15:09:17 +0100 | <Joao003> | lol |
2023-12-11 15:09:21 +0100 | <Joao003> | % 1 |
2023-12-11 15:09:21 +0100 | <yahb2> | 1 |
2023-12-11 15:10:36 +0100 | eayus70 | (~eayus@8afbc74e.st-andrews.ac.uk) (Ping timeout: 250 seconds) |
2023-12-11 15:13:34 +0100 | igemnace | (~ian@user/igemnace) |
2023-12-11 15:16:22 +0100 | <Joao003> | why do type definitions use () instead of Unit? |
2023-12-11 15:17:11 +0100 | <ski> | it's the empty tuple type |
2023-12-11 15:17:11 +0100 | edr | (~edr@user/edr) |
2023-12-11 15:17:38 +0100 | <Joao003> | @hoogle Unit |
2023-12-11 15:17:39 +0100 | <lambdabot> | GHC.Tuple data Unit a |
2023-12-11 15:17:39 +0100 | <lambdabot> | GHC.Tuple Unit :: a -> Unit a |
2023-12-11 15:17:39 +0100 | <lambdabot> | module Graphics.Rendering.Chart.Axis.Unit |
2023-12-11 15:17:56 +0100 | <Joao003> | @hoogle () |
2023-12-11 15:17:56 +0100 | <lambdabot> | GHC.Tuple data () |
2023-12-11 15:17:56 +0100 | <lambdabot> | GHC.Tuple () :: () |
2023-12-11 15:18:02 +0100 | <Joao003> | different... |
2023-12-11 15:18:21 +0100 | <ski> | in the MLs, tuple types `(T,U,V)' are spelled `t * u * v'. the empty tuple type `()' is spelled `unit' |
2023-12-11 15:18:53 +0100 | <ski> | yea, that `Unit' is the "unituple type", a tuple with one component, not zero components (which is what `() |
2023-12-11 15:18:56 +0100 | <ski> | ' has) |
2023-12-11 15:19:53 +0100 | <Joao003> | lemme copy from hackage: "The unit datatype Unit has one non-undefined member, the nullary constructor ()." |
2023-12-11 15:19:56 +0100 | <ski> | - {1 = 2,2 = 1}; |
2023-12-11 15:19:57 +0100 | <ski> | val it = (2,1) : int * int |
2023-12-11 15:20:10 +0100 | <ski> | - {1 = 2}; |
2023-12-11 15:20:12 +0100 | <ski> | val it = {1=2} : {1:int} |
2023-12-11 15:20:21 +0100 | <ski> | - {}; |
2023-12-11 15:20:23 +0100 | <Joao003> | what's t hat |
2023-12-11 15:20:23 +0100 | <ski> | val it = () : unit |
2023-12-11 15:20:26 +0100 | <ski> | that's SML |
2023-12-11 15:20:40 +0100 | <ski> | tuples are records, with field names being positive integers |
2023-12-11 15:21:22 +0100 | <ski> | "The unit datatype Unit has one non-undefined member, the nullary constructor ()." -- that's about the `()' type, not the `Unit' type above in `GHC.Tuple' |
2023-12-11 15:22:22 +0100 | <Joao003> | It says "data Unit" and also says that one of its constructors is () |
2023-12-11 15:22:43 +0100 | <ski> | where ? |
2023-12-11 15:22:58 +0100 | <Joao003> | https://hackage.haskell.org/package/ghc-prim-0.11.0/docs/GHC-Tuple-Prim.html |
2023-12-11 15:23:45 +0100 | danse-nr3 | (~danse@151.19.230.254) (Ping timeout: 252 seconds) |
2023-12-11 15:24:05 +0100 | <Joao003> | also, isn't Solo the 1-tuple datatype? |
2023-12-11 15:25:15 +0100 | <ski> | ok, i suppose `GHC.Tuple.Unit' was renamed into `GHC.Tuple.Solo' |
2023-12-11 15:25:30 +0100 | <ski> | it says "Since: ghc-prim-0.11.0" |
2023-12-11 15:25:44 +0100 | <Joao003> | oh |
2023-12-11 15:25:47 +0100 | <ski> | so it looks like that was probably recently |
2023-12-11 15:25:58 +0100 | <Joao003> | yeah |
2023-12-11 15:34:04 +0100 | <ski> | % $(return (TupE [])) |
2023-12-11 15:34:04 +0100 | <yahb2> | () |
2023-12-11 15:34:08 +0100 | <ski> | % $(return (TupE [Just (VarE 'otherwise)])) |
2023-12-11 15:34:09 +0100 | <yahb2> | Solo True |
2023-12-11 15:34:13 +0100 | <ski> | % :t $(return (TupE [Nothing])) |
2023-12-11 15:34:13 +0100 | <yahb2> | $(return (TupE [Nothing])) :: t -> Solo t |
2023-12-11 15:34:33 +0100 | <Joao003> | the solo type is the most useless thing ever |
2023-12-11 15:37:28 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3341-aec3-516d-6fbd-7275-d6e8.rev.sfr.net) (Ping timeout: 250 seconds) |
2023-12-11 15:38:21 +0100 | <ski> | % case $(return (UnboxedTupE [Just (VarE 'otherwise)])) of (# b #) -> b |
2023-12-11 15:38:21 +0100 | <yahb2> | True |
2023-12-11 15:38:23 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-12-11 15:38:29 +0100 | <ski> | % case $(return (UnboxedTupE [])) of (# #) -> b |
2023-12-11 15:38:29 +0100 | <yahb2> | <interactive>:75:45: error: Variable not in scope: b |
2023-12-11 15:38:33 +0100 | <ski> | % case $(return (UnboxedTupE [])) of (# #) -> () |
2023-12-11 15:38:33 +0100 | <yahb2> | () |
2023-12-11 15:38:41 +0100 | <ski> | % case $(return (UnboxedSumE (VarE 'otherwise) 1 2)) of (# x | #) -> Left x; (# | y #) -> Right y |
2023-12-11 15:38:41 +0100 | <yahb2> | Left True |
2023-12-11 15:38:45 +0100 | <ski> | % case $(return (UnboxedSumE (VarE 'otherwise) 2 2)) of (# x | #) -> Left x; (# | y #) -> Right y |
2023-12-11 15:38:45 +0100 | <yahb2> | Right True |
2023-12-11 15:39:40 +0100 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
2023-12-11 15:39:44 +0100 | alp_ | (~alp@2001:861:e3d6:8f80:c12e:3d55:b6:f405) (Ping timeout: 256 seconds) |
2023-12-11 15:40:05 +0100 | <Joao003> | ski? |
2023-12-11 15:42:50 +0100 | <ski> | hm ? |
2023-12-11 15:43:36 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3341-aec3-516d-6fbd-7275-d6e8.rev.sfr.net) |
2023-12-11 15:44:23 +0100 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 264 seconds) |
2023-12-11 15:47:05 +0100 | <Joao003> | say one thing we need in ghc |
2023-12-11 15:47:55 +0100 | <Joao003> | i think better error messages are needed |
2023-12-11 15:48:01 +0100 | <ski> | @ghc |
2023-12-11 15:48:01 +0100 | <lambdabot> | For basic information, try the `--help' option. |
2023-12-11 15:48:10 +0100 | <ski> | @ghc |
2023-12-11 15:48:11 +0100 | <lambdabot> | the eta-reduction property does not hold |
2023-12-11 15:48:26 +0100 | nate4 | (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
2023-12-11 15:48:48 +0100 | <Joao003> | @ghc |
2023-12-11 15:48:48 +0100 | <lambdabot> | Can't mix generic and non-generic equations for class method |
2023-12-11 15:49:13 +0100 | <Joao003> | this bot can mock ghc lol |
2023-12-11 15:49:37 +0100 | <Joao003> | @help ghc |
2023-12-11 15:49:37 +0100 | <lambdabot> | ghc. Choice quotes from GHC. |
2023-12-11 15:49:47 +0100 | <Joao003> | @ghc |
2023-12-11 15:49:47 +0100 | <lambdabot> | eval_thunk_selector: strange selectee |
2023-12-11 15:49:57 +0100 | <Joao003> | i'm really thonking |
2023-12-11 15:50:02 +0100 | <Joao003> | @ghc |
2023-12-11 15:50:02 +0100 | <lambdabot> | Can't happen |
2023-12-11 15:50:14 +0100 | <Joao003> | will never happen |
2023-12-11 15:50:15 +0100 | <Joao003> | @ghc |
2023-12-11 15:50:15 +0100 | <lambdabot> | No explicit method nor default method |
2023-12-11 15:50:20 +0100 | <Joao003> | @ghc |
2023-12-11 15:50:20 +0100 | <lambdabot> | On Alpha, I can only handle 4 non-floating-point arguments to foreign export dynamic |
2023-12-11 15:50:25 +0100 | <Joao003> | @ghc |
2023-12-11 15:50:25 +0100 | <lambdabot> | GHCi's bytecode generation machinery can't handle 64-bit code properly yet. |
2023-12-11 15:50:30 +0100 | <Joao003> | @ghc |
2023-12-11 15:50:30 +0100 | <lambdabot> | Use -fglasgow-exts to allow multi-parameter classes |
2023-12-11 15:50:47 +0100 | <Joao003> | @ghc |
2023-12-11 15:50:47 +0100 | <lambdabot> | Inferred type is less polymorphic than expected |
2023-12-11 15:52:04 +0100 | <Joao003> | @help |
2023-12-11 15:52:04 +0100 | <lambdabot> | help <command>. Ask for help for <command>. Try 'list' for all commands |
2023-12-11 15:52:08 +0100 | <Joao003> | @list |
2023-12-11 15:52:08 +0100 | <lambdabot> | What module? Try @listmodules for some ideas. |
2023-12-11 15:52:13 +0100 | <Joao003> | @help list |
2023-12-11 15:52:13 +0100 | <lambdabot> | list [module|command]. Show commands for [module] or the module providing [command]. |
2023-12-11 15:53:22 +0100 | nate4 | (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 256 seconds) |
2023-12-11 15:57:47 +0100 | Square2 | (~Square4@user/square) |
2023-12-11 15:58:00 +0100 | danza | (~danza@151.19.230.254) |
2023-12-11 16:01:00 +0100 | blastoise | (~blastoise@205.185.193.149) |
2023-12-11 16:01:15 +0100 | flounders | (~flounders@24.246.176.178) |
2023-12-11 16:03:23 +0100 | danza | (~danza@151.19.230.254) (Ping timeout: 260 seconds) |
2023-12-11 16:09:03 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-12-11 16:09:16 +0100 | euleritian | (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
2023-12-11 16:09:33 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2023-12-11 16:10:14 +0100 | danse-nr3 | (~danse@151.35.255.237) |
2023-12-11 16:12:08 +0100 | eayus | (~eayus@8afbc74e.st-andrews.ac.uk) (Ping timeout: 250 seconds) |
2023-12-11 16:12:31 +0100 | stiell | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 240 seconds) |
2023-12-11 16:15:18 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3341-aec3-516d-6fbd-7275-d6e8.rev.sfr.net) (Remote host closed the connection) |
2023-12-11 16:15:31 +0100 | Sgeo | (~Sgeo@user/sgeo) |
2023-12-11 16:15:49 +0100 | stiell | (~stiell@gateway/tor-sasl/stiell) |
2023-12-11 16:16:05 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds) |
2023-12-11 16:16:51 +0100 | euleritian | (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) |
2023-12-11 16:19:40 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3341-aec3-516d-6fbd-7275-d6e8.rev.sfr.net) |
2023-12-11 16:23:27 +0100 | euleritian | (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
2023-12-11 16:23:44 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2023-12-11 16:25:20 +0100 | akegalj | (~akegalj@78-3-59-204.adsl.net.t-com.hr) (Ping timeout: 252 seconds) |
2023-12-11 16:26:08 +0100 | califax | (~califax@user/califx) (Remote host closed the connection) |
2023-12-11 16:26:54 +0100 | akegalj | (~akegalj@78-1-93-196.adsl.net.t-com.hr) |
2023-12-11 16:27:44 +0100 | califax | (~califax@user/califx) |
2023-12-11 16:29:51 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3341-aec3-516d-6fbd-7275-d6e8.rev.sfr.net) (Remote host closed the connection) |
2023-12-11 16:30:27 +0100 | dwt_ | (~dwt_@2601:2c6:8381:e5c:606f:34a3:7300:6f05) (Ping timeout: 260 seconds) |
2023-12-11 16:30:34 +0100 | cimento | (CO2@gateway/vpn/protonvpn/cimento) (Ping timeout: 260 seconds) |
2023-12-11 16:31:10 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3341-aec3-516d-6fbd-7275-d6e8.rev.sfr.net) |
2023-12-11 16:32:06 +0100 | dwt_ | (~dwt_@2601:2c6:8381:e5c:c917:e876:d8ba:f05f) |
2023-12-11 16:34:02 +0100 | alp_ | (~alp@2001:861:e3d6:8f80:66b0:842b:748c:f4e2) |
2023-12-11 16:35:21 +0100 | akegalj | (~akegalj@78-1-93-196.adsl.net.t-com.hr) (Ping timeout: 245 seconds) |
2023-12-11 16:39:03 +0100 | cimento | (CO2@gateway/vpn/protonvpn/cimento) |
2023-12-11 16:40:31 +0100 | chiselfuse | (~chiselfus@user/chiselfuse) (Ping timeout: 240 seconds) |
2023-12-11 16:42:22 +0100 | akegalj | (~akegalj@95.168.120.43) |
2023-12-11 16:43:05 +0100 | chiselfuse | (~chiselfus@user/chiselfuse) |
2023-12-11 16:46:52 +0100 | xdej | (~xdej@quatramaran.salle-s.org) |
2023-12-11 16:50:14 +0100 | mmhat | (~mmh@p200300f1c702cd13ee086bfffe095315.dip0.t-ipconnect.de) |
2023-12-11 16:50:27 +0100 | akegalj | (~akegalj@95.168.120.43) (Read error: Connection reset by peer) |
2023-12-11 16:53:21 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.1.1) |
2023-12-11 16:53:57 +0100 | Fischmiep | (~Fischmiep@user/Fischmiep) |
2023-12-11 16:59:45 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
2023-12-11 17:01:08 +0100 | cfricke | (~cfricke@user/cfricke) (Quit: WeeChat 4.0.5) |
2023-12-11 17:02:16 +0100 | mmhat | (~mmh@p200300f1c702cd13ee086bfffe095315.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
2023-12-11 17:02:38 +0100 | mmhat | (~mmh@p200300f1c702cdcaee086bfffe095315.dip0.t-ipconnect.de) |
2023-12-11 17:03:24 +0100 | Pixi` | (~Pixi@user/pixi) |
2023-12-11 17:03:50 +0100 | mikess | (~sam@user/mikess) |
2023-12-11 17:05:59 +0100 | Pixi | (~Pixi@user/pixi) (Ping timeout: 264 seconds) |
2023-12-11 17:06:10 +0100 | <Joao003> | i hate the fact that there's min and minimum |
2023-12-11 17:06:42 +0100 | <danse-nr3> | > %t min |
2023-12-11 17:06:44 +0100 | <lambdabot> | <hint>:1:1: error: parse error on input ‘%’ |
2023-12-11 17:06:50 +0100 | <danse-nr3> | % :t min |
2023-12-11 17:06:50 +0100 | <yahb2> | min :: Ord a => a -> a -> a |
2023-12-11 17:06:54 +0100 | <danse-nr3> | % :t minimum |
2023-12-11 17:06:55 +0100 | <yahb2> | minimum :: (Foldable t, Ord a) => t a -> a |
2023-12-11 17:07:00 +0100 | zetef | (~quassel@95.77.17.251) |
2023-12-11 17:07:01 +0100 | thegeekinside | (~thegeekin@189.217.90.224) (Read error: Connection reset by peer) |
2023-12-11 17:07:26 +0100 | <danse-nr3> | you can just use min if you want |
2023-12-11 17:07:32 +0100 | <Joao003> | no |
2023-12-11 17:07:37 +0100 | <Joao003> | min is for 2 arguments |
2023-12-11 17:07:43 +0100 | <Joao003> | while minimum is for foldables |
2023-12-11 17:07:58 +0100 | <Joao003> | % min [1,2,3] |
2023-12-11 17:07:59 +0100 | <yahb2> | <interactive>:87:1: error: ; • No instance for (Show ([Integer] -> [Integer])) ; arising from a use of ‘Yahb2Defs.limitedPrint’ ; (maybe you haven't applied a function to enough... |
2023-12-11 17:08:04 +0100 | <Joao003> | % minimum [1,2,3] |
2023-12-11 17:08:04 +0100 | <yahb2> | 1 |
2023-12-11 17:08:09 +0100 | trev | (~trev@user/trev) (Quit: trev) |
2023-12-11 17:08:58 +0100 | trev | (~trev@user/trev) |
2023-12-11 17:09:52 +0100 | <danse-nr3> | @hoogle (Foldable t, Ord a) => (a -> a -> a) -> t a -> a |
2023-12-11 17:09:53 +0100 | <lambdabot> | Prelude foldr1 :: Foldable t => (a -> a -> a) -> t a -> a |
2023-12-11 17:09:53 +0100 | <lambdabot> | Prelude foldl1 :: Foldable t => (a -> a -> a) -> t a -> a |
2023-12-11 17:09:53 +0100 | <lambdabot> | Data.List foldl1 :: Foldable t => (a -> a -> a) -> t a -> a |
2023-12-11 17:10:15 +0100 | <Joao003> | @src Foldable |
2023-12-11 17:10:15 +0100 | <lambdabot> | Source not found. :( |
2023-12-11 17:10:17 +0100 | <Joao003> | ... |
2023-12-11 17:10:23 +0100 | <Joao003> | @t Foldable |
2023-12-11 17:10:23 +0100 | <lambdabot> | Maybe you meant: tell thank you thanks thesaurus thx tic-tac-toe ticker time todo todo-add todo-delete type v @ ? . |
2023-12-11 17:12:42 +0100 | Joao003 | (~Joao003@190.108.99.207) (Quit: Bye!) |
2023-12-11 17:12:53 +0100 | <danse-nr3> | @hoogle (Foldable t, Ord a, Monoid a) => (a -> a -> a) -> t a -> a |
2023-12-11 17:12:53 +0100 | <lambdabot> | Safe.Foldable foldl1Safe :: (Monoid m, Foldable t) => (m -> m -> m) -> t m -> m |
2023-12-11 17:12:53 +0100 | <lambdabot> | Safe.Foldable foldr1Safe :: (Monoid m, Foldable t) => (m -> m -> m) -> t m -> m |
2023-12-11 17:12:53 +0100 | <lambdabot> | Prelude foldr1 :: Foldable t => (a -> a -> a) -> t a -> a |
2023-12-11 17:15:25 +0100 | mechap | (~mechap@user/mechap) (Quit: WeeChat 4.1.2) |
2023-12-11 17:19:49 +0100 | <glguy> | I boiled down last night's problem into basically two left folds (per part) https://github.com/glguy/advent/blob/main/solutions/src/2023/11.hs |
2023-12-11 17:26:04 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-12-11 17:28:24 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
2023-12-11 17:36:05 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-12-11 17:36:46 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d128:ce35:54e1:65e2) (Remote host closed the connection) |
2023-12-11 17:37:01 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:444f:4a45:c596:a200) |
2023-12-11 17:37:47 +0100 | hasevil | (~hasevil@host-138-37-254-167.qmul.ac.uk) |
2023-12-11 17:38:39 +0100 | <hasevil> | Hi guys, it showing parse error on data. I don't understand what I'm dooing wrong here https://paste.tomsmeding.com/uutJGKZP |
2023-12-11 17:39:13 +0100 | <geekosaur> | on line 13 you're using `data` as a variable, but it's a keyword |
2023-12-11 17:39:19 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 240 seconds) |
2023-12-11 17:44:00 +0100 | <hasevil> | oh, dumb me |
2023-12-11 17:44:01 +0100 | califax | (~califax@user/califx) (Remote host closed the connection) |
2023-12-11 17:44:25 +0100 | califax | (~califax@user/califx) |
2023-12-11 17:46:40 +0100 | hasevil | (~hasevil@host-138-37-254-167.qmul.ac.uk) (Quit: nyaa~) |
2023-12-11 17:49:56 +0100 | finn_elija | (~finn_elij@user/finn-elija/x-0085643) |
2023-12-11 17:49:56 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
2023-12-11 17:49:56 +0100 | finn_elija | FinnElija |
2023-12-11 17:50:40 +0100 | zetef | (~quassel@95.77.17.251) (Ping timeout: 246 seconds) |
2023-12-11 17:57:46 +0100 | <iqubic> | glguy: How are you computing where the blank lines are? |
2023-12-11 18:01:57 +0100 | <glguy> | The blank lines are the space between locations where galaxies are |
2023-12-11 18:03:01 +0100 | <glguy> | So there - here - 1 counts the blank lines |
2023-12-11 18:05:07 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-12-11 18:05:58 +0100 | thegeekinside | (~thegeekin@189.217.90.224) |
2023-12-11 18:05:59 +0100 | danse-nr3 | (~danse@151.35.255.237) (Ping timeout: 264 seconds) |
2023-12-11 18:06:56 +0100 | Joao003 | (~Joao003@190.108.99.207) |
2023-12-11 18:07:25 +0100 | rosco | (~rosco@175.136.152.56) (Quit: Lost terminal) |
2023-12-11 18:07:28 +0100 | <Joao003> | is `(==) :: Char -> Char -> Bool' case sensitive? |
2023-12-11 18:07:51 +0100 | <c_wraith> | yes |
2023-12-11 18:09:06 +0100 | <c_wraith> | I'm curious, though.. WHat made you decide to ask us instead of ghci? We might lie! |
2023-12-11 18:09:42 +0100 | <glguy> | Maybe ghci would lie the first time and then change? |
2023-12-11 18:10:30 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 256 seconds) |
2023-12-11 18:11:14 +0100 | <exarkun> | To ask ghc you'd have to find all Char in the alphabetic category with uppercase and lowercase variations and test each of them, or you wouldn't know if it was _consistently_ case sensitive or insensitive |
2023-12-11 18:11:49 +0100 | <Joao003> | thx, it's because i didn't read the description of a kata |
2023-12-11 18:11:59 +0100 | <Joao003> | on codewars |
2023-12-11 18:11:59 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) |
2023-12-11 18:12:00 +0100 | <Joao003> | srry |
2023-12-11 18:13:08 +0100 | <exarkun> | but you could also think about some laws, which would probably be a more Haskelly solution than asking irc or ghci |
2023-12-11 18:13:41 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) (Remote host closed the connection) |
2023-12-11 18:14:29 +0100 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
2023-12-11 18:14:31 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:444f:4a45:c596:a200) (Remote host closed the connection) |
2023-12-11 18:15:44 +0100 | <iqubic> | glguy: It looks like l is the count of all galaxies that are in the current column or left of it? Is that correct? |
2023-12-11 18:15:57 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:444f:4a45:c596:a200) |
2023-12-11 18:19:00 +0100 | blastoise | (~blastoise@205.185.193.149) (Quit: Leaving) |
2023-12-11 18:20:08 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
2023-12-11 18:22:45 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
2023-12-11 18:24:17 +0100 | <glguy> | yeah |
2023-12-11 18:24:48 +0100 | danza | (~danza@151.35.255.237) |
2023-12-11 18:26:37 +0100 | <int-e> | Space stretches a million times as I walk from here to there. I watch the galaxies as I walk, l behind, and r ahead. |
2023-12-11 18:26:51 +0100 | <Joao003> | what are you talking about |
2023-12-11 18:27:07 +0100 | <int-e> | glguy's code |
2023-12-11 18:27:09 +0100 | <glguy> | https://adventofcode.com/2023/day/11 |
2023-12-11 18:27:36 +0100 | <iqubic> | It's much better than what I did. |
2023-12-11 18:28:23 +0100 | <glguy> | space travel would be just the worst if we had to take manhattan routes to get everywhere. Imagine satellite orbits :-o |
2023-12-11 18:28:40 +0100 | <glguy> | and this 2D situation? We'd have so many collisions |
2023-12-11 18:28:44 +0100 | <int-e> | I missed the big shortcut today, which was to use <rot13>yvarne rkgencbyngvb</rot13> |
2023-12-11 18:28:45 +0100 | <iqubic> | My algorithm is an O(N^2) thing where I compute the distance between each pair of points. |
2023-12-11 18:29:22 +0100 | <int-e> | oh I wrote totally naive code at first too |
2023-12-11 18:29:40 +0100 | <glguy> | yeah, being not clever got me 15th on the first star |
2023-12-11 18:29:40 +0100 | <iqubic> | How does your shortcut help you? |
2023-12-11 18:29:44 +0100 | DerDummNemetzkii | (~John_Ivan@user/john-ivan/x-1515935) (Ping timeout: 256 seconds) |
2023-12-11 18:29:57 +0100 | <int-e> | It explains how people did part 2 in 1-2 minutes. |
2023-12-11 18:30:08 +0100 | <int-e> | (some people) |
2023-12-11 18:30:46 +0100 | darchitect | (~darchitec@2a00:23c6:3584:df01:4cbc:8ff2:73ae:d845) |
2023-12-11 18:31:24 +0100 | <int-e> | Even if they start out with a naive full grid based solution. Which is a good fit for Haskell's lists. |
2023-12-11 18:32:42 +0100 | <iqubic> | My initial code had "expand xss = concatMap (\xs -> if '#' `elem` xs then [xs] else [xs, xs]" and "expanded = expand . transposs . expand . lines" |
2023-12-11 18:33:02 +0100 | <int-e> | Yeah I had something like that too. |
2023-12-11 18:33:54 +0100 | <iqubic> | The formatting is a bit off there. I should I have closed the lambda on the concatMap. But you get the idea. |
2023-12-11 18:34:08 +0100 | <int-e> | You also typo-d "transpose". |
2023-12-11 18:35:00 +0100 | <Joao003> | yo you just got me into advent of code (i'm coding in python though) |
2023-12-11 18:35:15 +0100 | <iqubic> | So I did. I usually have LSP tell me about those issues. |
2023-12-11 18:36:17 +0100 | <darchitect> | hey guys - do you think a sufficiently expressive type system can be a replacement to unit tests? |
2023-12-11 18:36:27 +0100 | <glguy> | nope |
2023-12-11 18:36:33 +0100 | <darchitect> | P.S. I'm a newb in functinal progrmming |
2023-12-11 18:36:49 +0100 | <darchitect> | glguy: I guess I was going after a more explanatory answer :( |
2023-12-11 18:36:55 +0100 | <iqubic> | Yeah. Unit tests are always gonna be needed. |
2023-12-11 18:36:57 +0100 | <monochrom> | Yes, but so expressive, you will give up type inference. |
2023-12-11 18:37:02 +0100 | <probie> | A sufficiently expressive type system _can_ be a replacement to unit tests |
2023-12-11 18:37:10 +0100 | <probie> | You just put the fact that the unit test passes in the type |
2023-12-11 18:37:23 +0100 | aruns | (~aruns@user/aruns) |
2023-12-11 18:37:38 +0100 | <int-e> | Even if your type system is so needy, I mean dependent, that it entails proofs of correctness, you'll still want to check that the properties that the types encode do what you want. |
2023-12-11 18:37:42 +0100 | <monochrom> | In fact, you will give up proof inference. That's right, you go all out write correctness proofs in the type system, that's how you replace tests. |
2023-12-11 18:38:13 +0100 | <glguy> | proofs don't even really replace unit tests |
2023-12-11 18:38:20 +0100 | <glguy> | YOu still need to check what it is you actually proved |
2023-12-11 18:38:37 +0100 | <glguy> | properties can be wrong, too |
2023-12-11 18:39:07 +0100 | <ski> | darchitect : property-based testing can be quite nice |
2023-12-11 18:39:14 +0100 | <int-e> | . o O ( In another universe it's proofs all the way down. ) |
2023-12-11 18:39:17 +0100 | <darchitect> | no I guess I meant that - in light of current LLM developments you can easily have LLMs write tests based on your type and then implement the function that passes the tests with some guidance on whether you want your program to be readable/fast/memory-efficient etc.. and then they would just do it |
2023-12-11 18:39:44 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-12-11 18:39:44 +0100 | <glguy> | You generally can't generate unit tests from types |
2023-12-11 18:39:56 +0100 | <glguy> | (at least not in a useful way) |
2023-12-11 18:39:58 +0100 | <int-e> | And also... so you'll still have tests? |
2023-12-11 18:40:12 +0100 | <darchitect> | yeah but you won't have to write them |
2023-12-11 18:40:31 +0100 | <int-e> | I wouldn't get my hopes up. |
2023-12-11 18:40:32 +0100 | <probie> | but that's not replacing them, that's just outsourcing them |
2023-12-11 18:40:39 +0100 | <darchitect> | yeah to a machine |
2023-12-11 18:40:41 +0100 | <monochrom> | That's interesting. Now we have to prove that the generated tests are correct! |
2023-12-11 18:41:02 +0100 | <int-e> | And interesting! |
2023-12-11 18:41:29 +0100 | <glguy> | unit tests generally test things that the types don't check or even indicate |
2023-12-11 18:41:31 +0100 | <int-e> | (We can already automate throwing a million random tests at code. But we have a harder time automating covering all corner cases.) |
2023-12-11 18:42:06 +0100 | <int-e> | (Kerword fuzzing... I think I've read about people coupling that with SMT solvers to get more coverage.) |
2023-12-11 18:42:18 +0100 | <int-e> | Ker -> Key |
2023-12-11 18:42:51 +0100 | <darchitect> | I mainly started teh conversation because I work in ML and I feel like that LLMs will never replace the necessity to express your thoughts with mathematical precision not just using natural language. So I am wondering what would the role be for LLMs in cases where you do need to express precisely what you need to happen and for now I think using the type system as spec and letting the model |
2023-12-11 18:42:53 +0100 | <darchitect> | implement the code, then write tests based off of the function and our job would be to decide whether the tests are all covered... |
2023-12-11 18:43:27 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 256 seconds) |
2023-12-11 18:43:27 +0100 | <darchitect> | I don't know if I am making too much sense here just thinking out loud |
2023-12-11 18:44:00 +0100 | <int-e> | The role of LLMs will be to fool people into thinking that they've understood a specification... until the bug reports come pouring in. |
2023-12-11 18:44:08 +0100 | <monochrom> | It is an open question because there is no data on training LLMs on formulas instead of prose. |
2023-12-11 18:44:24 +0100 | <iqubic> | Let's say you wrote a function "rev :: [a] -> [a]" to reverse lists. How would you verify that your code is actually doing the right thing? |
2023-12-11 18:44:37 +0100 | <darchitect> | if you were able to encode the ordering in the type you could |
2023-12-11 18:44:47 +0100 | <dminuoso_> | int-e │ The role of LLMs will be to fool people into thinking that they've understood a specification... until the bug reports come pouring in. |
2023-12-11 18:44:47 +0100 | <int-e> | I believe that LLMs (in their current state) do not have a sufficiently deep feedback loop for formal reasoning. |
2023-12-11 18:44:58 +0100 | <dminuoso_> | And this is different from actual math publications exactly.. how? |
2023-12-11 18:45:05 +0100 | <monochrom> | OK I guess Microsoft Copilot is data on training an LLM on code. That's something. |
2023-12-11 18:45:08 +0100 | <int-e> | But they make excellent electric monks. |
2023-12-11 18:45:17 +0100 | <ski> | darchitect : Ocaml or SML ? |
2023-12-11 18:45:34 +0100 | <monochrom> | (The result is not great.) |
2023-12-11 18:45:34 +0100 | <darchitect> | ski: just any functional language relaly |
2023-12-11 18:45:44 +0100 | <ski> | yes, but you said ML |
2023-12-11 18:46:05 +0100 | <int-e> | monochrom: I imagine it tends to work for boilerplate, which is like 99% of all code these days. :P |
2023-12-11 18:46:07 +0100 | <darchitect> | ski: no no Machine Learning, sorry forgot I'm not in an AI chat :D |
2023-12-11 18:46:22 +0100 | <ski> | oh .. not Machine Language, either, then .. :/ |
2023-12-11 18:46:30 +0100 | <monochrom> | My LLM says that if both "ML" and "LLM" appear in the same sentence then "ML" means machine learning. :D |
2023-12-11 18:46:35 +0100 | <ski> | (or Mailing Lists .. guess there's a bunch) |
2023-12-11 18:46:42 +0100 | <int-e> | monochrom: And because we have LLMs now we can afford writing even more boilerplate code! |
2023-12-11 18:46:47 +0100 | TheCoffeMaker | (~TheCoffeM@user/thecoffemaker) (Ping timeout: 264 seconds) |
2023-12-11 18:46:55 +0100 | <int-e> | Productivity is going to go through the roof. |
2023-12-11 18:47:03 +0100 | <dminuoso_> | I mean when I make a merge request to some github repo, my role too is to fool people into thinking Ive understood their code and that my code adds some value. |
2023-12-11 18:47:07 +0100 | ski | . o O ( more places for bugs to hide in. luvly jubly ! ) |
2023-12-11 18:47:10 +0100 | <monochrom> | This is one more reason why programming is a scam. |
2023-12-11 18:47:17 +0100 | <dminuoso_> | With something like GHC there's a lot of "fooling" in the way you phrase and present your changes. |
2023-12-11 18:47:28 +0100 | <int-e> | (productivity is, of course, measured in lines of code per day) |
2023-12-11 18:47:32 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:444f:4a45:c596:a200) (Remote host closed the connection) |
2023-12-11 18:47:58 +0100 | <monochrom> | Previously, I already said that lack of static type checking is already a scam because you are hiding bugs from the user at pay time. |
2023-12-11 18:48:07 +0100 | <darchitect> | I still don't see how a probabilistic model can replace programmers |
2023-12-11 18:48:20 +0100 | <monochrom> | Now it is a scam the second time because you get paid to write boilerplate code. |
2023-12-11 18:48:20 +0100 | TheCoffeMaker | (~TheCoffeM@user/thecoffemaker) |
2023-12-11 18:48:21 +0100 | <dminuoso_> | darchitect: Programers themselves prove to be probabilitistic models too. |
2023-12-11 18:48:21 +0100 | <darchitect> | at some point you just need to be specific on what you want to do to the last detail |
2023-12-11 18:48:39 +0100 | <dminuoso_> | Its just that currently some individuals tend to have better training. |
2023-12-11 18:49:09 +0100 | <ski> | and perhaps somewhat better judgement |
2023-12-11 18:49:21 +0100 | <EvanR> | average number of "wtfs" per minute in code review |
2023-12-11 18:49:33 +0100 | <darchitect> | I would find it weird to have an AI model write the spec for an airplane based off of text from the internet :D |
2023-12-11 18:49:35 +0100 | <int-e> | dminuoso_: The proper way to read a math publication is to take the guidance of the text and follow the formal reasoning steps yourself with a critical eye. I guess that's similar to how you interact with an LLM, but with a math paper there's a chance that the author actually reasoned through the things they wrote about. |
2023-12-11 18:49:43 +0100 | John_Ivan | (~John_Ivan@user/john-ivan/x-1515935) |
2023-12-11 18:50:45 +0100 | <tromp> | has any LLM been tried on solving AoC puzzles? |
2023-12-11 18:51:54 +0100 | <geekosaur> | no doubt ssomeone's using it now |
2023-12-11 18:51:55 +0100 | <EvanR> | probably, though it's against the rules this year |
2023-12-11 18:52:01 +0100 | <int-e> | Specifically? Hmm. There's all this fine tuning of LLMs going on which is relatively cheap... somebody must have tried that with AoC. |
2023-12-11 18:52:52 +0100 | <tromp> | Oh, I see it now in the About section: Can I use AI to get on the global leaderboard? |
2023-12-11 18:53:16 +0100 | <int-e> | Yeah, direct link: https://adventofcode.com/about#faq_ai_leaderboard |
2023-12-11 18:53:36 +0100 | <int-e> | Note that they don't care once the top 100 is filled up. |
2023-12-11 18:54:01 +0100 | <int-e> | (Well, I guess they care, but who would want to police that...) |
2023-12-11 18:54:27 +0100 | <tromp> | it would be nice if they simply allowed ppl to sign up an AI, which would keep them out of the human leaderboard |
2023-12-11 18:54:36 +0100 | <darchitect> | will type theory still be a thing of the future ? As in what would it's main use be in programming if we're all writing "good-enough" programs with lots of empirical tests and no proofs |
2023-12-11 18:54:45 +0100 | <darchitect> | in the future * |
2023-12-11 18:54:48 +0100 | <tromp> | and show them on an exclusive and separate AI leaderboard |
2023-12-11 18:55:05 +0100 | <EvanR> | it makes sense to say "if you want an AI contest try another contest" |
2023-12-11 18:55:29 +0100 | <EvanR> | since it takes a lot of human work to put this one together |
2023-12-11 18:55:33 +0100 | <Joao003> | i installed deskpins just to pin my irc client |
2023-12-11 18:55:48 +0100 | <monochrom> | We don't all write good-enough programs. |
2023-12-11 18:56:06 +0100 | <tromp> | doesn't a separate AI leaderboard make more sense? More data from same design effort |
2023-12-11 18:56:06 +0100 | <dminuoso_> | int-e: This is no different from say a program. Unless this went through a automated theorem prover (whose correctness Ill just assume axiomatically for the sake of discussion), the mere fact that you cannot trust the author himself is why you cant necessarily trust your personal judgement. Its how various Jacobian Conjecture were accepted for a while, despite ultimately being proven wrong. |
2023-12-11 18:56:12 +0100 | <int-e> | monochrom: not-to-bad is where the money's at ;) |
2023-12-11 18:56:20 +0100 | <monochrom> | heehee |
2023-12-11 18:56:23 +0100 | <int-e> | *too |
2023-12-11 18:56:25 +0100 | <dminuoso_> | We're just deeply flawed - its just that especially mathematicians strike to reduce the errors. |
2023-12-11 18:56:26 +0100 | <EvanR> | well some of the questions don't have randomly generated input data |
2023-12-11 18:56:36 +0100 | <dminuoso_> | No different from LLM engineers trying to reduce their models errors. |
2023-12-11 18:56:39 +0100 | <monochrom> | But there are niches that insist on proofs. |
2023-12-11 18:56:42 +0100 | <int-e> | (but that was a good place for inserting a typo) |
2023-12-11 18:56:43 +0100 | <EvanR> | AI on those would disrupt the humans |
2023-12-11 18:56:52 +0100 | Square | (~Square@user/square) |
2023-12-11 18:56:58 +0100 | Square2 | (~Square4@user/square) (Ping timeout: 256 seconds) |
2023-12-11 18:57:00 +0100 | <dminuoso_> | monochrom: But how do you know correctness of a proof! |
2023-12-11 18:57:03 +0100 | <EvanR> | the first AI to reach the goal solves it for everyone |
2023-12-11 18:57:23 +0100 | <int-e> | dminuoso_: Yes, math is an empirical science where the experiment is taking a paper and letting an expert in its respective field read it. |
2023-12-11 18:57:38 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
2023-12-11 18:57:53 +0100 | <monochrom> | Well yeah their real goal is extremely high confidence, and they have chosen proofs as the means. |
2023-12-11 18:57:53 +0100 | <ski> | math is also an aesthetic endeavor |
2023-12-11 18:58:02 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
2023-12-11 18:58:09 +0100 | <int-e> | But no, LLMs at this point cannot sufficiently imitate a mathematician to produce papers that are worth subjecting to that experiment. |
2023-12-11 18:58:47 +0100 | <dminuoso_> | Not yet, anyhow. |
2023-12-11 18:58:47 +0100 | <Franciman> | int-e: i think they can do fine enough in the history of mathematics |
2023-12-11 18:58:51 +0100 | <int-e> | Will future LLMs be different? Maybe. They'll need a different architecture. |
2023-12-11 18:59:40 +0100 | <monochrom> | You know, I'm very cynical about human abilities too. |
2023-12-11 18:59:52 +0100 | <dminuoso_> | In fact Im going to argue that in general scientific publications there is a feedback loop that trains scientists to act precisely like LLM: Try and convince people about your idea being right. Whether it is right is often irrelevant: |
2023-12-11 18:59:58 +0100 | <int-e> | ("large language model" is a stupidly generic term. And stupid in that it sounds as if it's just about size.) |
2023-12-11 19:00:02 +0100 | <dminuoso_> | Impact factor of a Nature or Science publication: Thats what counts. |
2023-12-11 19:00:14 +0100 | <dminuoso_> | Not correctness of science. |
2023-12-11 19:00:17 +0100 | <monochrom> | My model of human thought: A backend that's correct >70% of the time, and a not-gate for the front end. |
2023-12-11 19:00:41 +0100 | <monochrom> | So yes I agree that LLMs are stupid but humans are beyond stupid. |
2023-12-11 19:01:26 +0100 | <monochrom> | At present, LLMs already make better politicians than human politicians. |
2023-12-11 19:02:07 +0100 | <EvanR> | on a practical matter they make better sports writers |
2023-12-11 19:02:14 +0100 | <trev> | monochrom: careful...that means they can lie and steal better too |
2023-12-11 19:02:17 +0100 | <monochrom> | (Well, at least until some robot overlord changes politics from "verbally convincing" to "actual proofs".) |
2023-12-11 19:02:28 +0100 | <dminuoso_> | trev: Oh ChatGPT has no problem with confabulating the world. |
2023-12-11 19:02:32 +0100 | <trev> | lolz |
2023-12-11 19:02:35 +0100 | araujo | (~araujo@216.73.163.11) (Ping timeout: 260 seconds) |
2023-12-11 19:02:58 +0100 | <trev> | it's so confident |
2023-12-11 19:03:10 +0100 | <dminuoso_> | The kind of stories you see, where it confabulates imaginary papers, quoting them and describing them in great detail... |
2023-12-11 19:03:25 +0100 | <dminuoso_> | Describing history events that never occured.. |
2023-12-11 19:03:43 +0100 | <dminuoso_> | Id say ChatGPT is ripe to evolve into politics. |
2023-12-11 19:03:57 +0100 | <ski> | or to get into textbook writing |
2023-12-11 19:04:11 +0100 | <EvanR> | there was an AI generated political ad a few months back, kind of disturbing |
2023-12-11 19:04:14 +0100 | <darchitect> | do you reckon if we had all math encapsulated in a proof assistant and then the ai explored possible reasoing paths to come to a proof, then I guess we can the proof for truth |
2023-12-11 19:04:28 +0100 | <dminuoso_> | darchitect: This is already being explored by Google at least. |
2023-12-11 19:04:46 +0100 | <darchitect> | are you getting this from the latest reasoning example for Gemini ? |
2023-12-11 19:06:35 +0100 | <monochrom> | Yeah a proof assistant is great at checking an alleged proof, an LLM is great at creating an alleged proof, the two of them yelling at each other can get things done right, afterall that's how I work too. |
2023-12-11 19:06:56 +0100 | <monochrom> | "I argue with myself all the time. It adds sparks to my arguments." |
2023-12-11 19:06:58 +0100 | <dminuoso_> | darchitect: As just a single small excerpt: https://www.nature.com/articles/s41586-022-05172-4 |
2023-12-11 19:07:49 +0100 | <monochrom> | There are also people hooking up ChatGPT with Mathematica or Wolfram Alpha. |
2023-12-11 19:08:16 +0100 | <dminuoso_> | Glue code written by ChatGPT? |
2023-12-11 19:09:06 +0100 | <darchitect> | yeah I mean everything we do in our heads is ultimately search, question is whether reinforcement learning + LLM is what we really do in our heads |
2023-12-11 19:09:40 +0100 | <darchitect> | or actually the question is - is it better to do RL + LLM or is our mind better |
2023-12-11 19:09:55 +0100 | <dminuoso_> | Id start by asking the question: How do you even measure "better"? |
2023-12-11 19:10:32 +0100 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
2023-12-11 19:11:07 +0100 | <duncan> | A backend that's correct 70% of the time is.. hideously bad |
2023-12-11 19:11:09 +0100 | <darchitect> | well in terms of producing faster code for example, or shorter and faster code |
2023-12-11 19:11:18 +0100 | <dminuoso_> | Take Copilot and the latest 10,000 internal junior developer issues at Microsoft. If Copilot can fix those bugs while costing less on average (in terms of service outages, or human costs involved in fixing broken systems) - is it better than a junior developer? |
2023-12-11 19:11:22 +0100 | gmg | (~user@user/gehmehgeh) |
2023-12-11 19:11:27 +0100 | <dminuoso_> | From a business perspective: it probably is. |
2023-12-11 19:11:39 +0100 | <darchitect> | dminuoso_: yeah deffinitely |
2023-12-11 19:11:41 +0100 | <Rembane> | I wonder how much it will slow down development on those code bases. |
2023-12-11 19:11:58 +0100 | <darchitect> | dminuoso_: I was talking more about new math or for mission-critical systems programming |
2023-12-11 19:12:23 +0100 | <darchitect> | is there a way to get the LLMs to be better than humans or is it a fundamental barier to AI |
2023-12-11 19:12:43 +0100 | <dminuoso_> | Look at SpaceX, they use an awful lot of C++ in their systems - not the primary candidate for proven and reliable hard real time systems if you asked anyone from 20 years ago. |
2023-12-11 19:13:00 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3341-aec3-516d-6fbd-7275-d6e8.rev.sfr.net) (Remote host closed the connection) |
2023-12-11 19:13:04 +0100 | <dminuoso_> | But it seems to work? |
2023-12-11 19:13:17 +0100 | <duncan> | darchitect: if you are asking "is there a way to get the LLMs to be better than humans", you have a fatal issue of problem specification |
2023-12-11 19:14:07 +0100 | <duncan> | It's the equivalent of consultants criticising the technical people for focusing on data management instead of getting on and doing the real work of modelling |
2023-12-11 19:14:46 +0100 | <dminuoso_> | We already live in a world where domain specific machines are better than humans. Robot arms are faster and more precise than human arms. Pumps have higher throughput than a person with a bucket. Neural networks can recognize writing with a much higher speed and precision than average humans. |
2023-12-11 19:15:35 +0100 | <duncan> | sure, and the neural networks not infrequently don't perform better than linear regression. touché? |
2023-12-11 19:16:11 +0100 | <dminuoso_> | Sorry, too many negatives in there. |
2023-12-11 19:16:24 +0100 | <dminuoso_> | My neural net cannot process this. >:) |
2023-12-11 19:16:33 +0100 | <darchitect> | yeah true, I guess what I'm really getting at is this - For some programs, expressing your throughts precisely will still be necessary, because we are the agents that "will things" and models are things that bring them "into being", what is the future of programming? Will there be programs that NEED to be written in code as opposed to explained in a natural language ? If not, then the robots can |
2023-12-11 19:16:34 +0100 | <darchitect> | just write assembly because nobody needs to read their code if we know it's correct and it's going to run with "sufficient reliability" |
2023-12-11 19:16:40 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:444f:4a45:c596:a200) |
2023-12-11 19:17:14 +0100 | <int-e> | what |
2023-12-11 19:17:30 +0100 | <duncan> | darchitect: ask yourself, does this pass the "so what" test |
2023-12-11 19:17:31 +0100 | <dminuoso_> | My biggest issue is having no answers when my girlfriend asks me how to deal with students submitting homework solutions that were seemingly produced by ChatGPT. |
2023-12-11 19:17:33 +0100 | <int-e> | higher level languages *structure* programs |
2023-12-11 19:17:36 +0100 | <darchitect> | sorry not great enlgish here |
2023-12-11 19:18:20 +0100 | <darchitect> | int-e: simplified - does PL research have any value if we go in the direction of full on AI ? |
2023-12-11 19:18:25 +0100 | <int-e> | It's not just about readability, it's about hiding complexity and providing layers of abstraction. |
2023-12-11 19:18:32 +0100 | <int-e> | Yes, it does. |
2023-12-11 19:20:29 +0100 | <darchitect> | int-e: Right, but in this case - don't we all just need to build 1 good language the machines speak and that's it. They can just forever optimize on it because the data will grow and grow. |
2023-12-11 19:20:51 +0100 | Tuplanolla | (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) |
2023-12-11 19:21:12 +0100 | <ski> | dminuoso_ : tell her to ask them to explain it, in person ? |
2023-12-11 19:21:19 +0100 | <int-e> | /If/ that ever happens, that would just mean they'd do their own PL research, at least when translated to human terms. |
2023-12-11 19:21:29 +0100 | tzh | (~tzh@c-71-193-181-0.hsd1.or.comcast.net) |
2023-12-11 19:21:29 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-12-11 19:22:48 +0100 | <dminuoso_> | ski: The student denies, improves their ChatGPT prompt the next time. The real issue isnt necessarily the single incident, but rather the impact on learning. |
2023-12-11 19:22:55 +0100 | <ski> | dminuoso_ : what if there won't be as many junior developers who get enough experience to develop past that ? |
2023-12-11 19:23:20 +0100 | <darchitect> | int-e: well why would we need to hide complexity in this case, if they will do PL research as an emergent feature of having trillions of neurons |
2023-12-11 19:23:48 +0100 | <ski> | dminuoso_ : yea, ignore whether they actually used ChatGPT to produce it. ask them to explain how it works |
2023-12-11 19:23:56 +0100 | <ski> | in person |
2023-12-11 19:24:10 +0100 | <dminuoso_> | ski: Like I said, the deeper problem isnt how to reveal someone who used it. |
2023-12-11 19:24:29 +0100 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
2023-12-11 19:24:34 +0100 | <dminuoso_> | Its just that the tool has become to easily accessible, that this is slowly having an impact on student learning. |
2023-12-11 19:24:39 +0100 | <dminuoso_> | Not in a good way. |
2023-12-11 19:24:42 +0100 | <ski> | well, if ChatGPT wrote the code, then ChatGPT should earn the grade, no ? |
2023-12-11 19:24:44 +0100 | <dminuoso_> | At least in heir classes. |
2023-12-11 19:24:52 +0100 | <dminuoso_> | ski: This is Biology, mind you. |
2023-12-11 19:25:02 +0100 | <ski> | mhm |
2023-12-11 19:25:41 +0100 | ski | . o O ( "To Heir or not to Heir" -- some King's Quest game (IV ?) ) |
2023-12-11 19:26:01 +0100 | <int-e> | darchitect: You have way more faith in the power of big numbers than I do. |
2023-12-11 19:26:08 +0100 | mrmr15533 | (~mrmr@user/mrmr) |
2023-12-11 19:26:21 +0100 | <dminuoso_> | Prague University has stopped requiring written Bachelor thesis - though there's more facettes to this. However, the advance of language models tipped the scale. |
2023-12-11 19:26:58 +0100 | <dminuoso_> | Perhaps in 20 years from now, we will have changed education systems to cope with such tools. |
2023-12-11 19:27:06 +0100 | <dminuoso_> | But education changes rather slowly. |
2023-12-11 19:27:32 +0100 | <darchitect> | int-e: no, no I don't I think these are just probabilistic machines after all and I don't think they are doing anything we're doing in our heads, but I just want to have a more precise confirmation (or refutal) to my own thinking. |
2023-12-11 19:27:35 +0100 | <ski> | well .. i do guess, with podcasts and the like, more people have started to focus more again on auditory learning, over visual learning |
2023-12-11 19:27:39 +0100 | ft | (~ft@p3e9bc784.dip0.t-ipconnect.de) |
2023-12-11 19:27:46 +0100 | <ski> | (which was more the case, before the printing press) |
2023-12-11 19:28:30 +0100 | <EvanR> | makes sense, the percent of human population stuck in traffic increases |
2023-12-11 19:29:15 +0100 | <darchitect> | int-e: I really want to continue studying PL design, but in my mind I am always thinking whether I should study the classic PL design or I should study PL design the machines will find useful one day... or I've probably had too much tea today |
2023-12-11 19:29:18 +0100 | <darchitect> | :d |
2023-12-11 19:30:04 +0100 | alp_ | (~alp@2001:861:e3d6:8f80:66b0:842b:748c:f4e2) (Ping timeout: 246 seconds) |
2023-12-11 19:30:05 +0100 | <ski> | (e.g. with "mind/memory castle/palace/journey/space"/"method of loci". <https://en.wikipedia.org/wiki/Mind_palace> being used since ancient times) |
2023-12-11 19:30:12 +0100 | <int-e> | darchitect: If these things reason in any way like humans do, they will need layers of abstraction to have a fighting chance against bugs. If they don't then any speculation that I can hope to offer is completely meaningless. This isn't even philosophical anymore, it's becoming a matter of beliefs, so it's bascially religious. |
2023-12-11 19:30:32 +0100 | <ephemient> | https://youtu.be/rhgwIhB58PA "The Biggest Myth In Education. You are not a visual learner — learning styles are a stubborn myth." |
2023-12-11 19:32:01 +0100 | <darchitect> | int-e: yeah I agree.. |
2023-12-11 19:32:49 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3341-aec3-516d-6fbd-7275-d6e8.rev.sfr.net) |
2023-12-11 19:33:54 +0100 | <darchitect> | int-e: I wonder if there is any research of using LLMs on doing just that -> getting a program in a typed lambda calculus and asking it to generate the abstractions it thinks are most useful, but then I presume it would just regurgitate something it read on reddit or github :( |
2023-12-11 19:36:28 +0100 | ski | . o O ( "Autism, Academics, and Animals | Dr. Temple Grandin" <https://www.youtube.com/watch?v=XYZP1wuGBD8#t=3m8s> (re different kinds of thinkers, verbal, object-visual, visual-spatial .. and other things, like lack of hands-on shops leading to wear and tear of machinery, and about improvement of animal handling in meat processing) ) |
2023-12-11 19:37:05 +0100 | qqq | (~qqq@92.43.167.61) |
2023-12-11 19:38:17 +0100 | wagle | (~wagle@quassel.wagle.io) (Quit: http://quassel-irc.org - Chat comfortably. Anywhere.) |
2023-12-11 19:38:35 +0100 | wagle | (~wagle@quassel.wagle.io) |
2023-12-11 19:38:40 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3341-aec3-516d-6fbd-7275-d6e8.rev.sfr.net) (Remote host closed the connection) |
2023-12-11 19:39:00 +0100 | wagle | (~wagle@quassel.wagle.io) (Client Quit) |
2023-12-11 19:39:52 +0100 | alexherbo2 | (~alexherbo@60.37.22.93.rev.sfr.net) |
2023-12-11 19:39:52 +0100 | wagle | (~wagle@quassel.wagle.io) |
2023-12-11 19:43:22 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 246 seconds) |
2023-12-11 19:44:36 +0100 | danik292 | (~danik292@109-81-93-115.rct.o2.cz) |
2023-12-11 19:48:00 +0100 | mechap | (~mechap@user/mechap) |
2023-12-11 19:48:00 +0100 | danik292 | (~danik292@109-81-93-115.rct.o2.cz) (Client Quit) |
2023-12-11 19:49:56 +0100 | nate4 | (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
2023-12-11 19:52:32 +0100 | danik292 | (~danik292@109-81-93-115.rct.o2.cz) |
2023-12-11 19:54:51 +0100 | nate4 | (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 256 seconds) |
2023-12-11 19:57:50 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
2023-12-11 19:59:06 +0100 | bratwurst | (~blaadsfa@2604:3d09:2083:a200:216:3eff:fe5a:a1f8) |
2023-12-11 20:00:32 +0100 | bratwurst | (~blaadsfa@2604:3d09:2083:a200:216:3eff:fe5a:a1f8) (Client Quit) |
2023-12-11 20:03:41 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 252 seconds) |
2023-12-11 20:04:57 +0100 | danik292 | (~danik292@109-81-93-115.rct.o2.cz) (Quit: Client closed) |
2023-12-11 20:06:13 +0100 | danza | (~danza@151.35.255.237) (Read error: Connection reset by peer) |
2023-12-11 20:07:22 +0100 | danik292 | (~danik292@109-81-93-115.rct.o2.cz) |
2023-12-11 20:15:16 +0100 | danik292 | (~danik292@109-81-93-115.rct.o2.cz) (Quit: Client closed) |
2023-12-11 20:16:27 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
2023-12-11 20:18:01 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-12-11 20:19:16 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
2023-12-11 20:19:45 +0100 | John_Ivan | (~John_Ivan@user/john-ivan/x-1515935) (Quit: Disrupting the dragon's slumber one time too often shall eventually bestow upon all an empirical and indiscriminate conflagration that will last for all goddamn eternity.) |
2023-12-11 20:20:46 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 245 seconds) |
2023-12-11 20:20:58 +0100 | danza | (~danza@151.37.252.39) |
2023-12-11 20:26:49 +0100 | danik292 | (~danik292@109-81-93-115.rct.o2.cz) |
2023-12-11 20:27:01 +0100 | danik292 | (~danik292@109-81-93-115.rct.o2.cz) (Client Quit) |
2023-12-11 20:28:21 +0100 | bilegeek | (~bilegeek@2600:1008:b08b:7355:7869:26c7:cf9e:bac4) |
2023-12-11 20:31:18 +0100 | mikess | (~sam@user/mikess) (Quit: leaving) |
2023-12-11 20:33:19 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
2023-12-11 20:39:11 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 260 seconds) |
2023-12-11 20:39:16 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:444f:4a45:c596:a200) (Remote host closed the connection) |
2023-12-11 20:43:33 +0100 | johnw_ | (~johnw@69.62.242.138) |
2023-12-11 20:43:46 +0100 | Guest25 | (~Guest25@46.39.53.144) |
2023-12-11 20:45:51 +0100 | johnw | (~johnw@69.62.242.138) (Ping timeout: 256 seconds) |
2023-12-11 20:47:45 +0100 | alp_ | (~alp@2001:861:e3d6:8f80:c150:fb83:d53f:eaf2) |
2023-12-11 20:49:09 +0100 | Guest25 | (~Guest25@46.39.53.144) (Quit: Client closed) |
2023-12-11 20:51:29 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
2023-12-11 20:53:17 +0100 | Joao003 | (~Joao003@190.108.99.207) (Bye!) |
2023-12-11 20:53:27 +0100 | Joao003 | (~Joao003@190.108.99.207) |
2023-12-11 21:03:41 +0100 | aruns | (~aruns@user/aruns) (Ping timeout: 240 seconds) |
2023-12-11 21:05:23 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-12-11 21:10:28 +0100 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht) |
2023-12-11 21:10:39 +0100 | [_] | (~itchyjunk@user/itchyjunk/x-7353470) |
2023-12-11 21:11:15 +0100 | fr33domlover | (~fr33domlo@towards.vision) (Quit: The Lounge - https://thelounge.chat) |
2023-12-11 21:14:44 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 268 seconds) |
2023-12-11 21:14:47 +0100 | fr33domlover | (~fr33domlo@towards.vision) |
2023-12-11 21:16:36 +0100 | jargon | (~jargon@32.sub-174-238-226.myvzw.com) |
2023-12-11 21:19:08 +0100 | mjs2600 | (~mjs2600@c-174-169-225-239.hsd1.vt.comcast.net) (Quit: ZNC 1.8.2 - https://znc.in) |
2023-12-11 21:19:37 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:444f:4a45:c596:a200) |
2023-12-11 21:19:52 +0100 | cwdar^ | (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
2023-12-11 21:21:15 +0100 | ec | (~ec@gateway/tor-sasl/ec) |
2023-12-11 21:22:07 +0100 | Maeda | (~Maeda@91-161-10-149.subs.proxad.net) (Quit: stop) |
2023-12-11 21:23:23 +0100 | mjs2600 | (~mjs2600@c-174-169-225-239.hsd1.vt.comcast.net) |
2023-12-11 21:24:10 +0100 | alexherbo2 | (~alexherbo@60.37.22.93.rev.sfr.net) (Remote host closed the connection) |
2023-12-11 21:24:26 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3341-aec3-39e5-e6a4-25fc-cb4b.rev.sfr.net) |
2023-12-11 21:37:09 +0100 | mikess | (~sam@user/mikess) |
2023-12-11 21:38:48 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-12-11 21:58:12 +0100 | <haskellbridge> | 12<Celestial> I don't know what that video is about specifically, but I just can't listen to Jordan Peterson. He is a right-wing freak who time and time again targets trans-people and spews bigoted nonsense |
2023-12-11 21:59:32 +0100 | Square2 | (~Square4@user/square) |
2023-12-11 22:01:12 +0100 | <ncf> | +1 |
2023-12-11 22:01:41 +0100 | <Rembane> | +1 |
2023-12-11 22:02:01 +0100 | Square | (~Square@user/square) (Ping timeout: 245 seconds) |
2023-12-11 22:05:40 +0100 | trev | (~trev@user/trev) (Quit: trev) |
2023-12-11 22:08:00 +0100 | thegeekinside | (~thegeekin@189.217.90.224) (Read error: Connection reset by peer) |
2023-12-11 22:13:50 +0100 | rvalue | (~rvalue@user/rvalue) (Quit: ZNC - https://znc.in) |
2023-12-11 22:14:04 +0100 | rvalue | (~rvalue@user/rvalue) |
2023-12-11 22:14:47 +0100 | thegeekinside | (~thegeekin@189.217.90.224) |
2023-12-11 22:14:47 +0100 | thegeekinside | (~thegeekin@189.217.90.224) (Read error: Connection reset by peer) |
2023-12-11 22:15:11 +0100 | <mauke> | yes (also why would you link to his youtube channel) |
2023-12-11 22:19:47 +0100 | drdo9 | (~drdo@bl14-14-49.dsl.telepac.pt) |
2023-12-11 22:19:55 +0100 | mikess | (~sam@user/mikess) (Quit: leaving) |
2023-12-11 22:20:25 +0100 | drdo | (~drdo@bl14-14-49.dsl.telepac.pt) (Killed (NickServ (GHOST command used by drdo9))) |
2023-12-11 22:20:34 +0100 | drdo9 | drdo |
2023-12-11 22:21:16 +0100 | thegeekinside | (~thegeekin@189.217.90.224) |
2023-12-11 22:21:19 +0100 | thegeekinside | (~thegeekin@189.217.90.224) (Read error: Connection reset by peer) |
2023-12-11 22:27:06 +0100 | danza | (~danza@151.37.252.39) (Ping timeout: 260 seconds) |
2023-12-11 22:27:07 +0100 | drdo8 | (~drdo@bl14-14-49.dsl.telepac.pt) |
2023-12-11 22:28:50 +0100 | fendor | (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) (Remote host closed the connection) |
2023-12-11 22:29:13 +0100 | drdo | (~drdo@bl14-14-49.dsl.telepac.pt) (Ping timeout: 276 seconds) |
2023-12-11 22:29:44 +0100 | drdo8 | drdo |
2023-12-11 22:30:57 +0100 | Guest70 | (~Guest70@137.59.204.20) |
2023-12-11 22:31:09 +0100 | mmhat | (~mmh@p200300f1c702cdcaee086bfffe095315.dip0.t-ipconnect.de) (Quit: WeeChat 4.1.2) |
2023-12-11 22:31:46 +0100 | Guest70 | (~Guest70@137.59.204.20) (Client Quit) |
2023-12-11 22:50:59 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2023-12-11 22:51:05 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-12-11 22:52:54 +0100 | igemnace | (~ian@user/igemnace) (Read error: Connection reset by peer) |
2023-12-11 22:53:21 +0100 | igemnace | (~ian@user/igemnace) |
2023-12-11 22:59:49 +0100 | mikess | (~sam@user/mikess) |
2023-12-11 22:59:49 +0100 | thegeekinside | (~thegeekin@189.217.90.224) |
2023-12-11 23:00:11 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
2023-12-11 23:03:44 +0100 | pavonia | (~user@user/siracusa) |
2023-12-11 23:04:35 +0100 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
2023-12-11 23:13:11 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
2023-12-11 23:16:15 +0100 | <Joao003> | how do i extract `x' out of `Just x' without pattern-matching? |
2023-12-11 23:16:36 +0100 | <monochrom> | Cannot. Use pattern matching. |
2023-12-11 23:16:53 +0100 | <Joao003> | @hoogle Maybe a -> a |
2023-12-11 23:16:54 +0100 | <lambdabot> | Data.Maybe fromJust :: HasCallStack => Maybe a -> a |
2023-12-11 23:16:54 +0100 | <lambdabot> | Network.AWS.Prelude fromJust :: () => Maybe a -> a |
2023-12-11 23:16:54 +0100 | <lambdabot> | Data.Maybe.Utils forceMaybe :: Maybe a -> a |
2023-12-11 23:17:03 +0100 | <monochrom> | If you find yourself doing it a million times, then: |
2023-12-11 23:17:10 +0100 | <monochrom> | 1. Write a helper function? |
2023-12-11 23:17:18 +0100 | <Joao003> | 2: |
2023-12-11 23:17:25 +0100 | <monochrom> | 2. Perhaps don't have Maybe in the first place? |
2023-12-11 23:17:35 +0100 | <Joao003> | % Data.Maybe.fromJust (Just 8) |
2023-12-11 23:17:35 +0100 | <yahb2> | 8 |
2023-12-11 23:19:09 +0100 | <geekosaur> | note that it throws if it's Nothing |
2023-12-11 23:19:55 +0100 | <Joao003> | but in my case it's guaranteed* to be just |
2023-12-11 23:20:22 +0100 | <Joao003> | * guaranteed under the circumstances of the codewars kata that i'm doing |
2023-12-11 23:21:50 +0100 | <monochrom> | In that kind of situations I usually use pattern matching and have "Nothing -> error "shouldn't happen because ..."" |
2023-12-11 23:22:16 +0100 | <Joao003> | i'm pointless |
2023-12-11 23:22:23 +0100 | <monochrom> | I am too lazy to import Data.Maybe so I would rather write that longer error message! |
2023-12-11 23:22:31 +0100 | <Joao003> | lol |
2023-12-11 23:22:34 +0100 | <glguy> | vscode will import it for me |
2023-12-11 23:22:38 +0100 | <c_wraith> | :t fromMaybe (error "message") |
2023-12-11 23:22:39 +0100 | <lambdabot> | Maybe a -> a |
2023-12-11 23:22:42 +0100 | <glguy> | *full speed ahead* |
2023-12-11 23:22:50 +0100 | machinedgod | (~machinedg@93-136-135-211.adsl.net.t-com.hr) |
2023-12-11 23:22:50 +0100 | <Joao003> | :t fromMaybe |
2023-12-11 23:22:51 +0100 | <lambdabot> | a -> Maybe a -> a |
2023-12-11 23:23:07 +0100 | <Joao003> | :t fromJust |
2023-12-11 23:23:08 +0100 | <lambdabot> | Maybe a -> a |
2023-12-11 23:23:15 +0100 | <monochrom> | Well yeah approximately the only IDE feature that I miss is auto imports. |
2023-12-11 23:23:15 +0100 | <Joao003> | @src fromJust |
2023-12-11 23:23:15 +0100 | <lambdabot> | fromJust Nothing = undefined |
2023-12-11 23:23:15 +0100 | <lambdabot> | fromJust (Just x) = x |
2023-12-11 23:23:25 +0100 | <Joao003> | IT USES PATTERN MATCHING NOOOOO |
2023-12-11 23:23:29 +0100 | <monochrom> | (compared to emacs haskell-mode or dante) |
2023-12-11 23:23:33 +0100 | <c_wraith> | everything uses pattern matching |
2023-12-11 23:23:39 +0100 | <c_wraith> | pattern matching is the primitive operation |
2023-12-11 23:23:41 +0100 | tv | (~tv@user/tv) |
2023-12-11 23:23:41 +0100 | <glguy> | Joao003: if you want to avoid pattern matching, use python |
2023-12-11 23:23:44 +0100 | <c_wraith> | there is no other option |
2023-12-11 23:23:45 +0100 | <Joao003> | ok |
2023-12-11 23:24:05 +0100 | <monochrom> | Yeah pattern matching is the fundamental one. You can write helper functions but it always traces back to pattern matching. |
2023-12-11 23:24:22 +0100 | <monochrom> | Why are you afraid of pattern matching? |
2023-12-11 23:24:43 +0100 | <Joao003> | 'cause i'm pointless |
2023-12-11 23:25:09 +0100 | <Joao003> | see the joke? |
2023-12-11 23:26:11 +0100 | <monochrom> | And when you later graduate to Agda or Coq or Lean or Epigram... then an elimination rule that looks like induction is the even more fundamental one. |
2023-12-11 23:26:48 +0100 | <monochrom> | But patterns or elimination rule, you still cannot escape from addressing "what about the other cases?" |
2023-12-11 23:27:21 +0100 | <darchitect> | monochrom: are you a bot or _ ? |
2023-12-11 23:27:28 +0100 | <glguy> | _ |
2023-12-11 23:27:38 +0100 | <darchitect> | :d |
2023-12-11 23:27:41 +0100 | <monochrom> | I am a Chinese Room, albeit biological. |
2023-12-11 23:28:19 +0100 | <monochrom> | Everyone loves a neurotic Chinese Room, no? \∩/ |
2023-12-11 23:28:40 +0100 | <c_wraith> | hmm. I've seen monochrom accused of many things before, but not being a bot |
2023-12-11 23:28:55 +0100 | <glguy> | c_wraith: time to update your counter |
2023-12-11 23:29:10 +0100 | <c_wraith> | I need a whole new column in on the whiteboard! |
2023-12-11 23:30:06 +0100 | <[Leary]> | If you really want to avoid pattern matching, you can do it by asking GHC to compile System F. |
2023-12-11 23:30:10 +0100 | <monochrom> | Well, consider the other side: I have accused humanity of many things, so it would be absurd if I self-identified as human, no? >:) |
2023-12-11 23:30:51 +0100 | <c_wraith> | nah, that just identifies you as a cynic |
2023-12-11 23:31:06 +0100 | <monochrom> | But System F simply makes you use something close to an elimination rule. |
2023-12-11 23:32:22 +0100 | <monochrom> | And after you have done that in anger, you realize it is only a superficial syntactic difference, it's still pattern matching. |
2023-12-11 23:32:46 +0100 | <Joao003> | to prove monochrom is a bot: |
2023-12-11 23:32:49 +0100 | <Joao003> | monochrom help |
2023-12-11 23:33:58 +0100 | <glguy> | You're going to have to work on your Turing Test |
2023-12-11 23:34:31 +0100 | <c_wraith> | you just need to know the right keyphrase |
2023-12-11 23:34:32 +0100 | <c_wraith> | hey monochrom, how are your students this term? |
2023-12-11 23:34:44 +0100 | <monochrom> | I don't teach a course this term. :) |
2023-12-11 23:34:52 +0100 | <c_wraith> | so.. perfect? |
2023-12-11 23:34:59 +0100 | <monochrom> | Oh next term is going to be nightmare. I have 9am classes. |
2023-12-11 23:35:40 +0100 | <monochrom> | And literally nightmare because normally I should be still sleeping at 9am. >:) |
2023-12-11 23:35:40 +0100 | <c_wraith> | that's inhumane |
2023-12-11 23:35:53 +0100 | chele | (~chele@user/chele) (Remote host closed the connection) |
2023-12-11 23:36:03 +0100 | <darkling> | Could be worse. At least you don't get the 4-5 slot on a Friday afternoon. |
2023-12-11 23:36:16 +0100 | <darchitect> | I like IRC |
2023-12-11 23:36:17 +0100 | <darchitect> | :) |
2023-12-11 23:36:27 +0100 | <Joao003> | darchitect: me too |
2023-12-11 23:36:41 +0100 | <monochrom> | Actually I would enjoy Friday 4-5pm and then tell students "now pub time!" |
2023-12-11 23:37:09 +0100 | <Joao003> | any1 does codewars here? |
2023-12-11 23:37:19 +0100 | <monochrom> | Great saying from Jay Misra after a conference: "Computer science has become a bit too technical, let's go for a drink." |
2023-12-11 23:37:28 +0100 | <c_wraith> | the courses where the instructor said that were some of my favorites |
2023-12-11 23:37:40 +0100 | <monochrom> | And to think that he wrote a lot of very technical papers... |
2023-12-11 23:37:45 +0100 | <Joao003> | monochrom: this is #haskell, not ## |
2023-12-11 23:38:46 +0100 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 276 seconds) |
2023-12-11 23:39:14 +0100 | <xerox> | Joao003: bunch of people in here are doing https://adventofcode.com/ right now |
2023-12-11 23:39:36 +0100 | <monochrom> | I think every 3 years one person comes here and does codewars... |
2023-12-11 23:39:49 +0100 | <Joao003> | xerox: i kno |
2023-12-11 23:46:32 +0100 | <monochrom> | Ugh wait, my colleague has proposed to swap class times with me, now I'm doing the afternoon classes instead! |
2023-12-11 23:46:51 +0100 | <c_wraith> | victory! |
2023-12-11 23:47:06 +0100 | <Joao003> | i hate afternoon classes |
2023-12-11 23:51:27 +0100 | nate4 | (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
2023-12-11 23:52:26 +0100 | <xerox> | monochrom: when I went to the very first `AngloHaskell's I was very surprised when what you said you would enjoy actually happened every day, I got used to it quite fast (: |
2023-12-11 23:55:40 +0100 | alp_ | (~alp@2001:861:e3d6:8f80:c150:fb83:d53f:eaf2) (Ping timeout: 276 seconds) |
2023-12-11 23:56:11 +0100 | nate4 | (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 245 seconds) |
2023-12-11 23:56:18 +0100 | <Joao003> | i think the most useful thing about monads is the fact that `(->) r` is a monad |
2023-12-11 23:57:59 +0100 | cwdar^ | (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Remote host closed the connection) |