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