Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 4013 4014 4015 4016 4017 4018 4019 4020 4021 4022 4023 .. 5022
— 502,152 events total
2021-03-25 00:10:12 → perrier-jouet joins (~perrier-j@modemcable012.251-130-66.mc.videotron.ca)
2021-03-25 00:10:28 <monochrom> "(S a -> T a) has positive a with fmap f = (posfmap_T f .) . (. negfmap_S f)" if "(S a) has negative a with fmap f = negfmap_S f" and "(T a) has positive a with fmap f = posfmap_T f"
2021-03-25 00:10:59 <ski> looks reasonable
2021-03-25 00:11:04 <monochrom> Recursively use that, along with the appropriate base cases.
2021-03-25 00:11:15 <ski> yep (and the `forall')
2021-03-25 00:11:30 × jiribenes quits (~jiribenes@rosa.jiribenes.com) (Remote host closed the connection)
2021-03-25 00:12:28 → Benzi-Junior joins (~BenziJuni@dsl-149-67-143.hive.is)
2021-03-25 00:13:04 × azure1 quits (~azure@103.154.230.130) (Read error: Connection reset by peer)
2021-03-25 00:13:06 → azure2 joins (~azure@103.154.230.130)
2021-03-25 00:13:45 × stree quits (~stree@68.36.8.116) (Ping timeout: 264 seconds)
2021-03-25 00:13:45 → kupi joins (uid212005@gateway/web/irccloud.com/x-ulwctdrxjxxnpyln)
2021-03-25 00:13:46 <ski> (`dimap f g = (g .) . (. f)', btw)
2021-03-25 00:14:19 <ski> (aka `f ~> g')
2021-03-25 00:16:54 <unyu> it's not haskell if it doesn't have squiggly arrows and other ascii <strike>noise</strike> art
2021-03-25 00:18:18 ski grins
2021-03-25 00:18:48 × pfurla quits (~pfurla@ool-182ed2e2.dyn.optonline.net) (Ping timeout: 245 seconds)
2021-03-25 00:18:48 × emmanuel_erc quits (~user@2603-7000-9600-01c9-0000-0000-0000-0874.res6.spectrum.com) (Read error: Connection reset by peer)
2021-03-25 00:19:01 <ski> (cf. how it's not called "pointless" for no reason :p)
2021-03-25 00:19:04 → emmanuel_erc joins (~user@2603-7000-9600-01c9-0000-0000-0000-0874.res6.spectrum.com)
2021-03-25 00:19:45 × ph88 quits (~ph88@ip5f5af71a.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds)
2021-03-25 00:23:00 → wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2021-03-25 00:24:38 × madjestic quits (~Android@86-88-72-244.fixed.kpn.net) (Ping timeout: 245 seconds)
2021-03-25 00:25:03 × Tuplanolla quits (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) (Quit: Leaving.)
2021-03-25 00:25:34 × zebrag quits (~inkbottle@aaubervilliers-654-1-109-157.w86-212.abo.wanadoo.fr) (Quit: Konversation terminated!)
2021-03-25 00:25:56 → zebrag joins (~inkbottle@aaubervilliers-654-1-109-157.w86-212.abo.wanadoo.fr)
2021-03-25 00:26:55 → stree joins (~stree@68.36.8.116)
2021-03-25 00:28:21 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 256 seconds)
2021-03-25 00:28:32 × nuncanada quits (~dude@179.235.160.168) (Read error: Connection reset by peer)
2021-03-25 00:31:02 × puke quits (~vroom@217.138.252.170) (Quit: puke)
2021-03-25 00:31:53 → ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net)
2021-03-25 00:32:08 × myShoggoth quits (~myShoggot@75.164.81.55) (Ping timeout: 245 seconds)
2021-03-25 00:32:08 × emmanuel_erc quits (~user@2603-7000-9600-01c9-0000-0000-0000-0874.res6.spectrum.com) (Read error: Connection reset by peer)
2021-03-25 00:32:40 → emmanuel_erc joins (~user@2603-7000-9600-01c9-0000-0000-0000-0874.res6.spectrum.com)
2021-03-25 00:32:43 → balbirs joins (~balbirs@121-45-173-48.tpgi.com.au)
2021-03-25 00:35:43 × cole-h quits (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) (Ping timeout: 256 seconds)
2021-03-25 00:36:47 × ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Ping timeout: 260 seconds)
2021-03-25 00:37:58 <L29Ah> https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/derive-functor so cute
2021-03-25 00:38:14 <L29Ah> i hope haskell will write code for me someday, given the type signatures ;)
2021-03-25 00:38:14 → __minoru__shirae joins (~shiraeesh@46.34.207.1)
2021-03-25 00:38:39 <glguy> If the type signatures were enough they'd be as hard to write as the program without them
2021-03-25 00:38:48 × balbirs quits (~balbirs@121-45-173-48.tpgi.com.au) (Quit: Leaving)
2021-03-25 00:38:49 × emmanuel_erc quits (~user@2603-7000-9600-01c9-0000-0000-0000-0874.res6.spectrum.com) (Read error: Connection reset by peer)
2021-03-25 00:39:09 <monochrom> Proof: Agda, Coq, Lean.
2021-03-25 00:39:15 → emmanuel_erc joins (~user@2603-7000-9600-01c9-0000-0000-0000-0874.res6.spectrum.com)
2021-03-25 00:39:38 <glguy> Those over-achieve and prove the type signatures can be harder to write than the original program
2021-03-25 00:40:56 <monochrom> I have a cunning plan! The programming language has its type system in sync with its term grammar. >:)
2021-03-25 00:41:59 <monochrom> var :: var. If f :: T and x :: U, then f x :: T U.
2021-03-25 00:42:29 <ski> @djinn (a -> b) -> ((m -> (a -> m) -> m) -> (m -> (b -> m) -> m))
2021-03-25 00:42:29 <lambdabot> f a b c d = b c (\ e -> d (a e))
2021-03-25 00:44:00 <ski> monochrom : reminds me of one time i was trying to convince someone that it probably wasn't a good idea to conflate `\a -> b' and `a -> b' (in the sense that `(\x -> e) :: (\a -> b)' when `x :: a' implies `e :: b')
2021-03-25 00:44:23 <monochrom> If "Gamma, var::T |- e::U", then "Gamma |- \var.e :: \T.U"
2021-03-25 00:44:36 <ski> exactly
2021-03-25 00:45:12 <monochrom> Free Programming Theorem: For every type t, t::t
2021-03-25 00:48:26 ski . o O ( <https://en.wikipedia.org/wiki/Lambek_calculus>,<https://en.wikipedia.org/wiki/Noncommutative_logic>,<https://en.wikipedia.org/wiki/Categorial_grammar>,<https://en.wikipedia.org/wiki/Pregroup_Grammar> )
2021-03-25 00:48:52 × dibblego quits (~dibblego@haskell/developer/dibblego) (Ping timeout: 276 seconds)
2021-03-25 00:51:33 → wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2021-03-25 00:51:52 <ski> (although i've thought about something looking a bit like `f x :: T U' ..)
2021-03-25 00:53:07 × solidus-river quits (~mike@174.127.249.180) (Remote host closed the connection)
2021-03-25 00:56:31 → ddellacosta joins (ddellacost@gateway/vpn/mullvad/ddellacosta)
2021-03-25 00:56:34 → ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net)
2021-03-25 00:56:36 × ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection)
2021-03-25 00:58:14 → elusive joins (~Jeanne-Ka@static-198-54-134-109.cust.tzulo.com)
2021-03-25 01:00:05 <monochrom> Would you like to call my language "System T_T"? >:)
2021-03-25 01:01:08 → dibblego joins (~dibblego@122-199-1-30.ip4.superloop.com)
2021-03-25 01:01:10 × dibblego quits (~dibblego@122-199-1-30.ip4.superloop.com) (Changing host)
2021-03-25 01:01:10 → dibblego joins (~dibblego@haskell/developer/dibblego)
2021-03-25 01:02:21 × epicte7us quits (~epictetus@ip72-194-215-136.sb.sd.cox.net) (Read error: Connection reset by peer)
2021-03-25 01:06:17 <ski> (more specfically, it would be `(| f ; x |) :: T U', given `f :: T' and `x :: U'. e.g. you could (re)express `sum (concat nss) = sum (map sum nss)' (with `nss :: [] ([] Nat)'), where `concat :: [] . [] -> []' and `sum :: [] Nat -> Nat' (or with any monoid, written additively), as `sum (| concat (| l0 , l1 |) ; n |) = sum (| l0 ; sum (| l1 ; n |) |)', where `l0,l1 :: []' and `n :: Nat')
2021-03-25 01:06:43 → pfurla joins (~pfurla@ool-182ed2e2.dyn.optonline.net)
2021-03-25 01:06:56 × thc202 quits (~thc202@unaffiliated/thc202) (Ping timeout: 240 seconds)
2021-03-25 01:07:19 → rajivr joins (uid269651@gateway/web/irccloud.com/x-dvlsvpxgnpvrwfuk)
2021-03-25 01:07:25 → Wuzzy joins (~Wuzzy@p57a2ecf2.dip0.t-ipconnect.de)
2021-03-25 01:07:48 <ski> "System Tᴛ" to me sounds like it would have constructs for expressing and manipulating sequences, maybe ?
2021-03-25 01:08:05 × twk- quits (~thewormki@unaffiliated/twk-) (Ping timeout: 265 seconds)
2021-03-25 01:08:23 <monochrom> "T_T" is meant to be an emoticon
2021-03-25 01:09:10 <ski> (i'm aware ;)
2021-03-25 01:09:40 <int-e> oh, sentience
2021-03-25 01:09:56 <monochrom> well, a pun on all of these: the emoticon, "system T", T subscript T being another notation for "term T with type T" or "type T with term T"
2021-03-25 01:10:26 <int-e> monochrom: let's play hangman with it
2021-03-25 01:10:34 <monochrom> hahaha
2021-03-25 01:10:37 <ski> didn't Church use superscripts, for the types ?
2021-03-25 01:10:43 <int-e> . o O ( tut tut tut, not what you're thinking )
2021-03-25 01:11:16 × DataComputist quits (~lumeng@50.43.26.251) (Ping timeout: 265 seconds)
2021-03-25 01:11:34 × whataday quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection)
2021-03-25 01:11:36 ski . o O ( "TÖT" )
2021-03-25 01:12:04 <int-e> . o O ( Ich tät ein "ä" bevorzugen. )
2021-03-25 01:12:41 → whataday joins (~xxx@2400:8902::f03c:92ff:fe60:98d8)
2021-03-25 01:12:42 × emmanuel_erc quits (~user@2603-7000-9600-01c9-0000-0000-0000-0874.res6.spectrum.com) (Read error: Connection reset by peer)
2021-03-25 01:12:51 → emmanuel_erc joins (~user@2603-7000-9600-01c9-0000-0000-0000-0874.res6.spectrum.com)
2021-03-25 01:17:37 → jamm_ joins (~jamm@unaffiliated/jamm)
2021-03-25 01:18:02 × m0rphism quits (~m0rphism@HSI-KBW-085-216-104-059.hsi.kabelbw.de) (Ping timeout: 265 seconds)
2021-03-25 01:20:58 → jamm__ joins (~jamm@unaffiliated/jamm)
2021-03-25 01:20:59 → twk- joins (~thewormki@unaffiliated/twk-)
2021-03-25 01:21:27 → molehillish joins (~molehilli@2600:8800:8d06:1800:a4ec:e3c6:6b54:caa8)
2021-03-25 01:22:39 × jamm_ quits (~jamm@unaffiliated/jamm) (Ping timeout: 268 seconds)
2021-03-25 01:24:24 × Synthetica quits (uid199651@gateway/web/irccloud.com/x-pidwjwkshsuukvyi) (Quit: Connection closed for inactivity)
2021-03-25 01:25:35 × zebrag quits (~inkbottle@aaubervilliers-654-1-109-157.w86-212.abo.wanadoo.fr) (Quit: Konversation terminated!)
2021-03-25 01:25:44 × jamm__ quits (~jamm@unaffiliated/jamm) (Ping timeout: 268 seconds)
2021-03-25 01:25:56 → zebrag joins (~inkbottle@aaubervilliers-654-1-109-157.w86-212.abo.wanadoo.fr)
2021-03-25 01:26:22 × molehillish quits (~molehilli@2600:8800:8d06:1800:a4ec:e3c6:6b54:caa8) (Ping timeout: 260 seconds)
←Prev  Next→
Page 1 .. 4013 4014 4015 4016 4017 4018 4019 4020 4021 4022 4023 .. 5022

All times are in UTC.