Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 .. 5022
— 502,152 events total
2020-11-03 12:43:24 <miladz68> Just :: a -> Maybe a
2020-11-03 12:43:58 <miladz68> good so far
2020-11-03 12:44:04 <dminuoso> miladz68: So one of the type inference rules GHC uses, is for instance, if we know `f :: S -> T` for some arbitrary choics of S and T, and we know that `x :: S`, then we can *deduce* that `f x :: T`
2020-11-03 12:44:44 <dminuoso> Anyhow, lets go back!
2020-11-03 12:45:24 <miladz68> I didnt get this part So one of the type inference rules GHC uses, is for instance, if we know `f :: S -> T` for some arbitrary choics of S and T, and we know that `x :: S`, then we can *deduce* that `f x :: T`
2020-11-03 12:46:36 <dminuoso> miladz68: If `f is a function from S to T, and x is something of value S, then the expression `f applied to x` has type T
2020-11-03 12:46:44 <dminuoso> It's a deducible fact
2020-11-03 12:47:02 <miladz68> I understand that
2020-11-03 12:47:32 hackage lsp-types 1.0.0.1 - Haskell library for the Microsoft Language Server Protocol, data types https://hackage.haskell.org/package/lsp-types-1.0.0.1 (luke_)
2020-11-03 12:47:42 <dminuoso> miladz68: That rule can go in both directions, if it somehow figures out `f x :: T`, it can deduce that `f :: _ -> T`
2020-11-03 12:47:44 → ensyde joins (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net)
2020-11-03 12:48:07 × Amras quits (~Amras@unaffiliated/amras0000) (Ping timeout: 272 seconds)
2020-11-03 12:48:44 <miladz68> I think I understand that
2020-11-03 12:49:07 <miladz68> I understand it actually, makes sense
2020-11-03 12:50:04 → Kaiepi joins (~Kaiepi@nwcsnbsc03w-47-55-225-82.dhcp-dynamic.fibreop.nb.bellaliant.net)
2020-11-03 12:50:49 <miladz68> dminuoso please continue if you can
2020-11-03 12:51:09 × mmohammadi9812 quits (~mmohammad@188.210.118.100) (Quit: Quit)
2020-11-03 12:51:10 <dminuoso> miladz68: So all of this was just unrelated, just wanted to nudge you into the mindset of GHC here.
2020-11-03 12:51:24 → mmohammadi9812 joins (~mmohammad@188.210.118.100)
2020-11-03 12:51:37 <miladz68> dminuoso I understand so far
2020-11-03 12:51:38 <dminuoso> Lets start off with a simpler but related example
2020-11-03 12:51:47 <dminuoso> % f :: Maybe Char; f = 2
2020-11-03 12:51:47 <yahb> dminuoso: ; <interactive>:30:22: error:; * No instance for (Num (Maybe Char)) arising from the literal `2'; * In the expression: 2; In an equation for `f': f = 2
2020-11-03 12:51:50 <dminuoso> What happened here?
2020-11-03 12:52:07 <dminuoso> So the first thing to understand, is that numbers are *polymorphic* values
2020-11-03 12:52:25 × ensyde quits (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net) (Ping timeout: 240 seconds)
2020-11-03 12:52:26 <dminuoso> What this code really says is:
2020-11-03 12:52:34 <dminuoso> f :: Maybe Char; f = fromInteger 2
2020-11-03 12:52:39 × mmohammadi9812 quits (~mmohammad@188.210.118.100) (Client Quit)
2020-11-03 12:52:42 <dminuoso> So now, if we look at
2020-11-03 12:52:44 <dminuoso> % :t fromInteger
2020-11-03 12:52:44 <yahb> dminuoso: Num a => Integer -> a
2020-11-03 12:52:55 → mmohammadi9812 joins (~mmohammad@188.210.118.100)
2020-11-03 12:53:09 <dminuoso> This will instantiate the tpye variable `a` at `Maybe Char`, and that's *fine*, the type signature allows for this
2020-11-03 12:53:21 → piyush-kurur joins (~user@14.139.174.50)
2020-11-03 12:53:22 <dminuoso> but that creates a constraint `Num (Maybe Char)` that we need to solve
2020-11-03 12:53:36 <dminuoso> So GHC will look up in its knowledge base, but fail to find a matching instance
2020-11-03 12:53:59 <dminuoso> >> This will instantiate the tpye variable `a` at `Maybe Char`,
2020-11-03 12:54:09 <dminuoso> The reason GHC does this, is what I explained earlier
2020-11-03 12:54:14 <dminuoso> from the type annotation
2020-11-03 12:54:18 <dminuoso> f :: Maybe Char
2020-11-03 12:54:19 <miladz68> dminuoso let me digest this. this is getting interesting
2020-11-03 12:54:21 <dminuoso> It then sees
2020-11-03 12:54:29 <dminuoso> fromInteger 2 :: Maybe Char
2020-11-03 12:54:45 <dminuoso> So it knows the return type of `fromInteger` must be Maybe Char
2020-11-03 12:55:17 <miladz68> dminuoso, so far so good. I understand
2020-11-03 12:56:19 <dminuoso> miladz68: Afterwards, you should really watch the video I linked. Its a wonderful talk :)
2020-11-03 12:56:25 → ghghghgh joins (d4fc771c@212.252.119.28)
2020-11-03 12:56:39 <dminuoso> miladz68: To introduce a new language, to make the *choice* of a type variable of a polymorphic thing apparent, we will write:
2020-11-03 12:56:43 <dminuoso> % id @Int 1
2020-11-03 12:56:44 <yahb> dminuoso: 1
2020-11-03 12:56:52 <dminuoso> The @Int means "set the type variable to Int"
2020-11-03 12:57:02 <dminuoso> So if we have `id :: a -> a`, then `id @Int :: Int -> Int`
2020-11-03 12:57:04 <dminuoso> So far so good?
2020-11-03 12:57:10 → zoran119 joins (~zoran119@124-169-22-52.dyn.iinet.net.au)
2020-11-03 12:57:27 <miladz68> dminuoso good so far
2020-11-03 12:57:34 → AlterEgo- joins (~ladew@124-198-158-163.dynamic.caiway.nl)
2020-11-03 12:58:01 <dminuoso> miladz68: GHC does this internally everywhere, so it's not bad in this discussion.
2020-11-03 12:58:12 <dminuoso> % t :: Fix Mex; t = Fix (Con 2)
2020-11-03 12:58:17 <dminuoso> Let's think about what happens here
2020-11-03 12:58:30 <dminuoso> First thing, we note that `f :: Fix Mex`
2020-11-03 12:58:43 <dminuoso> And we see `t` being bound to `Fix` applied to something
2020-11-03 12:58:53 <dminuoso> So using the same reasoning from above, we can therefore deduce
2020-11-03 12:59:06 <dminuoso> % newtype Fix f = Fix (f (Fix f))
2020-11-03 12:59:06 <yahb> dminuoso:
2020-11-03 12:59:08 <dminuoso> % :t Fix
2020-11-03 12:59:09 <yahb> dminuoso: f (Fix f) -> Fix f
2020-11-03 12:59:18 <dminuoso> Since we know that's the type of Fix
2020-11-03 12:59:40 <dminuoso> To solve for this, we set `f` to some as-of-yet unknown type, call it _t
2020-11-03 12:59:52 <dminuoso> So our Fix has type `_t (Fix _t) -> Fix _t`
2020-11-03 13:00:01 <dminuoso> We then know that
2020-11-03 13:00:04 → ensyde joins (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net)
2020-11-03 13:00:11 <dminuoso> Con 2 :: _t (Fix _t)
2020-11-03 13:00:19 <dminuoso> (Because it appears as an argument to Fix)
2020-11-03 13:00:27 <dminuoso> And we know that `Fix (Con 2) :: Fix _t`
2020-11-03 13:01:10 <dminuoso> And we also know that `Fix (Con 2) :: Fix Mex`
2020-11-03 13:01:20 <dminuoso> So we can deduce that `_t = Mex`
2020-11-03 13:01:29 <dminuoso> If we go plug that knowledge in we notice that:
2020-11-03 13:01:39 <dminuoso> Con 2 :: Mex (Fix Mex)
2020-11-03 13:02:05 <dminuoso> So recall, how a numbers are polymorphic with that fromInteger:
2020-11-03 13:02:13 <dminuoso> Con (fromInteger 2) :: Mex (Fix Mex)
2020-11-03 13:02:50 <dminuoso> From the above data type definition we also have: Con :: a -> Mex a
2020-11-03 13:02:52 → p-core joins (~Thunderbi@193.165.236.104)
2020-11-03 13:03:41 <miladz68> I still cannot see the error
2020-11-03 13:03:44 <dminuoso> Hold on, almost there!
2020-11-03 13:03:52 <dminuoso> miladz68: Did you follow so far?
2020-11-03 13:03:53 → cfricke joins (~cfricke@unaffiliated/cfricke)
2020-11-03 13:04:00 <miladz68> dminusoso Yes
2020-11-03 13:04:36 <dminuoso> So since that Con takes a type variable, we too instantiate some as-of-yet unknown type variable
2020-11-03 13:04:44 <dminuoso> So `Con :: _u -> Mex _u
2020-11-03 13:04:52 × ensyde quits (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net) (Ping timeout: 256 seconds)
2020-11-03 13:04:55 <dminuoso> so (fromInteger 2) :: _u
2020-11-03 13:05:17 <dminuoso> But, we just established:
2020-11-03 13:05:20 <dminuoso> 14:01:39 dminuoso | Con 2 :: Mex (Fix Mex)
2020-11-03 13:05:23 <dminuoso> So we know that _u = Fix Mex
2020-11-03 13:05:25 → urodna joins (~urodna@unaffiliated/urodna)
2020-11-03 13:05:34 <dminuoso> % :t fromInteger
2020-11-03 13:05:34 <yahb> dminuoso: Num a => Integer -> a
2020-11-03 13:05:46 <miladz68> Ok
2020-11-03 13:05:47 <dminuoso> Here too we set `a` to some as-of-yet unknown type called _v
←Prev  Next→
Page 1 .. 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 .. 5022

All times are in UTC.