Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→ 502,152 events total
2020-11-13 01:13:28 <taio> The selection would be made via the namespace.
2020-11-13 01:15:43 × ChaiTRex quits (~ChaiTRex@gateway/tor-sasl/chaitrex) (Ping timeout: 240 seconds)
2020-11-13 01:18:03 ChaiTRex joins (~ChaiTRex@gateway/tor-sasl/chaitrex)
2020-11-13 01:20:10 nbloomf joins (~nbloomf@2600:1700:ad14:3020:4085:c5d6:bbdf:5f4e)
2020-11-13 01:20:12 × borne quits (~fritjof@200116b86423eb004fbf5cd6c83663b1.dip.versatel-1u1.de) (Ping timeout: 260 seconds)
2020-11-13 01:20:28 <unclechu> hey, can someone remind me what `|` means here? `type Demote k = (r :: Type) | r -> k`
2020-11-13 01:21:04 <taio> for example like this: adopt Ord as My Ord
2020-11-13 01:21:06 <taio> instance My Ord ... where ...
2020-11-13 01:23:08 TxGuy joins (~coffee2th@172-125-238-23.lightspeed.rcsntx.sbcglobal.net)
2020-11-13 01:24:28 × TxGuy quits (~coffee2th@172-125-238-23.lightspeed.rcsntx.sbcglobal.net) (Client Quit)
2020-11-13 01:25:46 <monochrom> https://mail.haskell.org/pipermail/haskell-cafe/2017-May/127147.html
2020-11-13 01:26:49 × devalot quits (~ident@mail.pmade.com) (Quit: ZNC - http://znc.in)
2020-11-13 01:27:08 <monochrom> (highest density of puns in a title ever, heehee)
2020-11-13 01:27:25 <dsal> unclechu: It's just a sum type like Bool
2020-11-13 01:27:27 <dsal> @src Bool
2020-11-13 01:27:27 <lambdabot> data Bool = False | True deriving (Eq, Ord)
2020-11-13 01:28:38 dsal suddenly very distracted by that deriving list
2020-11-13 01:28:45 <dsal> I'm glad I don't have to write base
2020-11-13 01:29:02 Lord_of_Life joins (~Lord@46.217.223.48)
2020-11-13 01:30:27 merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-11-13 01:30:28 jonatanb joins (~jonatanb@83.24.155.27.ipv4.supernova.orange.pl)
2020-11-13 01:30:35 <solonarv> dsal: no, that is not a sum type (cc: unclechu )
2020-11-13 01:30:49 × Lord_of_Life_ quits (~Lord@46.217.216.229) (Ping timeout: 264 seconds)
2020-11-13 01:31:12 <solonarv> that's an injectivity annotation (InjectiveTypeFamilies), which uses similar syntax to FunctionalDependencies
2020-11-13 01:31:31 <dsal> I just noticed `type` there. Been writing wrong language all day.
2020-11-13 01:31:35 <monochrom> fancy
2020-11-13 01:32:22 <dsal> Sorry for spreading my confusion.
2020-11-13 01:32:23 <solonarv> both (r :: Type) and r -> k would be illegal syntax in that position of a data declaration
2020-11-13 01:32:28 <monochrom> Yeah I suffer a bit of language mix-up too. After having written a fair amount of Racket, I wrote in C "(for i=0"
2020-11-13 01:32:35 <monochrom> and "(if i==0"
2020-11-13 01:33:32 <dsal> solonarv: Yeah, I'm at my least smart of the day.
2020-11-13 01:33:40 <dsal> I was writing go all day.
2020-11-13 01:34:07 <solonarv> same tbh, I've been up for 20 hours now and had a bunch of various brain-using things to do all day
2020-11-13 01:34:17 <monochrom> Further in the past, when I was writing both Java and Haskell, I wrote "public class Ord where"
2020-11-13 01:34:45 <monochrom> Aw, up for 20 hours, that kills, you need sleep.
2020-11-13 01:34:52 <unclechu> solonarv: thanks
2020-11-13 01:34:58 dsal is having a sleep deprivation conversation in another chat
2020-11-13 01:35:04 × jonatanb quits (~jonatanb@83.24.155.27.ipv4.supernova.orange.pl) (Ping timeout: 258 seconds)
2020-11-13 01:35:34 wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2020-11-13 01:35:42 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds)
2020-11-13 01:35:45 <taio> ok thanks for answering...
2020-11-13 01:35:51 <monochrom> Actually a short nap helps tremendously.
2020-11-13 01:36:45 × invaser quits (~Thunderbi@31.148.23.125) (Ping timeout: 240 seconds)
2020-11-13 01:37:55 <monochrom> My experience leads me to hypothesize that if you are working hard and sleep-deprived like this, if you are OK with taking short naps, your body switches to the uber-sleep mode, giving you the much fabled superpower of uber-sleep.
2020-11-13 01:38:00 <hekkaidekapus> Another sleepless here: taio, fancy a paper?
2020-11-13 01:40:16 × nbloomf quits (~nbloomf@2600:1700:ad14:3020:4085:c5d6:bbdf:5f4e) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-11-13 01:40:17 invaser joins (~Thunderbi@31.148.23.125)
2020-11-13 01:41:14 <taio> hm I'm not an academic. it's just an idea of mine. and I wonder if that would be possible or unproblematic.
2020-11-13 01:42:26 nbloomf joins (~nbloomf@2600:1700:ad14:3020:4085:c5d6:bbdf:5f4e)
2020-11-13 01:42:44 <hekkaidekapus> taio: “Type classes in Haskell” by C.V. Hall, K. Hammomd, S.L.P. Jones and P.L. Wadler <http://web.mit.edu/ghc/old.ghc/programatica/tools.old/semantics/Overloading/Related/p109-hall.pdf>
2020-11-13 01:44:07 <hekkaidekapus> You can skip the gnary parts and you will still get the gist of why you wanted to do was fundamentally problematic.
2020-11-13 01:44:08 × raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 260 seconds)
2020-11-13 01:45:32 <hekkaidekapus> Caveat: That paper covers what is now known as ‘Haskell 98’. Since 1998, there have been many additions to instance resolution mechanics.
2020-11-13 01:46:35 × jathan quits (~jathan@69.61.93.38) (Quit: WeeChat 2.3)
2020-11-13 01:46:36 <hekkaidekapus> *S.L. Peyton Jones
2020-11-13 01:46:43 <taio> well Idris has "named implementations" and it seems to work, to have proven itself.
2020-11-13 01:46:47 × nbloomf quits (~nbloomf@2600:1700:ad14:3020:4085:c5d6:bbdf:5f4e) (Client Quit)
2020-11-13 01:46:57 × invaser quits (~Thunderbi@31.148.23.125) (Ping timeout: 258 seconds)
2020-11-13 01:47:13 <hekkaidekapus> Idris is a whole other beast.
2020-11-13 01:48:24 <unclechu> i have a GADT `Stdout ∷ α `OneOf` '[ 'Play, 'Render ] ⇒ Backend α` (where `OneOf` is a type family which constrain an element to be in a list).
2020-11-13 01:48:26 <unclechu> i want to define a type-class which would convert type-level values to runtime values so i defined it like this: `class ToVal (α ∷ τ) where toVal ∷ Proxy (α ∷ τ) → τ`
2020-11-13 01:48:27 <unclechu> but this `instance ToVal ('Stdout ∷ Backend 'Play) where toVal Proxy = Stdout` fails with `it has an unpromotable context ‘OneOf α '[ 'Play, 'Render]’`
2020-11-13 01:48:34 <unclechu> can i do something about it?
2020-11-13 01:49:15 nbloomf joins (~nbloomf@2600:1700:ad14:3020:4085:c5d6:bbdf:5f4e)
2020-11-13 01:50:02 × kish` quits (~oracle@unaffiliated/oracle) (Remote host closed the connection)
2020-11-13 01:51:02 × neightchan quits (~natechan@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer)
2020-11-13 01:52:27 <unclechu> i cannot define any type with that constrainer constructor: `type Test = '[ 'Stdout ] :: [Backend 'Play]` fails with “unpromotable context”
2020-11-13 01:52:40 blankhart joins (~blankhart@pool-100-35-219-3.nwrknj.fios.verizon.net)
2020-11-13 01:53:01 nahcetan joins (~natechan@108-233-125-227.lightspeed.sntcca.sbcglobal.net)
2020-11-13 01:53:58 <unclechu> constrained*
2020-11-13 01:55:15 × Chi1thangoo quits (~Chi1thang@87.112.60.168) (Ping timeout: 260 seconds)
2020-11-13 01:56:37 × electricityZZZZ quits (~electrici@108-216-157-17.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 264 seconds)
2020-11-13 01:56:52 raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
2020-11-13 01:59:36 × taio quits (~enrik@p200300ceaf3ada00997810ade8eb1ff9.dip0.t-ipconnect.de) (Quit: Konversation terminated!)
2020-11-13 02:00:11 × nbloomf quits (~nbloomf@2600:1700:ad14:3020:4085:c5d6:bbdf:5f4e) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-11-13 02:00:11 × Collateral quits (~Collatera@4e69b241.skybroadband.com) (Ping timeout: 246 seconds)
2020-11-13 02:00:26 × Hijiri quits (~Hijiri@104.236.61.10) (Ping timeout: 272 seconds)
2020-11-13 02:06:32 merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-11-13 02:07:19 × raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 256 seconds)
2020-11-13 02:07:40 <blankhart> let is treated as a core language construct rather than as sugar for a lambda and application in some presentations like write you a haskell. is let generalization the reason for this? are there others?
2020-11-13 02:09:26 <monochrom> That and recursion.
2020-11-13 02:09:51 <dolio> What does it mean to be a 'core language construct'? The dynamic semantics in Haskell are given in terms of other things, but the type checking is different.
2020-11-13 02:10:05 <dolio> In the Haskell report, I mean.
2020-11-13 02:10:51 × tinwood quits (~tinwood@general.default.akavanagh.uk0.bigv.io) (Remote host closed the connection)
2020-11-13 02:10:51 <blankhart> fair, i was just referring to type checking
2020-11-13 02:12:15 devalot joins (~ident@mail.pmade.com)
2020-11-13 02:12:22 sim590 joins (~sim590@modemcable090.207-203-24.mc.videotron.ca)
2020-11-13 02:13:55 tinwood joins (~tinwood@general.default.akavanagh.uk0.bigv.io)
2020-11-13 02:14:12 <blankhart> monochrom, is the recursion point that you need to separate out let in order to have proper binding groups? i am not quite there yet in studying this so the question may be premature
2020-11-13 02:14:34 <blankhart> but that is what i took you to mean
2020-11-13 02:14:54 <blankhart> oh nevermind i think i see
2020-11-13 02:15:21 <blankhart> you can't have a recursive (anonymous) lambda
2020-11-13 02:15:50 nbloomf joins (~nbloomf@2600:1700:ad14:3020:4085:c5d6:bbdf:5f4e)
2020-11-13 02:15:52 <monochrom> :)
2020-11-13 02:15:55 <unclechu> correct me if my assumption if i’m wrong: using GADTs with constraints on type-level is currently impossible in haskell?
2020-11-13 02:16:02 <unclechu> is my assumption is wrong*
2020-11-13 02:16:19 <unclechu> if my assumption*.. you get it
2020-11-13 02:19:17 g-belmonte joins (~g-belmont@2804:14c:8786:9312:3638:eaf5:dc36:146d)
2020-11-13 02:19:25 × olligobber quits (olligobber@gateway/vpn/privateinternetaccess/olligobber) (Ping timeout: 264 seconds)
2020-11-13 02:21:42 erisco joins (~erisco@d24-57-249-233.home.cgocable.net)

All times are in UTC.