Logs: liberachat/#haskell
| 2021-06-02 22:11:20 | × | ddellacosta quits (~ddellacos@86.106.121.17) (Ping timeout: 272 seconds) |
| 2021-06-02 22:11:21 | <hpc> | oh right |
| 2021-06-02 22:12:00 | <hpc> | % class LowerColor (c :: Color) where color :: Tagged c Color |
| 2021-06-02 22:12:00 | <yahb> | hpc: |
| 2021-06-02 22:12:10 | <hpc> | % instance LowerColor Red where color = Tagged Red |
| 2021-06-02 22:12:10 | <yahb> | hpc: |
| 2021-06-02 22:12:16 | <hpc> | % instance LowerColor Green where color = Tagged Green |
| 2021-06-02 22:12:16 | <yahb> | hpc: |
| 2021-06-02 22:12:27 | <hpc> | you can do something like that to get your types back to the value level |
| 2021-06-02 22:12:32 | <hpc> | and it doesn't have to be so direct |
| 2021-06-02 22:14:29 | <dminuoso> | % f :: forall (n :: Nat) (k :: Color) (l :: Color). (KnownNat n, n ~ Value k + Value l) => Tagged k String -> Tagged l String -> (Integer, Int); f (Tagged l) (Tagged r) = (natVal (Proxy @n), length l + length r) |
| 2021-06-02 22:14:29 | <yahb> | dminuoso: |
| 2021-06-02 22:15:00 | <dminuoso> | % f (Tagged "its red" :: Tagged 'Red String) (Tagged "its green" :: Tagged 'Green String) |
| 2021-06-02 22:15:00 | <yahb> | dminuoso: (30,16) |
| 2021-06-02 22:15:37 | <dminuoso> | djb2021: Next level now! We can define variables (by using equality constraints), and then we can pull these type level numbers back into the value level |
| 2021-06-02 22:16:21 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 2021-06-02 22:16:43 | <janus> | ok i have made a repo for my project with template haskell that doesn't work with profiling: http://github.com/ysangkok/cabal-profiling-issue |
| 2021-06-02 22:16:45 | <dminuoso> | Note in particular |
| 2021-06-02 22:16:56 | <dminuoso> | There is a constraint (its left to a =>): |
| 2021-06-02 22:17:00 | <dminuoso> | n ~ Value k + Value l |
| 2021-06-02 22:17:13 | <janus> | if i remove cabal.project, it compiles, but if it is left there, it doesn't. i don't understand it since i thought profiling shouldn't need source changes |
| 2021-06-02 22:17:29 | <djb2021> | wait - i didn't understand your % f :: forall ... |
| 2021-06-02 22:17:40 | <dminuoso> | djb2021: ignore the forall bits until the dot. |
| 2021-06-02 22:17:45 | <dminuoso> | pretend this reads: |
| 2021-06-02 22:17:48 | <hpc> | djb2021: copy it to a text editor and split it into two lines on the ; |
| 2021-06-02 22:17:53 | <dminuoso> | (KnownNat n, n ~ Value k + Value l) => Tagged k String -> Tagged l String -> (Integer, Int); f (Tagged l) (Tagged r) = (natVal (Proxy @n), length l + length r) |
| 2021-06-02 22:18:21 | <dminuoso> | Think of this as setting the variable `n` to be the type family Value applied to k, plus (this is a type level natural plus) type family Value applied to l |
| 2021-06-02 22:18:25 | <dminuoso> | If you recall my above definition |
| 2021-06-02 22:18:31 | <dminuoso> | that means `n ~ 30` at the type level |
| 2021-06-02 22:18:34 | × | michalz quits (~user@185.246.204.60) (Remote host closed the connection) |
| 2021-06-02 22:18:49 | <dminuoso> | natVal let's you pull down a type level natural back into the value world (true magic going on!) |
| 2021-06-02 22:19:18 | <hpc> | % :t natVal |
| 2021-06-02 22:19:18 | <yahb> | hpc: KnownNat n => proxy n -> Integer |
| 2021-06-02 22:19:34 | <hpc> | it's like an infinite version of class LowerColor |
| 2021-06-02 22:20:55 | <monochrom> | Wait a second, I think I heard that profiling and TH can't mix. |
| 2021-06-02 22:21:46 | <Arsen> | can cabal build deps on all cores in cabal install? right now, I'm stuck on a single pandoc build compiling one file at a time, with another 11 cores fully free |
| 2021-06-02 22:22:07 | <dminuoso> | djb2021: or maybe a different example |
| 2021-06-02 22:22:09 | <dminuoso> | % type family Len s where Len '[] = 0; Len (x ': xs) = 1 + Len xs |
| 2021-06-02 22:22:09 | <yahb> | dminuoso: |
| 2021-06-02 22:22:15 | <dminuoso> | Here, type level length for type level lists |
| 2021-06-02 22:23:15 | → | ddellacosta joins (~ddellacos@86.106.121.115) |
| 2021-06-02 22:23:28 | <djb2021> | so computations at the type level? |
| 2021-06-02 22:24:05 | <dminuoso> | % tyl :: forall (n :: Nat) (s :: [Data.Kind.Type]) a. (KnownNat n, n ~ Len s) => Tagged s a -> Integer; tyl _ = natVal (Proxy @n) |
| 2021-06-02 22:24:05 | <yahb> | dminuoso: |
| 2021-06-02 22:24:20 | <janus> | monochrom: oh :O but if that is the case, why doesn't ghc immediatly quit once it sees LANGUAGE TemplateHaskell and profiling is on? |
| 2021-06-02 22:24:37 | <dminuoso> | % tyl (Tagged "foo" :: Tagged '[Float, Double, Int, 'Red, 'Green] String) |
| 2021-06-02 22:24:37 | <yahb> | dminuoso: ; <interactive>:138:29: error:; * Expected a type, but 'Red has kind `Color'; * In the first argument of `Tagged', namely '[Float, Double, Int, 'Red, 'Green]; In an expression type signature: Tagged '[Float, Double, Int, 'Red, 'Green] String; In the first argument of `tyl', namely `(Tagged "foo" :: Tagged '[Float, Double, Int, 'Red, 'Green] String)' |
| 2021-06-02 22:24:44 | <dminuoso> | % tyl (Tagged "foo" :: Tagged '[Float, Double, Int] String) |
| 2021-06-02 22:24:44 | <yahb> | dminuoso: 3 |
| 2021-06-02 22:24:48 | <dminuoso> | err bad example |
| 2021-06-02 22:24:56 | <dminuoso> | % tyl (Tagged "foo" :: Tagged '[Float, Double, Int, Char, IO ()] String) |
| 2021-06-02 22:24:56 | <yahb> | dminuoso: 5 |
| 2021-06-02 22:24:59 | <dminuoso> | djb2021: Yes! |
| 2021-06-02 22:26:19 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2021-06-02 22:26:41 | <dminuoso> | djb2021: The beauty of these type level computations, is that the resulting types can be used to type terms with. |
| 2021-06-02 22:26:50 | × | eight quits (~eight@user/eight) (Quit: Rebooting) |
| 2021-06-02 22:27:23 | <hpc> | and that the type-level language closely resembles the value-level language |
| 2021-06-02 22:27:36 | <hpc> | if you squint, C++ has been doing type-level programming for ages with templates |
| 2021-06-02 22:27:46 | <dminuoso> | servant is a prime example of this. You express an API with a very rich type, and then you use complicated type level computations to turn that rich type into something you can type a function with. |
| 2021-06-02 22:28:15 | <djb2021> | that is exactly what i wanted to write but i hesitated because i was not sure if that is blasphemic :) |
| 2021-06-02 22:28:41 | <djb2021> | ?? |
| 2021-06-02 22:28:42 | × | gehmehgeh quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 2021-06-02 22:28:43 | <dminuoso> | djb2021: https://hackage.haskell.org/package/servant-0.18.2/docs/Servant-API-Generic.html#t:ToServant |
| 2021-06-02 22:28:55 | <djb2021> | i have never used the servant library |
| 2021-06-02 22:28:56 | × | ddellacosta quits (~ddellacos@86.106.121.115) (Ping timeout: 268 seconds) |
| 2021-06-02 22:28:58 | <hpc> | djb2021: now you're getting it :D |
| 2021-06-02 22:29:15 | → | eight joins (~eight@user/eight) |
| 2021-06-02 22:29:24 | <dminuoso> | djb2021: imagine we did this: |
| 2021-06-02 22:29:34 | <dminuoso> | data (path :: k) :> (a :: *) |
| 2021-06-02 22:29:36 | <dminuoso> | % data (path :: k) :> (a :: *) |
| 2021-06-02 22:29:36 | <yahb> | dminuoso: ; <interactive>:141:27: error:; Operator applied to too few arguments: *; With NoStarIsType, `*' is treated as a regular type operator. ; Did you mean to use `Type' from Data.Kind instead? |
| 2021-06-02 22:29:40 | <dminuoso> | % data (path :: k) :> (a :: Type) |
| 2021-06-02 22:29:40 | <yahb> | dminuoso: ; <interactive>:142:27: error:; Ambiguous occurrence `Type'; It could refer to; either `Language.Haskell.TH.Type', imported from `Language.Haskell.TH' (and originally defined in `Language.Haskell.TH.Syntax'); or `Data.Kind.Type', imported from `Data.Kind' (and originally defined in `GHC.Types') |
| 2021-06-02 22:29:43 | <dminuoso> | % data (path :: k) :> (a :: Data.Kind.Type) |
| 2021-06-02 22:29:43 | <yahb> | dminuoso: |
| 2021-06-02 22:30:09 | <hpc> | there's something morbidly hilarious about "Data.Kind.Type" |
| 2021-06-02 22:30:12 | <dminuoso> | djb2021: now next up, you have to accept that strings can exist on the type level too (that is "foo" can be a type!) |
| 2021-06-02 22:30:22 | <dminuoso> | djb2021: are you with me so far? |
| 2021-06-02 22:30:48 | × | azeem quits (~azeem@dynamic-adsl-94-34-34-125.clienti.tiscali.it) (Remote host closed the connection) |
| 2021-06-02 22:30:58 | → | azeem joins (~azeem@dynamic-adsl-94-34-34-125.clienti.tiscali.it) |
| 2021-06-02 22:31:35 | <djb2021> | i didn't understand the servant stuff - what is the goal of the library |
| 2021-06-02 22:31:41 | <dminuoso> | you will in a second! :) |
| 2021-06-02 22:31:59 | <dminuoso> | next up we will conjure a data kind using what we learned |
| 2021-06-02 22:32:29 | <dminuoso> | % data Method = Post | Get |
| 2021-06-02 22:32:29 | <yahb> | dminuoso: |
| 2021-06-02 22:32:37 | <dminuoso> | Now we have a type level 'Post and 'Get |
| 2021-06-02 22:32:39 | × | tonyday quits (~user@202-65-93-249.ip4.superloop.com) (Read error: Connection reset by peer) |
| 2021-06-02 22:32:52 | <dminuoso> | The above data type :> exists without needing any lifting |
| 2021-06-02 22:32:54 | → | tonyday joins (~user@202-65-93-249.ip4.superloop.com) |
| 2021-06-02 22:33:53 | <dminuoso> | djb2021: if you keep on doing this, you get to have a purely type thing that looks like this: |
| 2021-06-02 22:34:25 | <dminuoso> | % type Endpoint = "users" :> Capture "userId" Int :> Get '[JSON] User |
| 2021-06-02 22:34:25 | <yahb> | dminuoso: ; <interactive>:145:28: error: Not in scope: type constructor or class `Capture'; <interactive>:145:58: error: Not in scope: type constructor or class `JSON'; <interactive>:145:64: error: Not in scope: type constructor or class `User' |
| 2021-06-02 22:34:30 | <dminuoso> | Which is just a pure type |
| 2021-06-02 22:34:37 | <dminuoso> | If we can then use type machinery to say: |
| 2021-06-02 22:35:14 | × | wonko quits (~wjc@62.115.229.50) (Quit: See You Space Cowboy..) |
| 2021-06-02 22:35:17 | <dminuoso> | f :: ServerType Endpoint; f userId = loadUserFromDatabase userId |
| 2021-06-02 22:35:24 | → | ru0mad joins (~ru0mad@82-64-17-144.subs.proxad.net) |
| 2021-06-02 22:36:01 | <dminuoso> | The choice `ServerType` is imaginary, but imagine this was a sophisticated type calculation, that would *return* `Int -> IO User` |
| 2021-06-02 22:36:38 | <dminuoso> | This machinery lets us derive a router, server handlers, client handlers - all well typed because the shape is communicated through a type |
| 2021-06-02 22:36:43 | × | ru0mad quits (~ru0mad@82-64-17-144.subs.proxad.net) (Client Quit) |
All times are in UTC.