Logs: liberachat/#haskell
| 2021-06-18 09:14:29 | → | Erutuon joins (~Erutuon@user/erutuon) |
| 2021-06-18 09:14:36 | × | Erutuon quits (~Erutuon@user/erutuon) (Client Quit) |
| 2021-06-18 09:14:57 | × | azeem quits (~azeem@176.200.249.255) (Ping timeout: 272 seconds) |
| 2021-06-18 09:15:10 | → | azeem joins (~azeem@176.200.249.255) |
| 2021-06-18 09:15:13 | × | MoC quits (~moc@user/moc) (Quit: Konversation terminated!) |
| 2021-06-18 09:15:17 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-06-18 09:15:33 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-06-18 09:15:41 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-06-18 09:15:41 | × | yd502_ quits (~yd502@180.168.212.6) (Ping timeout: 268 seconds) |
| 2021-06-18 09:15:45 | <Profpatsch> | whttps://github.com/yesodweb/wai/issues/849 |
| 2021-06-18 09:20:42 | × | agumonke` quits (~user@88.163.231.79) (Ping timeout: 240 seconds) |
| 2021-06-18 09:21:36 | <hololeap> | OT question but I've been thinking... is it theoretically possible to create a language that has n-dimensions of type levels? in other words, instead of just types and kinds, also kinds of kinds and kinds of kinds of kinds etc. |
| 2021-06-18 09:21:46 | <dminuoso> | hololeap: Yes. |
| 2021-06-18 09:21:54 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:c962:f999:5484:e62b) |
| 2021-06-18 09:21:58 | <merijn> | hololeap: Google (Extended) Calculus of Constructions |
| 2021-06-18 09:22:44 | <dminuoso> | Dont Idris and Agda have infinite towers like that? |
| 2021-06-18 09:22:44 | <hololeap> | lol I was expecting more of a pause :) |
| 2021-06-18 09:23:03 | <merijn> | dminuoso: Yes, iirc |
| 2021-06-18 09:23:04 | <kuribas> | in a dependent language type level and kind level are the same. |
| 2021-06-18 09:23:17 | <merijn> | kuribas: Yes, but also, no |
| 2021-06-18 09:23:26 | <dminuoso> | kuribas: only in GHC Haskell. |
| 2021-06-18 09:23:29 | <merijn> | TypeInType is malarkey |
| 2021-06-18 09:23:30 | <dminuoso> | or rather, that's a particualr example |
| 2021-06-18 09:23:37 | <merijn> | An abomination unto the lord |
| 2021-06-18 09:23:37 | <dminuoso> | Idris/Agda do not have TypeInType |
| 2021-06-18 09:23:55 | <kuribas> | dminuoso: no, type level and kind level are quite separate in haskell. |
| 2021-06-18 09:24:07 | <merijn> | hololeap: CoC uses an infinite hierarchy with indexing instead of GHC's TypeInType |
| 2021-06-18 09:24:08 | <kuribas> | in idris kind level *is* type level. |
| 2021-06-18 09:24:10 | <hololeap> | well, how would you encode in an actual language, say, the 5th dimension of that stack |
| 2021-06-18 09:24:12 | <merijn> | kuribas: No |
| 2021-06-18 09:24:15 | <kuribas> | the type of a type is just a type. |
| 2021-06-18 09:24:27 | <dminuoso> | 11:23:55 kuribas | dminuoso: no, type level and kind level are quite separate in haskell. |
| 2021-06-18 09:24:29 | <dminuoso> | no they are not |
| 2021-06-18 09:24:29 | <merijn> | idris uses indexed universes like Extended CoC afaik |
| 2021-06-18 09:24:32 | <hololeap> | or have people done stuff like this in idris already? |
| 2021-06-18 09:24:35 | <dminuoso> | kuribas: they are the same in GHC Haskell. |
| 2021-06-18 09:24:50 | <dminuoso> | kuribas: GHC just has a lot of pleasantries in pretty printing error messages to make you think they are different. |
| 2021-06-18 09:24:57 | <merijn> | hololeap: Normally people have either 4 (term, type, kind, sort) or they just generalise to infinity |
| 2021-06-18 09:25:01 | <dminuoso> | and there's some ergonomics. but internally, they are the same |
| 2021-06-18 09:25:04 | <Taneb> | hololeap: so, in Agda, 3 has type Nat which has type Set which has type Set1 which has type Set2 etc |
| 2021-06-18 09:25:13 | <merijn> | hololeap: afaik Idris and Agda generalise to infinity |
| 2021-06-18 09:25:15 | ← | Profpatsch parts (~Profpatsc@static.88-198-193-255.clients.your-server.de) (WeeChat 3.1) |
| 2021-06-18 09:25:40 | <hololeap> | interesting. it totally makes sense, though |
| 2021-06-18 09:26:10 | <dminuoso> | Im not quite sure when the move happened in GHC, but the conflating of Kinds and Types happened a while ago. boxscape surely knows from the top off his heart. |
| 2021-06-18 09:26:11 | × | sekun quits (~sekun@180.190.218.38) (Remote host closed the connection) |
| 2021-06-18 09:26:24 | <boxscape> | 8.0 |
| 2021-06-18 09:26:24 | <merijn> | hololeap: I vaguely recall learning most of this stuff for an Extended CoC paper by Luo |
| 2021-06-18 09:26:32 | <merijn> | hololeap: But it was...pretty brutal to get through :) |
| 2021-06-18 09:26:48 | <hololeap> | will that level of abstraction ever reach GHC, for instance, after dependent types are implemented? |
| 2021-06-18 09:27:03 | → | yd502 joins (~yd502@180.168.212.6) |
| 2021-06-18 09:27:06 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:c962:f999:5484:e62b) (Ping timeout: 240 seconds) |
| 2021-06-18 09:27:17 | <hololeap> | I have been tempted to reach for kinds of kinds before, and then realized they dont exist in GHC |
| 2021-06-18 09:27:38 | <kuribas> | merijn: ah right, Type == Type 1 |
| 2021-06-18 09:27:50 | <kuribas> | :t Type => Type 2 |
| 2021-06-18 09:27:51 | <lambdabot> | error: parse error on input ‘=>’ |
| 2021-06-18 09:27:56 | → | yd502_ joins (~yd502@180.168.212.6) |
| 2021-06-18 09:28:01 | <hololeap> | (although when I go past kinds it's a signal that I'm "smartifying" the problem) |
| 2021-06-18 09:28:40 | → | sekun joins (~sekun@180.190.218.38) |
| 2021-06-18 09:28:49 | <kuribas> | dminuoso: so GHC supports infinite type hierarchies already? |
| 2021-06-18 09:29:14 | <merijn> | kuribas: No |
| 2021-06-18 09:29:16 | <dminuoso> | kuribas: no. |
| 2021-06-18 09:29:26 | <merijn> | kuribas: GHC just goes "lol, fuck it, who needs consistency in their logic" |
| 2021-06-18 09:29:29 | <dminuoso> | kuribas: GHC has TypeInType, meaning `Type :: Type` |
| 2021-06-18 09:29:48 | <dminuoso> | Even if you dont enable the extension, that's the reality of it. |
| 2021-06-18 09:30:07 | <boxscape> | (in fact the extension is deprecated) |
| 2021-06-18 09:30:16 | × | feliix42 quits (~felix@gibbs.uberspace.de) (Read error: Connection reset by peer) |
| 2021-06-18 09:30:30 | <hololeap> | can you use that to (for instance) a kind-level Bool? |
| 2021-06-18 09:30:38 | <hololeap> | *create a |
| 2021-06-18 09:30:47 | × | derelict quits (~derelict@user/derelict) (Ping timeout: 272 seconds) |
| 2021-06-18 09:31:43 | × | yd502 quits (~yd502@180.168.212.6) (Ping timeout: 268 seconds) |
| 2021-06-18 09:32:23 | <hololeap> | I suppose that would be encoded as (k -> k -> k) |
| 2021-06-18 09:33:11 | → | dunkeln joins (~dunkeln@94.129.65.28) |
| 2021-06-18 09:33:30 | → | feliix42 joins (~felix@gibbs.uberspace.de) |
| 2021-06-18 09:35:32 | → | ddellacosta joins (~ddellacos@86.106.121.100) |
| 2021-06-18 09:36:18 | <hololeap> | it should be `True = (k1 -> k2 -> k1) ; False = (k1 -> k2 -> k2)` |
| 2021-06-18 09:37:18 | <hololeap> | is this how DataKinds does it at the low level? does it church-encode an ADT as a type? |
| 2021-06-18 09:37:59 | → | MoC joins (~moc@user/moc) |
| 2021-06-18 09:38:27 | <hololeap> | *as a higher-kinded type |
| 2021-06-18 09:38:54 | × | jneira quits (~jneira@212.8.115.226) (Quit: Client closed) |
| 2021-06-18 09:39:02 | <hololeap> | mm I got lost |
| 2021-06-18 09:39:28 | → | jneira joins (~jneira@212.8.115.226) |
| 2021-06-18 09:39:42 | → | BosonCollider joins (~olofs@90-227-86-119-no542.tbcn.telia.com) |
| 2021-06-18 09:40:21 | × | ddellacosta quits (~ddellacos@86.106.121.100) (Ping timeout: 268 seconds) |
| 2021-06-18 09:41:00 | <boxscape> | I'm not sure there's a good reason for it to use a church encoding here |
| 2021-06-18 09:41:25 | <boxscape> | it seems like you should be able to do something very similar to how ADTs are handled at runtime |
| 2021-06-18 09:41:34 | <boxscape> | but |
| 2021-06-18 09:41:37 | <boxscape> | I don't know how it's done |
| 2021-06-18 09:41:37 | <hololeap> | boxscape: well, I was just thinking that you could use the current mechanism of higher-level kinds to encode different things already |
| 2021-06-18 09:41:54 | <boxscape> | hm |
| 2021-06-18 09:45:35 | → | derelict joins (~derelict@user/derelict) |
| 2021-06-18 09:46:14 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-06-18 09:48:19 | → | fef joins (~thedawn@user/thedawn) |
| 2021-06-18 09:49:02 | → | CookE[] joins (~thedawn@user/thedawn) |
| 2021-06-18 09:49:06 | × | fabfianda quits (~fabfianda@mob-5-90-255-176.net.vodafone.it) (Ping timeout: 268 seconds) |
| 2021-06-18 09:49:28 | → | Katarushisu joins (~Katarushi@cpc152083-finc20-2-0-cust170.4-2.cable.virginm.net) |
| 2021-06-18 09:49:56 | → | fabfianda joins (~fabfianda@net-93-148-121-206.cust.dsl.teletu.it) |
| 2021-06-18 09:51:03 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 272 seconds) |
| 2021-06-18 09:52:48 | × | neceve quits (~quassel@2a02:c7f:607e:d600:a95a:ecd2:e57a:3130) (Ping timeout: 268 seconds) |
| 2021-06-18 09:52:55 | × | fef quits (~thedawn@user/thedawn) (Ping timeout: 252 seconds) |
| 2021-06-18 09:54:54 | → | agumonke` joins (~user@88.163.231.79) |
All times are in UTC.