Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 .. 5022
— 502,152 events total
2020-11-03 12:13:04 × MaoZeDong_ quits (~yuri@2a00:1370:8135:4003:f085:2e15:a839:240d) (Ping timeout: 240 seconds)
2020-11-03 12:15:58 × Kaiepi quits (~Kaiepi@nwcsnbsc03w-47-55-225-82.dhcp-dynamic.fibreop.nb.bellaliant.net) (Remote host closed the connection)
2020-11-03 12:17:00 → idhugo joins (~idhugo@users-1190.st.net.au.dk)
2020-11-03 12:17:03 → ensyde joins (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net)
2020-11-03 12:17:04 × obihann quits (~jhann@156.34.160.69) (Quit: Lost terminal)
2020-11-03 12:17:28 → obihann joins (~jhann@156.34.160.69)
2020-11-03 12:17:53 → Kaiepi joins (~Kaiepi@nwcsnbsc03w-47-55-225-82.dhcp-dynamic.fibreop.nb.bellaliant.net)
2020-11-03 12:18:12 → Deide joins (~Deide@217.155.19.23)
2020-11-03 12:19:24 → Kaeipi joins (~Kaiepi@nwcsnbsc03w-47-55-225-82.dhcp-dynamic.fibreop.nb.bellaliant.net)
2020-11-03 12:20:13 × Kaiepi quits (~Kaiepi@nwcsnbsc03w-47-55-225-82.dhcp-dynamic.fibreop.nb.bellaliant.net) (Remote host closed the connection)
2020-11-03 12:20:45 × TMA quits (tma@twin.jikos.cz) (Ping timeout: 240 seconds)
2020-11-03 12:21:56 × ensyde quits (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net) (Ping timeout: 260 seconds)
2020-11-03 12:22:05 × olligobber quits (olligobber@gateway/vpn/privateinternetaccess/olligobber) (Ping timeout: 240 seconds)
2020-11-03 12:24:19 → miladz68 joins (~manjaro-u@static.84.147.251.148.clients.your-server.de)
2020-11-03 12:24:35 × perrier-jouet quits (~perrier-j@modemcable012.251-130-66.mc.videotron.ca) (Quit: WeeChat 2.9)
2020-11-03 12:25:07 <miladz68> hi everyone
2020-11-03 12:26:38 <miladz68> I have a code that I cannot make to type check. can someone help me here. I also dont know how to copy the code here. I was told this is the best place to ask these kinf of questions if not I would be happy to be pointed to the right place
2020-11-03 12:26:46 <dminuoso> @where paste
2020-11-03 12:26:47 <lambdabot> Help us help you: please paste full code, input and/or output at eg https://paste.tomsmeding.com
2020-11-03 12:27:42 <miladz68> thank you for your responses. here is the code https://paste.tomsmeding.com/dV1xjvgF
2020-11-03 12:28:08 <dminuoso> miladz68: Feel free to use the button "+ Add another file" and then include the type error there
2020-11-03 12:29:38 <miladz68> I added the error
2020-11-03 12:29:46 <dminuoso> miladz68: Ah I see!
2020-11-03 12:29:54 <dminuoso> miladz68: You can't have `Con a` like that
2020-11-03 12:30:04 <dminuoso> You could say `Con Int` instead
2020-11-03 12:30:09 <dminuoso> % newtype Fix f = Fix (f (Fix f))
2020-11-03 12:30:09 <yahb> dminuoso:
2020-11-03 12:30:18 <dminuoso> % data Mex a = Con Int | Ad a a
2020-11-03 12:30:19 <yahb> dminuoso:
2020-11-03 12:30:36 <dminuoso> % v :: Fix Mex; v = Fix (Con 12)
2020-11-03 12:30:37 <yahb> dminuoso:
2020-11-03 12:30:56 <miladz68> what if I want Con to be generic and not specific on Int ?
2020-11-03 12:31:11 <dminuoso> % ex :: Fix Mex; ex = Fx (Fx (Con 2) `Ad` Fx (Con 3))
2020-11-03 12:31:12 <yahb> dminuoso: ; <interactive>:23:21: error:; * Data constructor not in scope: Fx :: Mex a2 -> Fix Mex; * Perhaps you meant one of these: `F#' (imported from GHC.Exts), `Data.Functor.Foldable.Fix' (imported from Data.Functor.Foldable), `Ghci7.Fix' (imported from Ghci7); <interactive>:23:25: error:; * Data constructor not in scope: Fx :: Mex a0 -> a2; * Perhaps you meant one of these: `F#' (imported fr
2020-11-03 12:31:27 <dminuoso> miladz68: Then you must add another type parameter
2020-11-03 12:31:34 <dminuoso> % data Mex t a = Con t | Ad a a
2020-11-03 12:31:34 <yahb> dminuoso:
2020-11-03 12:31:50 <dminuoso> % ex :: Fix Mex; ex = Fix (Fix (Con 2) `Ad` Fix (Con 3))
2020-11-03 12:31:50 <yahb> dminuoso: ; <interactive>:25:11: error:; * Expecting one more argument to `Mex'; Expected kind `* -> *', but `Mex' has kind `* -> * -> *'; * In the first argument of `Fix', namely `Mex'; In the type signature: ex :: Fix Mex
2020-11-03 12:31:51 <dminuoso> err
2020-11-03 12:31:55 <dminuoso> % ex :: Fix (Mex Int); ex = Fix (Fix (Con 2) `Ad` Fix (Con 3))
2020-11-03 12:31:55 <yahb> dminuoso:
2020-11-03 12:31:58 → Aquazi joins (uid312403@gateway/web/irccloud.com/x-cxspimotkygwnrbt)
2020-11-03 12:32:19 <miladz68> Ok thanks
2020-11-03 12:33:17 <miladz68> another question though. I Seem unable to understand how ghc resolves types, what is the best place to learn about this? is there a book ?
2020-11-03 12:34:05 <dminuoso> miladz68: Mmm, the best literature I know of is Pierces TaPL
2020-11-03 12:34:12 <merijn> miladz68: From a basic "I wanna write Haskell" perspective or from "I wanna make this myself" perspective?
2020-11-03 12:34:14 <dminuoso> But depending on what you want to learn it could be a bit heavy
2020-11-03 12:34:42 <merijn> TaPL is more for the latter perspective :p
2020-11-03 12:34:45 <dminuoso> Although..
2020-11-03 12:34:51 <dminuoso> Actually there is a very very good talk
2020-11-03 12:35:01 <dminuoso> miladz68: https://www.youtube.com/watch?v=x3evzO8O9e8
2020-11-03 12:35:13 <dminuoso> There's nobody more qualified to explain how GHCs type inference works than SPJ himself. :)
2020-11-03 12:35:23 <merijn> miladz68: For practical "writing Haskell" is sufficient to think of as an equation solver
2020-11-03 12:35:23 → ensyde joins (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net)
2020-11-03 12:35:54 <miladz68> I want to know how haskell type system works why my code didn't type check and how to write more advanced type level haskell code
2020-11-03 12:36:05 × alp quits (~alp@2a01:e0a:58b:4920:65ec:1bbd:4b97:e92d) (Ping timeout: 272 seconds)
2020-11-03 12:36:26 <merijn> miladz68: The most confusing effect of that equation solving is that, unlike stuff you see in Java/C++/etc. the type checking is bidirectional
2020-11-03 12:36:35 <dminuoso> miladz68: the specific example I can talk you through
2020-11-03 12:36:42 <dminuoso> It's not complicated, it's rather simple, actually
2020-11-03 12:36:49 <dminuoso> % newtype Fix f = Fix (f (Fix f))
2020-11-03 12:36:49 <yahb> dminuoso:
2020-11-03 12:36:50 <kuribas> isn't type checking more like logic programming, but without backtracking?
2020-11-03 12:36:55 <dminuoso> % data Mex a = Con a | Ad a a
2020-11-03 12:36:56 <yahb> dminuoso:
2020-11-03 12:37:08 <dminuoso> % t :: Fix Mex; t = Fix (Con 2)
2020-11-03 12:37:08 <yahb> dminuoso: ; <interactive>:29:28: error:; * No instance for (Num (Fix Mex)) arising from the literal `2'; * In the first argument of `Con', namely `2'; In the first argument of `Fix', namely `(Con 2)'; In the expression: Fix (Con 2)
2020-11-03 12:37:14 <merijn> kuribas: I would argue the "logic programming without backtracking" is just "solving systems of equations"
2020-11-03 12:37:38 <kuribas> makes sense
2020-11-03 12:37:52 <kuribas> as unification is assigning values to variables
2020-11-03 12:37:55 <merijn> miladz68: FWIW, I think wanting to "writing more advanced type level Haskell" is a beginners mistake that leads to more pain than productivity :)
2020-11-03 12:37:57 <dminuoso> miladz68: For a somewhat detailed guide, check out the video of the talk I linked earlier.
2020-11-03 12:38:18 <miladz68> dminuoso please continure. I want to if I can make sense of it
2020-11-03 12:38:25 <dminuoso> Alright
2020-11-03 12:38:45 <dminuoso> miladz68: What's the type of the *data* constructor `Fix` in the above expression bound to t?
2020-11-03 12:38:49 <dminuoso> Monomorphized
2020-11-03 12:38:55 <dminuoso> That is
2020-11-03 12:39:03 <dminuoso> t :: Fix Mex; t = (Fix :: _) (Con 2)
2020-11-03 12:39:05 <miladz68> merjin I am not a complete beginner, I have been wrestling with haskell for 2 years on and off
2020-11-03 12:39:10 <dminuoso> What goes into the hole _ there?
2020-11-03 12:39:20 → alp joins (~alp@2a01:e0a:58b:4920:2923:faed:144a:c0cf)
2020-11-03 12:39:33 <miladz68> let me check with the compiler
2020-11-03 12:39:38 <dminuoso> Id rather you use your head
2020-11-03 12:40:29 × ensyde quits (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net) (Ping timeout: 268 seconds)
2020-11-03 12:40:33 × Kaeipi quits (~Kaiepi@nwcsnbsc03w-47-55-225-82.dhcp-dynamic.fibreop.nb.bellaliant.net) (Remote host closed the connection)
2020-11-03 12:40:53 <dminuoso> If you say "I dont know" that's fine, I can go one step back
2020-11-03 12:40:54 <miladz68> dminuoso Fix :: Fix f is it corect ?
2020-11-03 12:41:08 <merijn> miladz68: Even then, though. I'd consider myself an expert and even in my biggest codebase of like 10k LOC of Haskell, there's maybe 3 lines of advanced type level stuff?
2020-11-03 12:41:14 <miladz68> i would appreciate going an step back
2020-11-03 12:41:17 <dminuoso> Alright
2020-11-03 12:41:23 <dminuoso> Let's start with a simpler example:
2020-11-03 12:41:29 <merijn> Well, maybe a bit more if we count GADTs without type level shenanigans
2020-11-03 12:41:31 <dminuoso> Just 'c'
2020-11-03 12:41:46 <dminuoso> We could play human type inference engine, using intuitive rules we somehow carry in our head
2020-11-03 12:41:58 × xerox_ quits (~xerox@unaffiliated/xerox) (Ping timeout: 260 seconds)
2020-11-03 12:42:09 <dminuoso> We know that 'c' :: Char
2020-11-03 12:42:10 <miladz68> merjin Oh OK. then i want to learn to understand the type system more
2020-11-03 12:42:33 <dminuoso> Then, the data definition of `data Maybe a = Nothing | Just a` gives us `Just a :: a -> Maybe a`
2020-11-03 12:42:55 <miladz68> dminuoso, I understan this
2020-11-03 12:43:19 <dminuoso> So if we apply `Just` to 'c', that means ((Just :: Char -> Maybe Char) 'c') :: Maybe Char
←Prev  Next→
Page 1 .. 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 .. 5022

All times are in UTC.