Logs: freenode/#haskell
| 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.