Logs: freenode/#haskell
| 2021-04-13 17:06:47 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 2021-04-13 17:06:49 | <ski> | perhaps you could use unusual grammatical forms .. |
| 2021-04-13 17:06:54 | <ski> | .. oh, they keft |
| 2021-04-13 17:07:08 | × | rond_ quits (5940206b@89-64-32-107.dynamic.chello.pl) (Quit: Connection closed) |
| 2021-04-13 17:08:04 | → | jonathanx_ joins (~jonathan@h-176-109.A357.priv.bahnhof.se) |
| 2021-04-13 17:08:38 | × | idhugo quits (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) (Ping timeout: 240 seconds) |
| 2021-04-13 17:09:35 | × | jonathanx quits (~jonathan@h-176-109.A357.priv.bahnhof.se) (Ping timeout: 246 seconds) |
| 2021-04-13 17:18:59 | × | kritzefitz quits (~kritzefit@212.86.56.80) (Remote host closed the connection) |
| 2021-04-13 17:19:05 | × | HannaM quits (~quassel@p54849510.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 2021-04-13 17:19:18 | → | HannaM joins (~quassel@p54849510.dip0.t-ipconnect.de) |
| 2021-04-13 17:20:20 | → | fiedlr joins (~fiedlr@83.148.33.254) |
| 2021-04-13 17:20:26 | × | Rudd0 quits (~Rudd0@185.189.115.108) (Ping timeout: 240 seconds) |
| 2021-04-13 17:22:29 | → | jaykru joins (~user@unaffiliated/jaykru) |
| 2021-04-13 17:24:02 | × | ddellacosta quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 2021-04-13 17:24:38 | <jaykru> | does anybody here have experience with Gloss? I'm having trouble with `simulate`, which is successfully updating my state (as confirmed by a trace call) but not updating the display of my state :/ Is there a less magical way to work with real-time display updates in this library so I have more hope of figuring out what's going on? |
| 2021-04-13 17:24:43 | → | kristijonas_ joins (~kristijon@78-56-32-39.static.zebra.lt) |
| 2021-04-13 17:26:11 | × | kristijonas quits (~kristijon@78-56-32-39.static.zebra.lt) (Ping timeout: 240 seconds) |
| 2021-04-13 17:29:00 | → | acarrico joins (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) |
| 2021-04-13 17:29:48 | × | kini quits (~kini@unaffiliated/kini) (Remote host closed the connection) |
| 2021-04-13 17:31:08 | → | kini joins (~kini@unaffiliated/kini) |
| 2021-04-13 17:32:07 | → | Pickchea joins (~private@unaffiliated/pickchea) |
| 2021-04-13 17:32:34 | → | gitgood joins (~gitgood@80-44-9-246.dynamic.dsl.as9105.com) |
| 2021-04-13 17:35:06 | × | ubert quits (~Thunderbi@77.119.128.21.wireless.dyn.drei.com) (Ping timeout: 240 seconds) |
| 2021-04-13 17:35:47 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 2021-04-13 17:36:16 | → | Sheilong joins (uid293653@gateway/web/irccloud.com/x-ljvkmqtgqlpdhiue) |
| 2021-04-13 17:37:08 | × | ram19890 quits (~ram@49.207.130.109) (Quit: Konversation terminated!) |
| 2021-04-13 17:38:31 | → | justan0theruser joins (~justanoth@unaffiliated/justanotheruser) |
| 2021-04-13 17:38:35 | × | justanotheruser quits (~justanoth@unaffiliated/justanotheruser) (Ping timeout: 250 seconds) |
| 2021-04-13 17:38:56 | → | grimpeux joins (~textual@modemcable153.12-178-173.mc.videotron.ca) |
| 2021-04-13 17:39:53 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Ping timeout: 250 seconds) |
| 2021-04-13 17:42:40 | → | idhugo joins (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) |
| 2021-04-13 17:45:05 | × | grimpeux quits (~textual@modemcable153.12-178-173.mc.videotron.ca) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-04-13 17:45:32 | → | ddellacosta joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 2021-04-13 17:49:08 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-04-13 17:49:55 | → | grimpeux joins (~textual@modemcable153.12-178-173.mc.videotron.ca) |
| 2021-04-13 17:50:10 | × | ddellacosta quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Ping timeout: 265 seconds) |
| 2021-04-13 17:52:06 | × | zebrag quits (~inkbottle@aaubervilliers-654-1-2-51.w83-200.abo.wanadoo.fr) (Quit: Konversation terminated!) |
| 2021-04-13 17:52:25 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-2-51.w83-200.abo.wanadoo.fr) |
| 2021-04-13 17:52:55 | × | amerigo quits (uid331857@gateway/web/irccloud.com/x-nxarbmfdflgljuos) (Quit: Connection closed for inactivity) |
| 2021-04-13 17:57:58 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 2021-04-13 17:58:02 | → | hypercube joins (hypercube@gateway/vpn/protonvpn/hypercube) |
| 2021-04-13 17:58:05 | <wroathe> | Is the point of explicitly universally quantifying a type to imply that the types not explicitly universally quantified are instead existentially quantified? |
| 2021-04-13 17:58:15 | <wroathe> | i.e. the forall x. syntax |
| 2021-04-13 17:58:42 | → | vicfred joins (~vicfred@unaffiliated/vicfred) |
| 2021-04-13 17:59:37 | → | frozenErebus joins (~frozenEre@37.231.244.249) |
| 2021-04-13 18:00:42 | <monochrom> | No. |
| 2021-04-13 18:01:10 | <wroathe> | Well, types are implicitly universall quantified by default, right? |
| 2021-04-13 18:01:15 | <monochrom> | Yes. |
| 2021-04-13 18:01:18 | <wroathe> | universally* |
| 2021-04-13 18:01:55 | <wroathe> | No further questions, your honor. |
| 2021-04-13 18:02:20 | <monochrom> | :) |
| 2021-04-13 18:02:22 | <ski> | "Well, types are implicitly universall quantified by default, right?" -- no |
| 2021-04-13 18:02:41 | <ski> | type signature are (except for in some cases) |
| 2021-04-13 18:02:51 | <wroathe> | type variables, I meant |
| 2021-04-13 18:02:53 | <wroathe> | sorry |
| 2021-04-13 18:03:16 | <ski> | when you talk about quantification, or any binder, you must ask "where ?" |
| 2021-04-13 18:03:46 | → | alexm_ joins (~alexm_@161.8.254.229) |
| 2021-04-13 18:03:50 | <ski> | it's not the case that `[a] -> [a]' "is short for" `forall a. [a] -> [a]', e.g. |
| 2021-04-13 18:05:34 | × | idhugo quits (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) (Ping timeout: 252 seconds) |
| 2021-04-13 18:06:02 | <ski> | if it was, then e.g. `([a] -> [a]) -> [[a]] -> [[a]]' would mean the same as `(forall a. [a] -> [a]) -> [[a]] -> [[a]]', and `data ListTransf a = LT ([a] -> [a])' would mean the same as `data ListTransf a = LT (forall a. [a] -> [a])'. neither of which are actually the case |
| 2021-04-13 18:07:10 | <ski> | in most circumstances, a type *signature* without explicit quantification really means a corresponding one, where there's been added a `forall' just after the `::', binding the (free) type variables in the type |
| 2021-04-13 18:08:06 | × | alexm_ quits (~alexm_@161.8.254.229) (Ping timeout: 252 seconds) |
| 2021-04-13 18:08:08 | → | ram19890 joins (~ram@49.207.130.109) |
| 2021-04-13 18:08:51 | → | xprl-gjf joins (~gavin@98.154.147.147.dyn.plus.net) |
| 2021-04-13 18:09:07 | <ski> | exceptions are e.g. `data ListTransf a = LT {appListTransf :: [a] -> [a]}', and `class Eq a where (==) :: a -> a -> Bool' (which does not mean `class Eq a where (==) :: forall a. a -> a -> Bool'. `(==)' is a monomorphic method, not a polymorphic one. `fmap', otoh is polymorphic, since it really is `class Functor f where fmap :: forall a b. (a -> b) -> (f a -> f b)') |
| 2021-04-13 18:09:10 | <wroathe> | ski: It was a half-assed question that monochrom correctly called me out on. I'm still working through that Typing Haskell in Haskell paper and it occurred to me while I was writing the pattern type inference routine that I still have no idea how any of that forall. stuff works. |
| 2021-04-13 18:09:45 | <wroathe> | ski: But there's plenty of resources to learn about it online, and so don't trouble yourself |
| 2021-04-13 18:10:28 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 2021-04-13 18:10:48 | <[exa]> | wroathe: forall is only very implicitly present in THIH, they don't really implement any higher-order polymorphism |
| 2021-04-13 18:11:00 | <ski> | also, if you have a local signature inside a `where' or `let', which mentions a type variable bound by a type signature accompanying the outer defining equation (and `ScopedTypeVariables' is enables). (also, with `InstanceSigs', you can also put signatures inside `instance' declarations, and then tyvars mentioned in the head of the instance are in scope, so not "implicitly quantified", for the method type |
| 2021-04-13 18:11:02 | <monochrom> | I forgot: Does Typing Haskell in Haskell has an explicit forall internally? |
| 2021-04-13 18:11:06 | <ski> | signatures) |
| 2021-04-13 18:11:07 | × | whataday quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 2021-04-13 18:11:20 | <[exa]> | monochrom: iirc not |
| 2021-04-13 18:11:35 | <ski> | anyway, "implicit universal quantification" is nothing deep at all. it's just a convenient shorthand, to avoid explicitly spelling out `forall's all the time |
| 2021-04-13 18:11:52 | <wroathe> | They've got this constructor: data Scheme = Forall [Kind] (Qual Type) |
| 2021-04-13 18:12:09 | <monochrom> | Oh, that. |
| 2021-04-13 18:12:11 | <wroathe> | Which might not be the same thing. I'm hoping this paper will start making sense as I put the full type inference algorithm together |
| 2021-04-13 18:12:14 | → | whataday joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 2021-04-13 18:12:16 | <ski> | wroathe : did i mention "Polymorphic Type Inference" to you, already ? |
| 2021-04-13 18:12:25 | <[exa]> | THIH implements HM with typeclasses, recursion, context splits for local definitions, and some other minor goodies |
| 2021-04-13 18:12:29 | <wroathe> | ski: Not sure |
| 2021-04-13 18:12:44 | <ski> | "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> |
| 2021-04-13 18:12:50 | <[exa]> | wroathe: the "forall" in THIH is, more or less, the one from Hindley-Milner type system, which is only allowed once per polytype. |
| 2021-04-13 18:12:52 | <ski> | also, perhaps |
| 2021-04-13 18:12:56 | <ski> | @where on-understanding |
| 2021-04-13 18:12:56 | <lambdabot> | "On Understanding Types, Data Abstraction, and Polymorphism" by Luca Cardelli,Peter Wegner in 1985-12 at <http://lucacardelli.name/Papers/OnUnderstanding.A4.pdf> |
| 2021-04-13 18:12:59 | <ski> | @where on-understanding-revisited |
| 2021-04-13 18:12:59 | <lambdabot> | "On Understanding Data Abstraction, Revisited" by William R. Cook in 2009-10 at <http://www.cs.utexas.edu/~wcook/Drafts/2009/essay.pdf> |
| 2021-04-13 18:13:24 | <ski> | could be interesting, for further information relating to polymorphism/universals, and also to existentials (and relation to OO, and ADTs) |
| 2021-04-13 18:13:31 | wroathe | writes down the word polytype |
| 2021-04-13 18:14:23 | <monochrom> | OK, so in HM the dichotomy is "implicitly universally quantified" vs "an unknown waiting to be solved". |
| 2021-04-13 18:14:42 | <monochrom> | rather than universal vs existential |
| 2021-04-13 18:15:23 | <ski> | (oh, and regrettably, people often say "polymorphic type", when they really mean "universally quantified type". imho "polymorphic type" is something completely different. e.g. `forall a. a -> a' is not a polymorphic type (it is monomorphic, having kind `*'/`Type'). however `Const' (of kind `forall k. Type -> k -> Type' is a polymorphic type. also `Proxy') |
| 2021-04-13 18:15:36 | <monochrom> | people usually say "meta variable" for "unknown waiting to be solved". But I hate it. |
| 2021-04-13 18:15:54 | <[exa]> | +1 against metavariables |
| 2021-04-13 18:15:56 | <ski> | whyso ? |
| 2021-04-13 18:16:07 | <wroathe> | ski: So is your definition of polymorphic then that it has any kind, including *? |
| 2021-04-13 18:16:27 | <monochrom> | piling higher and deeper on the word "variable" |
| 2021-04-13 18:16:57 | <ski> | wroathe : no. a polymorphic value is one whose type is of the shape `forall a. ..a..'. a polymorphic type is one whose kind is of the shape `forall k. ..k..' -- i think that's the shortest way to put it |
All times are in UTC.