Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379 .. 5022
— 502,152 events total
2020-11-18 23:41:15 × chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer)
2020-11-18 23:41:29 <boxscape> though of course that's not fully specified at this point
2020-11-18 23:41:39 × elfets quits (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) (Ping timeout: 256 seconds)
2020-11-18 23:41:52 <dolio> And even in more uniform systems, parametricity gets kind of fuzzy and unsatisfying when you talk about applying it to types.
2020-11-18 23:42:05 → chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net)
2020-11-18 23:42:08 <boxscape> ski intuitively I would expect sameNat not to compile in a Haskell with foreach, but maybe it should, I'm not sure. Hm, would it compile in agda?
2020-11-18 23:42:28 <ski> (and this is one argument against the terminology "type constructor" (vs. "data constructor"), i suppose .. also, with `DataKinds', with say `data Tag = E | D', `Tag' being a kind, what do we call `Tag',`E',`D' ? calling the latter two "type constructors" would seem to be confusing, possibly ? .. oh, well)
2020-11-18 23:43:06 <ski> boxscape : in Agda, with implicit parameters, yes
2020-11-18 23:43:14 <boxscape> okay, fair enough
2020-11-18 23:43:32 <ski> or, well
2020-11-18 23:43:50 <ski> you'd have to actually do recursion on the `Nat's, not being able to use non-linear patterns
2020-11-18 23:44:09 <ski> (so not with that exact implementation. but you could implement it)
2020-11-18 23:44:13 <boxscape> ok
2020-11-18 23:44:30 → elfets joins (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de)
2020-11-18 23:46:37 × boxscape quits (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) (Quit: Connection closed)
2020-11-18 23:46:50 × jonatanb quits (~jonatanb@83.24.155.27.ipv4.supernova.orange.pl) (Remote host closed the connection)
2020-11-18 23:47:03 → boxscape joins (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55)
2020-11-18 23:47:19 × hexfive quits (~hexfive@50-47-142-195.evrt.wa.frontiernet.net) (Quit: i must go. my people need me.)
2020-11-18 23:48:01 <energizer> usually arrays are indexed by natural numbers. is there something like an array but indexed by some other type
2020-11-18 23:48:30 <energizer> like strings or whatever
2020-11-18 23:48:33 <ski> > listArray (LT,GT) [-1,0,1]
2020-11-18 23:48:35 <lambdabot> array (LT,GT) [(LT,-1),(EQ,0),(GT,1)]
2020-11-18 23:48:38 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
2020-11-18 23:49:01 <ski> perhaps you want some form of trie ?
2020-11-18 23:49:24 <ski> @type listArray (LT,GT) [-1,0,1 :: Integer]
2020-11-18 23:49:26 <lambdabot> Array Ordering Integer
2020-11-18 23:49:31 <ClaudiusMaximus> Ix is a class for mapping values of a type to natural numbers for use as array indices
2020-11-18 23:49:44 <ski> (an array indexed by values of type `Ordering')
2020-11-18 23:49:59 <ski> @type listArray
2020-11-18 23:50:01 <lambdabot> Ix i => (i, i) -> [e] -> Array i e
2020-11-18 23:50:23 → jonatanb joins (jonatanb@gateway/vpn/protonvpn/jonatanb)
2020-11-18 23:50:54 <energizer> there should be the property that a<b<c means b is a valid index whenever a and c are
2020-11-18 23:51:15 <ski> @type range
2020-11-18 23:51:16 <lambdabot> Ix a => (a, a) -> [a]
2020-11-18 23:51:27 <ski> gives values in a kind of "interval"
2020-11-18 23:51:46 <ski> (for two-dimensional arrays, it gives indices in a "rectangle")
2020-11-18 23:52:00 <ClaudiusMaximus> @type inRange -- tests, and i can never remember the argument order
2020-11-18 23:52:01 <lambdabot> Ix a => (a, a) -> a -> Bool
2020-11-18 23:52:05 <ski> > range ((-1,-1),(2,3))
2020-11-18 23:52:06 × chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer)
2020-11-18 23:52:07 <lambdabot> [(-1,-1),(-1,0),(-1,1),(-1,2),(-1,3),(0,-1),(0,0),(0,1),(0,2),(0,3),(1,-1),(...
2020-11-18 23:52:23 → chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net)
2020-11-18 23:52:54 <ClaudiusMaximus> (it has a name that sounds infix, but it is flipped w.r.t. infix usage)
2020-11-18 23:54:24 <ski> in other words, `range (lo,hi)' should give a list of all indices `i', where ⌜lo ≼ i ∧ i ≼ hi⌝, where the ordering here is not lexicographic ordering in case of tuples, but rather the product order (a partial order, not a total/linear one)
2020-11-18 23:57:06 <ski> (ClaudiusMaximus : i wonder how that happened ..)
2020-11-18 23:58:34 <boxscape> %! ghc --version
2020-11-18 23:58:34 <yahb> boxscape: [Segmentation fault]
2020-11-18 23:58:35 <boxscape> cool
2020-11-19 00:00:38 × boxscape quits (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) (Quit: Connection closed)
2020-11-19 00:00:49 → boxscape joins (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55)
2020-11-19 00:02:44 <boxscape> % :kind! Fam MkR (MkR :: Relation Int Int) -- so this is fine
2020-11-19 00:02:45 <yahb> boxscape: forall {k} {a :: k}. Relation a Int; = 'MkR
2020-11-19 00:02:46 <boxscape> % :kind! Fam MkR (MkR :: Int Int) -- But I do find it a bit confusing that this has no output
2020-11-19 00:02:46 <yahb> boxscape:
2020-11-19 00:03:24 <boxscape> I guess I'll try installing HEAD and see if it's fixed there
2020-11-19 00:03:31 → erisco joins (~erisco@d24-57-249-233.home.cgocable.net)
2020-11-19 00:05:27 × sfvm quits (~sfvm@37.228.215.148) (Remote host closed the connection)
2020-11-19 00:05:37 × alp quits (~alp@2a01:e0a:58b:4920:7462:8d66:154:f167) (Ping timeout: 272 seconds)
2020-11-19 00:06:19 ski . o O ( <https://lambdacats.github.io/fixed-in-head/> )
2020-11-19 00:07:01 → sfvm joins (~sfvm@37.228.215.148)
2020-11-19 00:07:34 <boxscape> :)
2020-11-19 00:08:23 <hpc> whenever someone says "it's fixed in head", i read it as "it's fixed in my imagination"
2020-11-19 00:08:26 × borne quits (~fritjof@200116b864880600f1dc39039d201adf.dip.versatel-1u1.de) (Ping timeout: 264 seconds)
2020-11-19 00:09:30 hackage witch 0.0.0.3 - Convert values from one type into another. https://hackage.haskell.org/package/witch-0.0.0.3 (fozworth)
2020-11-19 00:10:52 × jedws quits (~jedws@101.184.175.183) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-11-19 00:15:57 → heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-11-19 00:16:36 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 240 seconds)
2020-11-19 00:19:03 × mastarija quits (~mastarija@93-136-63-196.adsl.net.t-com.hr) (Remote host closed the connection)
2020-11-19 00:19:07 × Entertainment quits (~entertain@104.246.132.210) ()
2020-11-19 00:19:25 → mastarija joins (~mastarija@93-136-63-196.adsl.net.t-com.hr)
2020-11-19 00:20:19 × nbloomf quits (~nbloomf@2600:1700:ad14:3020:d091:432d:3cee:b0b2) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-11-19 00:24:41 × jonatanb quits (jonatanb@gateway/vpn/protonvpn/jonatanb) (Remote host closed the connection)
2020-11-19 00:27:44 × vicfred quits (~vicfred@unaffiliated/vicfred) (Quit: Leaving)
2020-11-19 00:27:44 × chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer)
2020-11-19 00:28:01 → chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net)
2020-11-19 00:28:19 × conal quits (~conal@64.71.133.70) (Ping timeout: 246 seconds)
2020-11-19 00:29:48 → nbloomf joins (~nbloomf@2600:1700:ad14:3020:6c29:bc9c:b97a:2b45)
2020-11-19 00:29:49 <monochrom> That's half true because clearly there is no release plan other than imagination.
2020-11-19 00:30:00 → conal joins (~conal@66.115.157.132)
2020-11-19 00:32:10 × solonarv quits (~solonarv@astrasbourg-653-1-156-4.w90-6.abo.wanadoo.fr) (Ping timeout: 265 seconds)
2020-11-19 00:32:13 × chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer)
2020-11-19 00:32:42 × haasn quits (~nand@mpv/developer/haasn) (Quit: ZNC 1.7.5+deb4 - https://znc.in)
2020-11-19 00:33:04 → chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net)
2020-11-19 00:33:39 DTZUZU is now known as toxix
2020-11-19 00:35:55 → hekkaidekapus_ joins (~tchouri@gateway/tor-sasl/hekkaidekapus)
2020-11-19 00:37:29 → fendor_ joins (~fendor@178.165.128.131.wireless.dyn.drei.com)
2020-11-19 00:37:38 × nbloomf quits (~nbloomf@2600:1700:ad14:3020:6c29:bc9c:b97a:2b45) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-11-19 00:37:43 × hekkaidekapus quits (~tchouri@gateway/tor-sasl/hekkaidekapus) (Ping timeout: 240 seconds)
2020-11-19 00:37:45 × jespada quits (~jespada@90.254.245.49) (Ping timeout: 256 seconds)
2020-11-19 00:37:50 × chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer)
2020-11-19 00:38:04 → chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net)
2020-11-19 00:38:25 <boxscape> ski: FWIW this fails in agda, but I'm not sure if the same caveat applies here that you mentioned about Nats https://pastebin.com/jKsJpPVd
2020-11-19 00:39:05 → jespada joins (~jespada@90.254.245.49)
2020-11-19 00:39:22 <boxscape> guess I should look up non-linear pattern
2020-11-19 00:39:32 <dolio> You need to prove it by cases.
2020-11-19 00:40:03 × fendor quits (~fendor@77.119.128.218.wireless.dyn.drei.com) (Ping timeout: 260 seconds)
2020-11-19 00:40:31 × mastarija quits (~mastarija@93-136-63-196.adsl.net.t-com.hr) (Quit: Leaving)
2020-11-19 00:40:34 <boxscape> dolio right, that would have been my intuition but from my conversation with ski it initially sounded like this would work (and it would in Haskell type families, I think)
2020-11-19 00:41:28 × fr33domlover quits (~fr33domlo@fsf/member/fr33domlover) (Ping timeout: 260 seconds)
2020-11-19 00:42:00 → haasn joins (~nand@mpv/developer/haasn)
←Prev  Next→
Page 1 .. 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379 .. 5022

All times are in UTC.