Logs: freenode/#haskell
| 2020-11-18 21:36:56 | × | cr3 quits (~cr3@192-222-143-195.qc.cable.ebox.net) (Ping timeout: 240 seconds) |
| 2020-11-18 21:37:00 | <dminuoso> | dolio: I copied the line that, roughly, was at the starting point of all of this. |
| 2020-11-18 21:37:08 | <dminuoso> | % foo :: forall a. (Show a => a -> IO ()) -> IO (); foo = undefined |
| 2020-11-18 21:37:08 | <yahb> | dminuoso: |
| 2020-11-18 21:37:10 | <ski> | Guest42 : single-parallel-step, yes |
| 2020-11-18 21:37:14 | <dminuoso> | % bar :: (forall a. Show a => a -> IO ()) -> IO (); bar = undefined |
| 2020-11-18 21:37:14 | <yahb> | dminuoso: |
| 2020-11-18 21:37:25 | × | britva quits (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) (Quit: This computer has gone to sleep) |
| 2020-11-18 21:37:38 | <Guest42> | ski: i think the i notes how many steps |
| 2020-11-18 21:37:42 | <unfixpoint> | At least it makes me crack up everytime because I always misspell it. So it will suggest me NoScopedTypevariables too. I don't even play video games but I know about no scoping >.> |
| 2020-11-18 21:37:45 | <Guest42> | but i'm not sure |
| 2020-11-18 21:38:30 | <dexterfoo> | any help with my question about foldr/foldl'? |
| 2020-11-18 21:38:36 | <ski> | Guest42 : hm, just noticed the ⌜i⌝ isn't there in what you wrote after "the smallet relation that" |
| 2020-11-18 21:39:02 | <Guest42> | yeah beause I think I made a mistake |
| 2020-11-18 21:39:21 | → | ericsagn1 joins (~ericsagne@2405:6580:0:5100:8c9:42ac:c0f6:8508) |
| 2020-11-18 21:39:38 | × | knupfer quits (~Thunderbi@200116b8244bd600690e470b1c9f0b95.dip.versatel-1u1.de) (Ping timeout: 264 seconds) |
| 2020-11-18 21:40:23 | <Guest42> | I have to write what it is in a paste website thing. I'll send the link once I'm finished |
| 2020-11-18 21:41:02 | <unfixpoint> | Use foldl' as you want to fold everything, but you could also just use fromList I think. |
| 2020-11-18 21:41:16 | <ski> | boxscape : imho, with `foo :: forall a. ..a..; foo = ...', the `a' bound by `forall a.' in the signature ought not to be in scope in the body `...'; while with `foo :: ..a..; foo = ...' (and an extension), it could make sense for `a' to be in scope in `...' |
| 2020-11-18 21:41:51 | <dminuoso> | dexterfoo: hard to say in general without knowing the details |
| 2020-11-18 21:41:59 | <c_wraith> | dexterfoo: foldl', for two reasons. 1) there's no meaningful result from evaluating just some of the list. 2) The result is a single value that you want to not have referring to previous versions of itself |
| 2020-11-18 21:42:27 | <dminuoso> | dexterfoo: Roughly, foldr is a good and safe default (because of how it plays with lazyness), foldl' is more rarely a better choice unless you know you will force the entire structure anyway. |
| 2020-11-18 21:42:55 | <dexterfoo> | dminuoso: thank you. i pasted a line of code that builds a Strict Map |
| 2020-11-18 21:42:59 | <c_wraith> | dexterfoo: and FWIW, in that case the fact that it's Data.Map.Strict is irrelevant. It will do the exact same thing with Data.Map.Lazy |
| 2020-11-18 21:43:03 | <dminuoso> | dexterfoo: the example seems contrived. |
| 2020-11-18 21:43:09 | <ski> | (should there be two versions of `TypeApplications', one only allowing it with values which have been given a type with explicit `forall's ?) |
| 2020-11-18 21:43:45 | <dminuoso> | ski: There's an accepted proposal to provide value level binders. |
| 2020-11-18 21:44:21 | <dminuoso> | With a syntax like `f @a x = ...` |
| 2020-11-18 21:44:23 | → | chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) |
| 2020-11-18 21:44:23 | <ski> | i recall hearing about it, i think, but it not being finished then |
| 2020-11-18 21:44:43 | <unfixpoint> | TIL `id @(forall a. a -> a) 101` won't work |
| 2020-11-18 21:45:09 | × | coot quits (~coot@37.30.49.253.nat.umts.dynamic.t-mobile.pl) (Quit: coot) |
| 2020-11-18 21:45:28 | <unfixpoint> | dminuoso: Can you not have `f (x :: a) = ...`, does it not bind `a`? |
| 2020-11-18 21:45:32 | <dminuoso> | dexterfoo: but yeah, for inserting into a map, a foldl' is likely the better candidate |
| 2020-11-18 21:45:37 | <ski> | yea, makes sense (apart from it appearing confusingly similar to as-patterns). so `foo :: forall a. ..a..; foo @a = ..a..' would make sense, but those would be two different `a' type variables |
| 2020-11-18 21:45:40 | × | geekosaur quits (82659a09@host154-009.vpn.uakron.edu) (Remote host closed the connection) |
| 2020-11-18 21:46:46 | <ski> | % id @(forall a. a -> a) id 101 |
| 2020-11-18 21:46:46 | <yahb> | ski: 101 |
| 2020-11-18 21:47:00 | <dexterfoo> | thank you unfixpoint dminuoso c_wraith |
| 2020-11-18 21:47:09 | <ski> | % id @(forall a. a -> a) False |
| 2020-11-18 21:47:10 | <yahb> | ski: ; <interactive>:211:24: error:; * Couldn't match expected type `a1 -> a1' with actual type `Bool'; * In the second argument of `id', namely `False'; In the expression: id @(forall a. a -> a) False; In an equation for `it': it = id @(forall a. a -> a) False |
| 2020-11-18 21:47:22 | <unfixpoint> | TypeApplication is meant to apply though, what is the proposal? |
| 2020-11-18 21:47:37 | <dminuoso> | https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0155-type-lambda.rst |
| 2020-11-18 21:47:50 | <unfixpoint> | Binding with `::` is good enough :S |
| 2020-11-18 21:48:31 | <ski> | unfixpoint : doesn't specify ordering too clearly |
| 2020-11-18 21:50:05 | ski | . o O ( `(map _) [] = []; map_f@(map f) ((f -> y):(map_f -> ys)) = y:ys' ) |
| 2020-11-18 21:50:08 | <Guest42> | we define an internal parralel reduction rule inductively by with the following rules: https://imgur.com/a/heRxIIw Intuitively it the parralel reduction we forbid to reduce the redex in head. Show that if s => s' and s' in normal head form then s is in normal head form. |
| 2020-11-18 21:50:29 | × | gumbish quits (4913050a@c-73-19-5-10.hsd1.wa.comcast.net) (Ping timeout: 245 seconds) |
| 2020-11-18 21:50:47 | × | stree quits (~stree@50-108-97-52.adr01.mskg.mi.frontiernet.net) (Quit: Caught exception) |
| 2020-11-18 21:51:02 | <Guest42> | Intuitively it is the parrallel reduction where we forbid* |
| 2020-11-18 21:51:02 | <dminuoso> | unfixpoint: GHC uses a variant of System F as its intermediate language, which essentially provides binders for type variables. So rather than `\x.x` you'd write `/\t.\x^t.x`. TypeApplications exist both to elaborate programs during type checking, as well as providing a more convenient and explicit way to do this on the Haskell level. |
| 2020-11-18 21:51:08 | → | stree joins (~stree@50-108-97-52.adr01.mskg.mi.frontiernet.net) |
| 2020-11-18 21:51:25 | <hekkaidekapus> | ski: Bring back PatternSignatures? |
| 2020-11-18 21:51:28 | → | brodie_ joins (~brodie@207.53.253.137) |
| 2020-11-18 21:51:28 | <dminuoso> | unfixpoint: The above proposal just brings this to a conclusion and makes the TypeApplications consistent with that. |
| 2020-11-18 21:52:17 | → | mbomba joins (~mbomba@bras-base-toroon2719w-grc-49-142-114-9-241.dsl.bell.ca) |
| 2020-11-18 21:52:20 | <ski> | hekkaidekapus : yea, i'd like being able to say `map (f :: a -> b) (xs :: [a]) :: [b] = ...' (including result ascription) |
| 2020-11-18 21:52:48 | <dminuoso> | Also, the pattern type signatures of ScopedTypeVariables is relatively noisy because it adds an unnecessary dimension |
| 2020-11-18 21:52:55 | <hekkaidekapus> | ski: I agree. That sentence is the title of a proposal, IIRC. |
| 2020-11-18 21:52:57 | → | falafel joins (~falafel@2601:547:1303:b30:7811:313f:d0f3:f9f4) |
| 2020-11-18 21:53:03 | <ski> | (or `map @a @b (f :: a -> b) (xs :: [a]) :: [b] = ...', if combined with the above proposal) |
| 2020-11-18 21:53:16 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 2020-11-18 21:53:19 | × | Ariakenom quits (~Ariakenom@h-98-128-229-104.NA.cust.bahnhof.se) (Quit: Leaving) |
| 2020-11-18 21:53:33 | <hekkaidekapus> | (But I was rejected I don’t recall for what reasons.) |
| 2020-11-18 21:53:38 | × | brodie_ quits (~brodie@207.53.253.137) (Client Quit) |
| 2020-11-18 21:54:07 | <dminuoso> | unfixpoint: In the lambda cube, we say that polymorphism gives us terms binding types. So why not provide proper binders for what we semantically already have. :) |
| 2020-11-18 21:54:21 | <dolio> | At the very least, there needs to be another way of accomplishing that, because that syntax is awful. |
| 2020-11-18 21:54:25 | <unfixpoint> | Wait how did you get `id @(forall a . a -> a ) id 101` to work? |
| 2020-11-18 21:54:45 | <unfixpoint> | Do I need newer GHC than 8.4.4? |
| 2020-11-18 21:54:57 | × | Franciman quits (~francesco@host-82-56-223-169.retail.telecomitalia.it) (Quit: Leaving) |
| 2020-11-18 21:55:08 | <hekkaidekapus> | ski: Result ascription has another proposal, dunno its state. |
| 2020-11-18 21:55:25 | <unfixpoint> | why is my GHC so old.. |
| 2020-11-18 21:55:29 | <ski> | Guest42 : hm, so no beta at top-level (nor in operator position, if top-level is an application, continuing heriditarily) |
| 2020-11-18 21:55:33 | <dminuoso> | hekkaidekapus: Is result ascriptions akin to how we ascript tyfams? |
| 2020-11-18 21:55:57 | <ski> | unfixpoint : you forgot to pass `id' as argument |
| 2020-11-18 21:55:59 | <dminuoso> | (also, can we get separate type family kind signatures?) |
| 2020-11-18 21:56:01 | <hekkaidekapus> | dminuoso: See ski’s example. |
| 2020-11-18 21:56:14 | <dminuoso> | hekkaidekapus: Ah indeed it looks like it. |
| 2020-11-18 21:56:46 | <ski> | (the MLs have result ascriptions) |
| 2020-11-18 21:57:25 | <hekkaidekapus> | dminuoso: Isn’t TF kind signatures realised by StandaloneKindSigs? |
| 2020-11-18 21:57:33 | <unfixpoint> | Yeah, but even so. It gives "GHC doesn't yet support impredicative polymorphism" for me |
| 2020-11-18 21:57:37 | <dminuoso> | unfixpoint: You just need to flip on ImpredicativeTypes |
| 2020-11-18 21:57:49 | <boxscape> | just pretend it supports them |
| 2020-11-18 21:57:51 | <dminuoso> | A notoriously buggy extension |
| 2020-11-18 21:58:04 | <dminuoso> | It crashes GHC, or your program, or who knows. |
| 2020-11-18 21:58:10 | <p0a> | Guest42: This channel is about Haskell... |
| 2020-11-18 21:58:11 | <boxscape> | though HEAD now has a new implementation, so that's nice |
| 2020-11-18 21:58:14 | <unfixpoint> | I'd rather not enable something that is "extremely flaky support" |
| 2020-11-18 21:58:20 | <ski> | iirc, there was a new idea for how to implement it, recently |
| 2020-11-18 21:58:40 | <dolio> | I don't think ImpredicativeTypes crashes anything. |
| 2020-11-18 21:58:45 | <dolio> | It just doesn't work very well. |
| 2020-11-18 21:58:48 | <unfixpoint> | Aaanyway, I should focus on other things for now. Thanks for all the help and interesting discussions |
| 2020-11-18 21:59:03 | <boxscape> | ski https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3220 |
| 2020-11-18 21:59:09 | <unfixpoint> | Thanks for the papers too, I'll check them later |
| 2020-11-18 21:59:23 | <chkno> | Is there a better way to do a lint-style check for partial function usage than egrep -wr '!!|fromJust|head|init|last|maximum|minimum|read|tail' ? |
| 2020-11-18 22:00:01 | <dminuoso> | chkno: You could also use a different prelude I guess. |
| 2020-11-18 22:00:06 | → | rprije joins (~rprije@124.148.131.132) |
| 2020-11-18 22:00:22 | <unfixpoint> | Solve Halting problem first |
| 2020-11-18 22:00:28 | × | seanparsons quits (~sean@cpc145088-gill21-2-0-cust281.20-1.cable.virginm.net) (Quit: ZNC 1.8.1 - https://znc.in) |
| 2020-11-18 22:00:30 | × | Varis quits (~Tadas@unaffiliated/varis) (Read error: Connection reset by peer) |
All times are in UTC.