Logs: freenode/#haskell
| 2020-11-18 21:15:30 | hackage | graphula 2.0.0.1 - A declarative library for describing dependencies between data https://hackage.haskell.org/package/graphula-2.0.0.1 (PatrickBrisbin) |
| 2020-11-18 21:15:40 | <dminuoso> | ski: Mm, can you actually express the `exists a. (Ord a,Widget a) => [a]` confusion with a forall encoding? |
| 2020-11-18 21:15:48 | <dminuoso> | (that is the forall continuation encoding) |
| 2020-11-18 21:16:01 | <dminuoso> | Ah I think you should be able to |
| 2020-11-18 21:16:28 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2020-11-18 21:16:33 | <dminuoso> | presumably it'd be: (forall a. [(Ord a, Widget a) => a] -> b) -> b |
| 2020-11-18 21:16:33 | <ski> | and yes, `exists' and `*>' are not valid Haskell (even with extensions) (maybe we'll get `exists', some day. there was another Haskell implementation which had limited support for it). regardless, imho, it's useful to reason in terms of `exists' and `*>', in pseudo-Haskell code, before getting to encoding it (in one of two main ways), in Haskell (with extensions) |
| 2020-11-18 21:16:38 | × | britva quits (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) (Quit: This computer has gone to sleep) |
| 2020-11-18 21:16:54 | <dminuoso> | or... no that doesnt look quite right |
| 2020-11-18 21:17:00 | × | dhouthoo quits (~dhouthoo@ptr-eiv6509pb4ifhdr9lsd.18120a2.ip6.access.telenet.be) (Quit: WeeChat 2.9) |
| 2020-11-18 21:17:04 | → | britva joins (~britva@31-10-157-156.cgn.dynamic.upc.ch) |
| 2020-11-18 21:17:14 | <ski> | dminuoso : not sure what you mean by "express the [..] confusion" |
| 2020-11-18 21:17:27 | <dminuoso> | ski: `exists a. (Ord a,Widget a) => [a]` |
| 2020-11-18 21:17:42 | <ski> | what is the confusion that you want to express ? |
| 2020-11-18 21:17:50 | <dminuoso> | ski: Can you express that term in haskell with forall |
| 2020-11-18 21:17:58 | <ski> | (or do you just mean to express that type, in Haskell with extensions ?) |
| 2020-11-18 21:18:01 | <dminuoso> | Right |
| 2020-11-18 21:18:09 | <dminuoso> | All extensions allowed. |
| 2020-11-18 21:18:13 | <ski> | exists a. (Ord a,Widget a) => [a] |
| 2020-11-18 21:18:30 | × | unfixpoint quits (1f0a965a@31-10-150-90.cgn.dynamic.upc.ch) (Remote host closed the connection) |
| 2020-11-18 21:18:30 | <ski> | = forall o. ((exists a. (Ord a,Widget a) => [a]) -> o) -> o |
| 2020-11-18 21:18:46 | <ski> | = forall o. (forall a. ((Ord a,Widget a) => [a]) -> o) -> o |
| 2020-11-18 21:19:12 | <ski> | (that's using `RankNTypes') |
| 2020-11-18 21:19:13 | <dminuoso> | Ah indeed. |
| 2020-11-18 21:19:33 | → | dcoutts_ joins (~duncan@33.14.75.194.dyn.plus.net) |
| 2020-11-18 21:19:36 | → | unfixpoint joins (1f0a965a@31-10-150-90.cgn.dynamic.upc.ch) |
| 2020-11-18 21:19:48 | <dminuoso> | Oh! And thus answering a question that arised over a year ago, for which I never got a satisfactory answer |
| 2020-11-18 21:19:54 | <ski> | oh ? |
| 2020-11-18 21:20:56 | <dminuoso> | Don't even know the context, but I was wondering about the meaning of `forall a. (ctxt ... => ...)` as opposed to `forall a. ctxt ... => ...` |
| 2020-11-18 21:22:12 | <dexterfoo> | foldr (\i m -> Map.insert i "value" m) Map.empty [1..100] |
| 2020-11-18 21:22:13 | <dexterfoo> | Should i use foldr or foldl'? The Map is strict |
| 2020-11-18 21:22:48 | × | boxscape59 quits (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) (Quit: Connection closed) |
| 2020-11-18 21:22:55 | × | britva quits (~britva@31-10-157-156.cgn.dynamic.upc.ch) (Quit: This computer has gone to sleep) |
| 2020-11-18 21:23:02 | <ski> | dminuoso : er, the precedence i'm using, those two should be the same thing |
| 2020-11-18 21:23:11 | → | boxscape joins (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) |
| 2020-11-18 21:23:37 | <Guest42> | Hi, I have a lambda calucus question. I have to show that if s ⇒βi |
| 2020-11-18 21:23:37 | <Guest42> | s' and s' is in head normal form then s is also in head normal form. Can someone help ? |
| 2020-11-18 21:23:44 | <ski> | ("quantifiers extend/scopes as far right as possible") |
| 2020-11-18 21:25:34 | <ski> | ⌜⇒βi⌝ being ? |
| 2020-11-18 21:26:29 | <dminuoso> | ski: Mmm. Im having a hard time remembering it might have been 2 years ago in fact, my logs dont reach that far back. |
| 2020-11-18 21:27:32 | × | ericsagn1 quits (~ericsagne@2405:6580:0:5100:b570:65da:9eeb:ab03) (Ping timeout: 260 seconds) |
| 2020-11-18 21:27:55 | × | borne quits (~fritjof@200116b864880600f1dc39039d201adf.dip.versatel-1u1.de) (Ping timeout: 272 seconds) |
| 2020-11-18 21:28:15 | <boxscape> | dminuoso do you remember if ctxt is supposed to depend on a? |
| 2020-11-18 21:28:17 | <dminuoso> | Roughly, I was looking into where forall and => could go, and there were some combinations I just couldn't make sense of |
| 2020-11-18 21:28:31 | <dminuoso> | Similar to, but not quite like: withDict :: HasDict c e => e -> (c => r) -> r |
| 2020-11-18 21:28:54 | → | britva joins (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) |
| 2020-11-18 21:29:32 | <ski> | ok |
| 2020-11-18 21:29:51 | <ski> | (boxscape : presumably ?) |
| 2020-11-18 21:29:56 | <Guest42> | =>βi is the smallet relation that is reflexive and s.t if s => s' then λx.s ⇒β λx.s |
| 2020-11-18 21:29:56 | <Guest42> | , |
| 2020-11-18 21:30:03 | <Guest42> | and if |
| 2020-11-18 21:30:27 | <boxscape> | I was thinking maaaybe it could have been forall a . ctxt ... => ... vs cxt => forall a . ..., but of course that wouldn't make sense in that case |
| 2020-11-18 21:30:34 | <dminuoso> | It arised from the question whether: (Show a => a -> IO ()) -> IO () was the same as forall a. (Show a => a -> IO ()) -> IO () |
| 2020-11-18 21:30:39 | <Guest42> | s ⇒β s |
| 2020-11-18 21:30:39 | <Guest42> | and t ⇒β t |
| 2020-11-18 21:30:40 | <Guest42> | alors s t ⇒β s |
| 2020-11-18 21:30:40 | <Guest42> | 0 |
| 2020-11-18 21:30:41 | <Guest42> | t |
| 2020-11-18 21:30:41 | <dminuoso> | That was the story, and my logs do reach that far. :) |
| 2020-11-18 21:30:41 | <Guest42> | 0 |
| 2020-11-18 21:30:42 | <Guest42> | et (λx.s)t ⇒β s |
| 2020-11-18 21:30:42 | <Guest42> | 0 |
| 2020-11-18 21:30:43 | <Guest42> | [t |
| 2020-11-18 21:30:43 | <Guest42> | 0/x |
| 2020-11-18 21:30:45 | × | cads quits (~cads@ip-64-72-99-232.lasvegas.net) (Ping timeout: 256 seconds) |
| 2020-11-18 21:30:57 | <dminuoso> | Guest42: please use a pasting service, you can find one linked in the topic |
| 2020-11-18 21:31:06 | <tomsmeding> | copying from a pdf? ;) |
| 2020-11-18 21:31:06 | → | borne joins (~fritjof@200116b864880600f1dc39039d201adf.dip.versatel-1u1.de) |
| 2020-11-18 21:31:12 | <Guest42> | yeah |
| 2020-11-18 21:31:13 | <ski> | dminuoso : definitely not the same |
| 2020-11-18 21:32:00 | hackage | phonetic-languages-examples 0.6.2.0 - A generalization of the uniqueness-periods-vector-examples functionality. https://hackage.haskell.org/package/phonetic-languages-examples-0.6.2.0 (OleksandrZhabenko) |
| 2020-11-18 21:32:50 | × | cosimone quits (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) (Quit: cosimone) |
| 2020-11-18 21:32:51 | → | nuncanada joins (~dude@179.235.160.168) |
| 2020-11-18 21:32:51 | <boxscape> | % testing42 :: (Show a => a -> IO ()) -> IO (); testing42 = undefined |
| 2020-11-18 21:32:52 | <yahb> | boxscape: |
| 2020-11-18 21:32:54 | <boxscape> | % :t +v testing42 |
| 2020-11-18 21:32:54 | <yahb> | boxscape: forall a. (Show a => a -> IO ()) -> IO () |
| 2020-11-18 21:32:59 | <boxscape> | is that not the second one? |
| 2020-11-18 21:33:17 | <boxscape> | seems like ghc infers them to be the same? |
| 2020-11-18 21:33:29 | <boxscape> | s/infer/does something to them |
| 2020-11-18 21:33:52 | <ski> | Guest42 : hm, so beta-reducing some number of parallel subexpressions (including reducing under lambda) |
| 2020-11-18 21:34:55 | <ski> | boxscape : in that context, the former is interpreted to have an implicit/elided `forall', and so is equivalent to the latter (with some caveats like `ScopedTypeVariables' ..) |
| 2020-11-18 21:35:22 | <boxscape> | ski so that means the context in dminuoso's question was implied to be different? |
| 2020-11-18 21:35:44 | <ski> | boxscape : but consider `data Foo a = MkFoo {testing42 :: (Show a => a -> IO ()) -> IO ()}' vs. `data Foo a = MkFoo {testing42 :: forall a. (Show a => a -> IO ()) -> IO ()}' -- these are not the same |
| 2020-11-18 21:35:53 | <boxscape> | ah, that's fair |
| 2020-11-18 21:35:53 | <unfixpoint> | I will never understand how ScopedTypeVariables is not default |
| 2020-11-18 21:35:59 | → | alp joins (~alp@2a01:e0a:58b:4920:7462:8d66:154:f167) |
| 2020-11-18 21:36:03 | <koz_> | unfixpoint: Because Haskell2010 doesn't have it. |
| 2020-11-18 21:36:06 | <dminuoso> | unfixpoint: historical reasons. |
| 2020-11-18 21:36:09 | <dolio> | dminuoso: Those types are the same. |
| 2020-11-18 21:36:13 | <unfixpoint> | Yeah, I know.. but wtf |
| 2020-11-18 21:36:16 | <koz_> | dminuoso: Was about to say 'hysterical raisins'. |
| 2020-11-18 21:36:17 | <ski> | `(Show a => a -> IO ()) -> IO ()' is a type expression with a free (type) variable. `forall a. (Show a => a -> IO ()) -> IO ()' isn't |
| 2020-11-18 21:36:19 | → | cads joins (~cads@ip-64-72-99-232.lasvegas.net) |
| 2020-11-18 21:36:31 | <dminuoso> | dolio: I know |
| 2020-11-18 21:36:32 | <koz_> | unfixpoint: Hysterical raisins is an explanation of many wtf phenomena, Haskell or otherwise. |
| 2020-11-18 21:36:39 | <dolio> | Oh, okay. |
| 2020-11-18 21:36:43 | <boxscape> | apparently there's some infelicities with ScopedTypeVariables that, if the stars align just right, might be fixed before something like it becomes standard, but I don't quite remember what they were |
| 2020-11-18 21:36:44 | <Guest42> | => is the beta parrallell reduction |
| 2020-11-18 21:36:49 | <ski> | imho, the behaviour of `ScopedTypeVariables' is the opposite of what it ought to be .. |
All times are in UTC.