Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→ 502,152 events total
2020-11-04 20:07:47 <matthew-> if I add TypeApp then I guess I should really rework TypeArrow to be l -> r -> TypeApp(TypeApp(Const("->"), l), r)
2020-11-04 20:08:01 <ski> you could probably special case any particular single (possibly recursive) algebraic data type, in a language you're designing
2020-11-04 20:08:28 × thir quits (~thir@p200300f27f0b7e00f4e9381c2bf90854.dip0.t-ipconnect.de) (Remote host closed the connection)
2020-11-04 20:08:44 Guest76112 joins (uid472329@gateway/web/irccloud.com/x-ennruecymrcxflva)
2020-11-04 20:09:49 <matthew-> ski: well if I have empty list constructor and cons as builtins, then I think I can get away with just starting the type inference env with suitable types for both of those functions. I'm just trying to get clear how to actually represent list foo as a type
2020-11-04 20:10:13 × vicfred quits (~vicfred@unaffiliated/vicfred) (Remote host closed the connection)
2020-11-04 20:10:20 cosimone joins (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd)
2020-11-04 20:10:41 vicfred joins (~vicfred@unaffiliated/vicfred)
2020-11-04 20:12:11 xerox_ joins (~xerox@unaffiliated/xerox)
2020-11-04 20:13:31 <ski> specify that empty list has elements of any type you like; and that non-empty list construction takes a value of some type and a list with elements of that type, and gives a list with elements of that type
2020-11-04 20:14:09 × o1lo01ol1o quits (~o1lo01ol1@bl8-213-81.dsl.telepac.pt) (Remote host closed the connection)
2020-11-04 20:14:31 hackage hsdev 0.3.4.0 - Haskell development library https://hackage.haskell.org/package/hsdev-0.3.4.0 (AlexandrRuchkin)
2020-11-04 20:15:36 <ski> to express the above in Haskell terms, given `data List a = Nil | Cons a (List a)', you specify that `Nil :: List a' and `Cons :: a -> List a -> List a' (where `a' is a type variable, `Nil' and `Cons' being polymorphic operations where `a' can be (consistently) replaced by any specific type)
2020-11-04 20:15:42 × knupfer quits (~Thunderbi@200116b82c1ba4001c1efa9cfbaac5ab.dip.versatel-1u1.de) (Ping timeout: 244 seconds)
2020-11-04 20:16:17 <ski> matthew- : however, you'll presumably also want some way to do a case-distinction on whether a list is empty or not (and in the latter case, access the head element, and the tail list)
2020-11-04 20:17:44 <matthew-> yes - I'm doing pattern matching too
2020-11-04 20:18:06 <matthew-> presumably I just use normal inference and then unify the type of the pattern with the type of the expr
2020-11-04 20:19:20 waskell_ joins (~quassel@d66-183-127-166.bchsia.telus.net)
2020-11-04 20:20:17 × nados quits (~dan@69-165-210-185.cable.teksavvy.com) (Remote host closed the connection)
2020-11-04 20:20:28 × Lycurgus quits (~niemand@98.4.97.110) (Quit: Exeunt)
2020-11-04 20:20:45 nados joins (~dan@69-165-210-185.cable.teksavvy.com)
2020-11-04 20:21:00 hackage reflex-gadt-api 0.1.0.0 - Interact with a GADT API in your reflex-dom application. https://hackage.haskell.org/package/reflex-gadt-api-0.1.0.0 (abrar)
2020-11-04 20:21:02 × asthasr quits (~asthasr@162.210.29.120) (Quit: asthasr)
2020-11-04 20:21:54 elliott_ joins (~elliott_@pool-108-51-141-12.washdc.fios.verizon.net)
2020-11-04 20:22:16 × waskell quits (~quassel@d66-183-124-7.bchsia.telus.net) (Ping timeout: 246 seconds)
2020-11-04 20:22:47 × nados quits (~dan@69-165-210-185.cable.teksavvy.com) (Remote host closed the connection)
2020-11-04 20:23:04 nados joins (~dan@69-165-210-185.cable.teksavvy.com)
2020-11-04 20:23:11 × Tario quits (~Tario@201.192.165.173) (Read error: Connection reset by peer)
2020-11-04 20:24:12 × nados quits (~dan@69-165-210-185.cable.teksavvy.com) (Remote host closed the connection)
2020-11-04 20:24:40 nados joins (~dan@69-165-210-185.cable.teksavvy.com)
2020-11-04 20:25:38 <ski> matthew- : yea, should work (in absense of existentials, GADTs, higher-rank). while patterns are more restrictive than expressions, their (type, in this case) behaviour should correspond to each other, on the overlap
2020-11-04 20:26:02 × sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937)
2020-11-04 20:26:10 Franciman joins (~francesco@host-79-36-167-172.retail.telecomitalia.it)
2020-11-04 20:26:39 knupfer joins (~Thunderbi@i5E86B46C.versanet.de)
2020-11-04 20:27:39 <hekkaidekapus> To go overboard, if more powerful patterns are needed, views could come into play. (But that’s another can of worms :)
2020-11-04 20:28:36 <matthew-> ski : cool. I guess it's more: for each fv(pattern), treat as Abs, so introduce new type var. Infer type of branch body, which will constrain these fresh vars. With that info, infer the type of the pattern. And then finally check the pattern type unifies with the case expression type
2020-11-04 20:30:40 <matthew-> and yes, I'm definitely keeping this simple - no higher-rank types, GADTs or other madness ;)
2020-11-04 20:30:58 justanotheruser joins (~justanoth@unaffiliated/justanotheruser)
2020-11-04 20:32:01 × elliott_ quits (~elliott_@pool-108-51-141-12.washdc.fios.verizon.net) (Ping timeout: 264 seconds)
2020-11-04 20:32:28 <ski> you could infer the type of the branch pattern before the type of the branch expression
2020-11-04 20:32:46 <ski> matthew- : HM ?
2020-11-04 20:32:59 britva joins (~britva@31-10-157-156.cgn.dynamic.upc.ch)
2020-11-04 20:36:47 heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-11-04 20:36:55 wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2020-11-04 20:37:13 <ski> matthew- : btw, if you've not seen it, perhaps "Polymorphic Type Inference" by Michael I. Schwartzbach in 1995-03 at <https://cs.au.dk/~amoeller/mis/typeinf.p(s|df)>,<https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.57.1493> could be interesting
2020-11-04 20:38:20 elliott_ joins (~elliott_@pool-108-51-141-12.washdc.fios.verizon.net)
2020-11-04 20:38:52 johnw joins (~johnw@haskell/developer/johnw)
2020-11-04 20:39:54 Tario joins (~Tario@37.218.241.6)
2020-11-04 20:40:36 <hekkaidekapus> matthew-: You can introduce a match construct which takes 2 arguments—a pattern and a value—and either fails or substitues variables in the pattern with values in the value.
2020-11-04 20:40:48 × Tario quits (~Tario@37.218.241.6) (Read error: Connection reset by peer)
2020-11-04 20:40:59 Tario joins (~Tario@201.192.165.173)
2020-11-04 20:41:06 × cosimone quits (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) (Remote host closed the connection)
2020-11-04 20:41:29 cosimone joins (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd)
2020-11-04 20:41:30 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 256 seconds)
2020-11-04 20:42:11 <hekkaidekapus> How to define that construct is discussed in details in Types and Programming Languages.
2020-11-04 20:42:16 × avdb quits (~avdb@ip-62-235-73-30.dsl.scarlet.be) (Ping timeout: 265 seconds)
2020-11-04 20:42:19 <hekkaidekapus> @where TaPL
2020-11-04 20:42:19 <lambdabot> "Types and Programming Languages" by Benjamin C. Pierce in 2002-02-01 at <https://www.cis.upenn.edu/~bcpierce/tapl/>
2020-11-04 20:43:40 <ski> i sortof dislike view patterns ..
2020-11-04 20:43:51 thir joins (~thir@pd9e1bd8a.dip0.t-ipconnect.de)
2020-11-04 20:44:00 <hekkaidekapus> ski: That’s for me?
2020-11-04 20:44:53 <hekkaidekapus> I was really going overboars: it is “views” in the Idris sense.
2020-11-04 20:45:04 <hekkaidekapus> *overboard
2020-11-04 20:47:23 <matthew-> ski: (sorry, was afk). Yes, HM
2020-11-04 20:47:40 wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2020-11-04 20:47:47 × cosimone quits (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) (Remote host closed the connection)
2020-11-04 20:47:53 <ski> i dunno the Idris sense
2020-11-04 20:48:11 cosimone joins (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd)
2020-11-04 20:48:33 <matthew-> yeah, I have physical TAPL and ATTPL back from PhD days some years back...
2020-11-04 20:49:42 <matthew-> ski: thanks for the paper pointer; reading now
2020-11-04 20:50:57 <hekkaidekapus> ski: <https://paste.tomsmeding.com/ifpl4FiR>
2020-11-04 20:51:06 × sfvm quits (~sfvm@37.228.215.148) (Quit: off to the basement, mixing up the medicine)
2020-11-04 20:51:23 × magicman quits (~tchakkazu@static-47-180-28-65.lsan.ca.frontiernet.net) (Quit: Lost terminal)
2020-11-04 20:52:13 × thir quits (~thir@pd9e1bd8a.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
2020-11-04 20:52:22 <bqv> sequence behaves nicely with IO, right?
2020-11-04 20:53:05 <ski> "nicely" means ?
2020-11-04 20:53:30 <ski> hekkaidekapus : why the index ?
2020-11-04 20:53:35 <bqv> i feel like there are gotchas somewhere
2020-11-04 20:53:47 <bqv> but i can't imagine how
2020-11-04 20:54:05 <bqv> if i'm talking nonsense, just means i'm overly paranoid. nevermind :)
2020-11-04 20:54:19 <ski> it's not tail-recursive, if that's what you were wondering about
2020-11-04 20:54:27 × cosimone quits (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) (Ping timeout: 244 seconds)
2020-11-04 20:55:11 <bqv> having trouble figuring the implications of that
2020-11-04 20:56:01 <dsal> Is there an easy way to get GHCI to run in a different Monad?
2020-11-04 20:56:07 <ski> if you use it on a really long list, it'll use a lot of stack
2020-11-04 20:56:16 <dsal> In particular, my own transformer stack over IO
2020-11-04 20:56:23 __xor joins (~xor@74.215.46.133)
2020-11-04 20:56:35 argent0 joins (~argent0@168.227.96.2)
2020-11-04 20:56:36 <bqv> hm, ok
2020-11-04 20:56:41 × _xor quits (~xor@74.215.46.133) (Read error: Connection reset by peer)
2020-11-04 20:56:45 <geekosaur> dsal: there's a command line option
2020-11-04 20:57:10 <ski> not afaik, dsal. i guess you might be able to do some wrapper on each invocation
2020-11-04 20:57:22 <hekkaidekapus> ski: The index transforms input is some preferred forms which can then be inspected with “covering functions”, another Idriss-ism. But I guess I’m way off-topic now.
2020-11-04 20:58:04 <ski> hekkaidekapus : i wonder whether that has any similarity to the (non-dependent) "active patterns" in F#
2020-11-04 20:58:10 <dsal> hmm... Yeah, running my own ghci would be kind of neat if I had an easy way to do that. The way I'm doing it isn't hard enough.
2020-11-04 20:58:37 <hekkaidekapus> ski: Unfortunately, I dunno F# ;)
2020-11-04 20:59:05 <geekosaur> https://downloads.haskell.org/ghc/latest/docs/html/users_guide/ghci.html#using-a-custom-interactive-printing-function note that the type can be something other than IO, although the example is still in IO
2020-11-04 20:59:39 <geekosaur> hm, not qute although it has that C a => so as long as it resolves to IO you're good to go
2020-11-04 20:59:46 <geekosaur> so a stack over IO should work
2020-11-04 21:00:01 <ski> i mean, you could make an `IORef S', and then a combinator that used that, having type `StateT S IO a -> IO a', updating, then wrapping each invocation in the interactor with that combinator

All times are in UTC.