Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 103 104 105 106 107 108 109 110 111 112 113 .. 5022
— 502,152 events total
2020-09-21 01:45:11 <ski> so if you see e.g.
2020-09-21 01:45:19 <ski> length :: [a] -> Int
2020-09-21 01:45:21 <ski> or
2020-09-21 01:45:31 <ski> take :: Int -> [a] -> [a]
2020-09-21 01:45:32 <ski> or
2020-09-21 01:45:41 <ski> sort :: Ord a => [a] -> [a]
2020-09-21 01:45:49 <ski> then these really mean
2020-09-21 01:45:58 <ski> length :: forall a. [a] -> Int
2020-09-21 01:46:04 <ski> take :: forall a. Int -> [a] -> [a]
2020-09-21 01:46:08 <ski> sort :: forall a. Ord a => [a] -> [a]
2020-09-21 01:46:46 <zebrag> ok
2020-09-21 01:47:01 <ski> however : this does not mean that e.g. `[a] -> [a]' "really means" `forall a. [a] -> [a]' !
2020-09-21 01:47:44 <ski> since, in that case, `foo :: ([a] -> [a]) -> ([a] -> [a])' could be argued to "really mean" `foo :: (forall a. [a] -> [a]) -> (forall a. [a] -> [a])', which is incorrect
2020-09-21 01:48:17 <ski> similarly, `data Foo a = MkFoo ([a] -> [a])' does not mean `data Foo a = MkFoo (forall a. [a] -> [a])'
2020-09-21 01:48:40 <ski> the implicit `forall' is only inserted, right after the `::', in a type signature
2020-09-21 01:49:43 <ski> and even then, there are a few exceptions, which boil down to the type variable(s) in question already being in scope. e.g. in `data Foo a = MkFoo {unFoo :: [a] -> [a]}', `a' is already in scope, bound by the `data Foo a =' "head" part
2020-09-21 01:50:23 <ski> also, in `class Eq a where (==) :: a -> a -> Bool', `a' is already in scope, when we reach the type signature. so, this does not mean `class Eq a where (==) :: forall a. a -> a -> Bool'
2020-09-21 01:50:37 <ski> (`(==)' is a monomorphic class method)
2020-09-21 01:50:47 × thir quits (~thir@p200300f27f0fc600ed2222922a5678d5.dip0.t-ipconnect.de) (Remote host closed the connection)
2020-09-21 01:51:06 <ski> (i mention this, because these seems to be common confusions about where implicit `forall's are inserted)
2020-09-21 01:51:15 → thir joins (~thir@p200300f27f0fc600ed2222922a5678d5.dip0.t-ipconnect.de)
2020-09-21 01:51:39 <ski> anyway, `length :: forall a. [a] -> Int' means that : for every type `a', `length' can be used as having type `[a] -> Int'
2020-09-21 01:51:59 <ski> strictly speaking, `length' is not a function, but a "polymorphic value"
2020-09-21 01:52:48 × cosimone quits (~cosimone@5.170.241.4) (Quit: Quit.)
2020-09-21 01:53:17 <ski> however, when going from `length :: forall a. [a] -> Int' to say `length :: [String] -> Int', specializing the polymorphic value, to a function in this case, we don't actually write anything more than `length'
2020-09-21 01:53:44 → inkbottle joins (~inkbottle@aaubervilliers-654-1-112-119.w86-198.abo.wanadoo.fr)
2020-09-21 01:54:01 <ski> (well, there is now an extension that allows one to explicitly write the specialization as `length @String', meaning that we pick `a' to be `String', so that this whole thing has type `[String] -> Int')
2020-09-21 01:54:13 × zebrag quits (~inkbottle@aaubervilliers-654-1-99-86.w86-212.abo.wanadoo.fr) (Ping timeout: 264 seconds)
2020-09-21 01:54:20 → nbloomf joins (~nbloomf@2600:1700:83e0:1f40:10e:bca5:1dcc:68c6)
2020-09-21 01:54:27 → tsrt^ joins (tsrt@ip98-184-89-2.mc.at.cox.net)
2020-09-21 01:55:12 → ddellacosta joins (~dd@86.106.121.168)
2020-09-21 01:55:56 × adamwespiser quits (~adam_wesp@209.6.42.110) (Remote host closed the connection)
2020-09-21 01:56:32 × Gurkenglas quits (~Gurkengla@unaffiliated/gurkenglas) (Ping timeout: 256 seconds)
2020-09-21 01:57:48 × suppi quits (~suppi@2605:f700:40:c00::e6fc:6842) (Ping timeout: 246 seconds)
2020-09-21 01:58:17 × thir quits (~thir@p200300f27f0fc600ed2222922a5678d5.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
2020-09-21 02:00:44 <inkbottle> ski: zebrag -> inkbottle; I'm still reading https://wiki.haskell.org/Rank-N_types, I think it was a very good suggestion
2020-09-21 02:01:00 → suppi joins (~suppi@2605:f700:40:c00::e6fc:6842)
2020-09-21 02:01:51 <ski> ah, ok
2020-09-21 02:02:22 × xff0x quits (~fox@2001:1a81:53e2:5200:158c:d17f:d83e:dc7f) (Ping timeout: 260 seconds)
2020-09-21 02:04:08 → xff0x joins (~fox@2001:1a81:53e9:6d00:158c:d17f:d83e:dc7f)
2020-09-21 02:04:13 → blankhart joins (~blankhart@pool-100-35-219-3.nwrknj.fios.verizon.net)
2020-09-21 02:04:23 <ski> inkbottle : did the above explanation make sense, so far ?
2020-09-21 02:07:34 × isovector1 quits (~isovector@d207-81-8-13.bchsia.telus.net) (Ping timeout: 272 seconds)
2020-09-21 02:09:14 → eric joins (~eric@191.193.105.46)
2020-09-21 02:09:25 × fulc9277 quits (~fulc927@unaffiliated/fulc927) (Ping timeout: 240 seconds)
2020-09-21 02:09:50 × eric quits (~eric@191.193.105.46) (Read error: Connection reset by peer)
2020-09-21 02:09:59 × danvet_ quits (~Daniel@2a02:168:57f4:0:efd0:b9e5:5ae6:c2fa) (Ping timeout: 272 seconds)
2020-09-21 02:10:01 × urodna quits (~urodna@unaffiliated/urodna) (Quit: urodna)
2020-09-21 02:10:45 <inkbottle> ski: yes, they did
2020-09-21 02:12:47 <ski> ok
2020-09-21 02:13:05 <ski> so, if you have
2020-09-21 02:13:20 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-09-21 02:13:22 <ski> blah :: (forall a. [a] -> [a]) -> [String] -> [String]
2020-09-21 02:13:35 <ski> blah f ss = map f (f ss)
2020-09-21 02:14:11 → notzmv` joins (~user@177.103.86.92)
2020-09-21 02:14:16 <ski> what this means is that `blah' itself is not polymorphic. rather, it requires its first argument (a callback function), to be polymorphic
2020-09-21 02:15:31 <ski> so, you can e.g. call `blah id ["foo","bar"]', but you can't call `blah (map toUpper) ["foo","bar"]', since `map toUpper' has type `String -> String' (that is, `[Char] -> [Char]'), so is not polymorphic
2020-09-21 02:15:58 × notzmv quits (~user@unaffiliated/zmv) (Disconnected by services)
2020-09-21 02:16:11 × notzmv` quits (~user@177.103.86.92) (Changing host)
2020-09-21 02:16:11 → notzmv` joins (~user@unaffiliated/zmv)
2020-09-21 02:16:13 notzmv` is now known as notzmv
2020-09-21 02:16:24 <ski> and, in this case, `blah' uses the fact that `f' is polymorphic, by picking two different types to use for `a', at the two different uses of `f' in the body
2020-09-21 02:16:50 <ski> (can you see if you can figure out which type `a' will be, in each of those two cases ?)
2020-09-21 02:17:38 <ski> (btw, in case, it's not totally obvious, the signature `blah :: forall a. ([a] -> [a]) -> [String] -> [String]' would not work at all, for this implementation of `blah')
2020-09-21 02:18:10 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 246 seconds)
2020-09-21 02:19:01 <ski> if you see `foo :: forall a. ..a..', then that means that the caller/user/consumer of `foo' will get to pick a type for `a'. while the callee/implementor/producer/definer of `foo', which is the definition/body for it, will have to make sure to work for any choice that could be made. may not assuming anything about `a'
2020-09-21 02:19:06 <inkbottle> hang on...
2020-09-21 02:19:18 × polyrain quits (~polyrain@2001:8003:e501:6901:3846:7fa4:c749:eb08) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-09-21 02:19:25 × ystael quits (~ystael@209.6.50.55) (Ping timeout: 240 seconds)
2020-09-21 02:19:38 <inkbottle> still reading what you wrote
2020-09-21 02:19:55 <ski> to the body of `foo', `a' acts like an unknown/forgotten/hidden/opaque/abstract/"skolem"/rigid type, that it may assume nothing about
2020-09-21 02:20:36 → drbean joins (~drbean@TC210-63-209-28.static.apol.com.tw)
2020-09-21 02:20:39 <ski> in the case of `sort :: forall a. Ord a => [a] -> [a]', the implementation of `sort' may assume that `a' is an instance of `Ord', and so can use the methods of `Ord' on values of type `a'. but can assume nothing else about `a'
2020-09-21 02:21:14 <ski> `foo' can't "look inside" values of type `a'. neither can `sort', apart from via the methods of `Ord'
2020-09-21 02:21:36 → notzmv` joins (~user@177.103.86.92)
2020-09-21 02:22:22 <ski> if you have say `foo :: forall a. (a -> Bool) -> ..a..', then `foo' can pass a value of type `a' to its callback argument (which is allowed to know what type `a' is, since it's provided by the caller, who picks `a'), and so is able to extract a `Bool' of info from the `a' value, using that
2020-09-21 02:22:56 <inkbottle> ok
2020-09-21 02:23:06 × notzmv` quits (~user@177.103.86.92) (Changing host)
2020-09-21 02:23:06 → notzmv` joins (~user@unaffiliated/zmv)
2020-09-21 02:23:09 × notzmv quits (~user@unaffiliated/zmv) (Disconnected by services)
2020-09-21 02:23:21 notzmv` is now known as notzmv
2020-09-21 02:23:30 <ski> however, in the case of the rank-two `blah', the caller of the polymorphic `f' is `blah' itself
2020-09-21 02:24:04 <ski> so, while the caller of the polymorphic `foo' was to choose `a', and the callee/implementation couldn't assume anything about `a'
2020-09-21 02:25:19 <ski> in the case of the rank-two `blah', these two rôles are reversed : the callee/implementation of `blah' is the one that can pick and choose types for `a', while the caller of `blah' can't assume anything about `a' (and hence must pass a polymorphic callback, that assumes nothing about `a')
2020-09-21 02:25:22 → ystael joins (~ystael@209.6.50.55)
2020-09-21 02:26:23 × machinedgod quits (~machinedg@d67-193-126-196.home3.cgocable.net) (Ping timeout: 265 seconds)
2020-09-21 02:27:04 → thir joins (~thir@p200300f27f0fc600ed2222922a5678d5.dip0.t-ipconnect.de)
2020-09-21 02:27:10 <ski> this reversal of rôles between caller/user/consumer and callee/implementor/producer/definer, as pertains to who may pick and choose the actual type to use for the type variable `a', and who has to make do with the choice that's being made, is due to, in the rank-two `blah', having `forall' "to the left (inside)" of a function arrow `->'
2020-09-21 02:27:28 hackage containers 0.6.4.1 - Assorted concrete container types https://hackage.haskell.org/package/containers-0.6.4.1 (dfeuer)
2020-09-21 02:27:38 <ski> if you have `foo :: forall a. (..a.. -> ..a..)', then the caller picks `a'
2020-09-21 02:28:04 <ski> if you have `foo :: ... -> (forall a. ..a..)', then the caller still picks `a' (but the first argument isn't allowed to mention `a')
2020-09-21 02:28:30 <ski> (note that e.g. `take :: forall a. Int -> [a] -> [a]' is basically the same thing as `take :: Int -> forall a. [a] -> [a]')
2020-09-21 02:29:00 <ski> but if you have `foo :: (forall a. ..a..) -> ...', the rank-two case, then the callee will get to pick `a'
2020-09-21 02:29:49 × blankhart quits (~blankhart@pool-100-35-219-3.nwrknj.fios.verizon.net) (Ping timeout: 260 seconds)
2020-09-21 02:30:21 × suppi quits (~suppi@2605:f700:40:c00::e6fc:6842) (Ping timeout: 246 seconds)
2020-09-21 02:30:44 <ski> if we had `foo :: ((forall a. ..a..) -> ...) -> ...', this would be rank-three (having a `forall' "inside, to the left of", two function arrows `->'), then the rôles are reversed again, so that the caller again picks `a' (by selecting a rank-two callback to pass, which will pick an `a' (or several), to use with its polymorphic callback)
2020-09-21 02:30:53 <ski> and so on, for higher ranks ..
2020-09-21 02:31:32 → blankhart joins (~blankhart@pool-100-35-219-3.nwrknj.fios.verizon.net)
2020-09-21 02:32:09 → adamwespiser joins (~adam_wesp@209.6.42.110)
2020-09-21 02:32:10 lagothrix is now known as Guest42888
←Prev  Next→
Page 1 .. 103 104 105 106 107 108 109 110 111 112 113 .. 5022

All times are in UTC.