Logs: freenode/#haskell
| 2020-11-03 14:13:04 | → | xff0x joins (~fox@2001:1a81:53b4:ba00:49d8:d2a:69a9:1ef4) |
| 2020-11-03 14:13:11 | <dminuoso> | daydaynatation: What do you mean by "installed the array package" exactly? |
| 2020-11-03 14:13:28 | <daydaynatation> | cabal install array |
| 2020-11-03 14:13:35 | <daydaynatation> | cabal install array --lib |
| 2020-11-03 14:13:47 | <dminuoso> | Yeah uh, and how did you start ghci? |
| 2020-11-03 14:13:56 | <daydaynatation> | cabal repl |
| 2020-11-03 14:13:59 | → | alp joins (~alp@2a01:e0a:58b:4920:5584:7343:90a1:2565) |
| 2020-11-03 14:14:17 | <dminuoso> | Is your cwd inside a cabal project? |
| 2020-11-03 14:14:34 | → | thunderrd joins (~thunderrd@183.182.115.112) |
| 2020-11-03 14:14:40 | <daydaynatation> | dminuoso: i see where the problem is. stupid me. i can simply run ghci |
| 2020-11-03 14:14:59 | <daydaynatation> | I had the habit of running stack ghci before |
| 2020-11-03 14:16:12 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2020-11-03 14:16:40 | <miladz68> | dminuoso :t flip :: (a -> b -> c) -> b -> a -> c now :t id :: z -> z so taking z as z=b->c replacing it into id we get id :: (b->c) -> (b->c) replacing into filp we get flip :: ( (b->c) -> b ->c) -> b -> (b->c) -> c and :t filp id :: b->(b->c) ->c |
| 2020-11-03 14:17:08 | <dminuoso> | miladz68: That seems a bit short |
| 2020-11-03 14:18:07 | <merijn> | You're skipping a step there, yeah :p |
| 2020-11-03 14:18:29 | <dminuoso> | miladz68: Let me give you a gist for the first step :) |
| 2020-11-03 14:18:56 | × | jjhoo quits (jahakala@dsl-trebng21-b048b5-171.dhcp.inet.fi) (Remote host closed the connection) |
| 2020-11-03 14:19:58 | <miladz68> | All did was to interpret id as :t id :: (b->c) -> b-> c and replace it into flip |
| 2020-11-03 14:20:13 | <miladz68> | dminuoso thanks |
| 2020-11-03 14:21:18 | → | ddellacosta joins (~dd@86.106.121.168) |
| 2020-11-03 14:21:30 | <tomsmeding> | miladz68: sure, but why choose b->c? :) |
| 2020-11-03 14:22:50 | <miladz68> | :tomsmeding because b->c would type check, but I don't know how ghc figures that out. Is that the missing step ? |
| 2020-11-03 14:22:50 | → | jjhoo joins (jahakala@dsl-trebng21-b048b5-171.dhcp.inet.fi) |
| 2020-11-03 14:23:12 | <tomsmeding> | it is :) |
| 2020-11-03 14:24:01 | <miladz68> | tomsmeding i will think more about it then |
| 2020-11-03 14:24:04 | <tomsmeding> | you're applying 'flip' to 'id'; this means that the first argument of 'flip', which has type 'a -> b -> c', must match the type of 'id', which is 'z -> z' |
| 2020-11-03 14:27:40 | → | p-core joins (~Thunderbi@193.165.237.18) |
| 2020-11-03 14:27:49 | <merijn> | miladz68: You get "a -> b -> c = z -> z" which in turn leads to the equations "z = a" and "z = b -> c". Typechecking then consists of validating that none of your equations contradict each other |
| 2020-11-03 14:28:18 | <merijn> | "z = a" and "z = b -> c" is fine IFF "a = b -> c" |
| 2020-11-03 14:29:12 | <miladz68> | merjin thanks. I now see how ghc worked it out. |
| 2020-11-03 14:30:13 | <dminuoso> | miladz68: Im preparing a more slightly more formal write up |
| 2020-11-03 14:30:16 | <dminuoso> | That will probably help |
| 2020-11-03 14:30:21 | → | acidjnk_new2 joins (~acidjnk@p200300d0c718f623ecaa4caf6803be45.dip0.t-ipconnect.de) |
| 2020-11-03 14:30:24 | <miladz68> | what is this process called ? type checking ? type inferrence ? |
| 2020-11-03 14:30:42 | <miladz68> | dminuoso thanks alot. |
| 2020-11-03 14:30:52 | ← | jil` parts (~user@45.86.162.6) ("ERC (IRC client for Emacs 26.1)") |
| 2020-11-03 14:31:03 | → | elfets joins (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) |
| 2020-11-03 14:31:57 | <dminuoso> | miladz68: type inference is an integral part of type checking |
| 2020-11-03 14:33:07 | <dminuoso> | The important realization is that types are not a value level property, they are of syntactical nature. Values dont have types |
| 2020-11-03 14:33:10 | <dminuoso> | Expressions have types |
| 2020-11-03 14:33:15 | <merijn> | dminuoso: Eh, I disagree |
| 2020-11-03 14:33:28 | <merijn> | You can do type checking without inference, so clearly it's not an "integral part" |
| 2020-11-03 14:33:45 | <merijn> | It's just that both use the same machinery in Haskell |
| 2020-11-03 14:34:04 | <dminuoso> | merijn: You cant do much type checking without at least some type inference, really. |
| 2020-11-03 14:34:24 | <dminuoso> | Say, at the very minimum you likely want some kind of [App] inference rule |
| 2020-11-03 14:34:47 | <dminuoso> | I mean yeah. technically you could, its just that such a type system wouldn't do much for you |
| 2020-11-03 14:35:35 | <dminuoso> | Without inference, this could not be checked for instance: f :: Int; f = (g :: Char -> Float) (x :: Char) |
| 2020-11-03 14:35:45 | <dminuoso> | (Or you'd have to just accept it) |
| 2020-11-03 14:36:26 | <merijn> | wut |
| 2020-11-03 14:36:40 | <merijn> | How does that require inference? |
| 2020-11-03 14:37:11 | <dminuoso> | merijn: how do you infer what the type of `g applied to x` is? |
| 2020-11-03 14:37:16 | → | pavonia joins (~user@unaffiliated/siracusa) |
| 2020-11-03 14:37:18 | <dminuoso> | How do you *know* it? |
| 2020-11-03 14:37:38 | <merijn> | You are conflating the English/logical meaning of infer with "type inference" |
| 2020-11-03 14:38:13 | <merijn> | "Char -> Float" applied to "Char" = "Float" isn't inferring anything |
| 2020-11-03 14:38:21 | <dminuoso> | Of course it is. |
| 2020-11-03 14:38:24 | × | chaosmasttter quits (~chaosmast@p200300c4a7117c017972e6cd644c1b14.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 2020-11-03 14:38:48 | <dminuoso> | You have to encode the machinery into the type checker to *know* it can do that |
| 2020-11-03 14:38:51 | <dminuoso> | And that's inference |
| 2020-11-03 14:39:08 | <merijn> | You literally have to encode the machinery to type check into any type checker... |
| 2020-11-03 14:39:12 | <dminuoso> | In the above, `g x :: Char` is an inferred type |
| 2020-11-03 14:39:13 | → | MaoZeDong_ joins (~yuri@2a00:1370:8135:4003:f085:2e15:a839:240d) |
| 2020-11-03 14:39:17 | <merijn> | That's what type checker are |
| 2020-11-03 14:39:18 | <dminuoso> | It's certainly not specified |
| 2020-11-03 14:39:34 | <dminuoso> | Hence my statement: type inference is an integral part of type checking |
| 2020-11-03 14:40:09 | <merijn> | Your usage of type inference does not conform to any common usage of type inference like in, say, TaPL |
| 2020-11-03 14:41:14 | <dminuoso> | It's quite as per TaPL |
| 2020-11-03 14:42:05 | × | daydaynatation quits (~user@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Read error: No route to host) |
| 2020-11-03 14:42:44 | → | christo joins (~chris@81.96.113.213) |
| 2020-11-03 14:43:29 | <dminuoso> | merijn: The reason you're allowed to assume `g x :: Char` in Haskell, is as per [App] rule in the damas milner type inference |
| 2020-11-03 14:43:35 | × | geekosaur quits (82659a09@host154-009.vpn.uakron.edu) (Remote host closed the connection) |
| 2020-11-03 14:43:43 | <merijn> | I refer you to the fact that type inference is discussed on...page 317 of TaPL and not needed for type checking, e.g. the simply typed lambda calculus |
| 2020-11-03 14:43:51 | <merijn> | Which, according to your definition, it would be |
| 2020-11-03 14:44:15 | <merijn> | dminuoso: There are type checking rules for function application too |
| 2020-11-03 14:44:48 | <merijn> | "Char -> Float" applied to "Char" = "Float" is a rule in even the simplest lambda calculus and doesn't require inference, just an application rule (which you need anyway) |
| 2020-11-03 14:45:09 | <merijn> | You only need inference for function application if you don't annotate functions with their argument types |
| 2020-11-03 14:45:15 | <merijn> | Which you already did |
| 2020-11-03 14:46:16 | <merijn> | I refer you to rule E-AppAbs on page 72 of TaPL :) |
| 2020-11-03 14:46:36 | <merijn> | oh, wait, that's the wrong one, hold on |
| 2020-11-03 14:47:21 | <merijn> | T-Abs and T-App on page 103 |
| 2020-11-03 14:47:25 | <dminuoso> | merijn: an application rule *is* an inference rue |
| 2020-11-03 14:47:42 | <merijn> | TaPL disagrees |
| 2020-11-03 14:47:52 | × | PyroLagus quits (PyroLagus@i.have.ipv6.on.coding4coffee.org) (Ping timeout: 246 seconds) |
| 2020-11-03 14:48:08 | → | PyroLagus joins (PyroLagus@i.have.ipv6.on.coding4coffee.org) |
| 2020-11-03 14:48:40 | <merijn> | type inference is the "act of computing a principal type for a term in which some or all annotations are left out" |
| 2020-11-03 14:48:58 | <lortabac> | IIRC most type systems presented in TAPL require no inference at all |
| 2020-11-03 14:49:07 | <merijn> | The fact that you can piggyback inference off of the typing rule for abstraction is orthogonal |
| 2020-11-03 14:49:10 | <lortabac> | STLC, System F... |
| 2020-11-03 14:49:31 | <merijn> | Consider the fact that you can't infer RankN types for functions, but you can still type check them |
| 2020-11-03 14:49:44 | → | Eason0210 joins (~user@101.85.10.81) |
| 2020-11-03 14:49:48 | × | macrover quits (~macrover@ip70-189-231-35.lv.lv.cox.net) (Ping timeout: 258 seconds) |
| 2020-11-03 14:50:21 | <merijn> | You can think of the T-App rule as "a logical inference", but that's not what any of the literature means when they talk about type inference |
| 2020-11-03 14:51:59 | <dminuoso> | 15:47:42 merijn | TaPL disagrees |
| 2020-11-03 14:52:02 | <dminuoso> | Im really curious. |
| 2020-11-03 14:52:09 | <dminuoso> | What you call type inference, TaPL calls type reconstruction |
| 2020-11-03 14:52:33 | <merijn> | It even says "type inference, see type reconstruction" |
| 2020-11-03 14:52:33 | <dminuoso> | The term "type inference" for these "logical inference rules" is used from the beginning throughout the entire book |
| 2020-11-03 14:53:20 | → | Guest8822 joins (562d675a@86-45-103-90-dynamic.agg2.ddk.dbc-mgr.eircom.net) |
| 2020-11-03 14:53:39 | <lortabac> | dminuoso: are you sure? that's not what I remember from reading that book |
| 2020-11-03 14:53:50 | <dminuoso> | lortabac: Im staring at it right now. |
All times are in UTC.