Newest at the top
| 2025-01-14 11:10:13 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-14 11:09:50 +0100 | <smiesner> | *laughs in java and js* (pls free me) |
| 2025-01-14 11:01:22 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds) |
| 2025-01-14 10:58:34 +0100 | <tomsmeding> | :D |
| 2025-01-14 10:58:23 +0100 | <kuribas> | Python and clojure :( |
| 2025-01-14 10:58:06 +0100 | <kuribas> | gotto do my day job now :) |
| 2025-01-14 10:57:19 +0100 | <kuribas> | tomsmeding: not exactly sure, I'll need to work it out... |
| 2025-01-14 10:56:57 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 244 seconds) |
| 2025-01-14 10:54:45 +0100 | <tomsmeding> | never mind that this type doesn't have a sensible implementation, but more complicated such examples do |
| 2025-01-14 10:54:15 +0100 | <tomsmeding> | so then how are you going to write the type "(f : Type -> Type) -> (a : Type) -> f a"? |
| 2025-01-14 10:53:39 +0100 | <kuribas> | polymorphic types. |
| 2025-01-14 10:53:29 +0100 | <kuribas> | Yeah, in the implementing language. Like HOAS. |
| 2025-01-14 10:52:28 +0100 | <tomsmeding> | wasn't the premise that you can write types using combinators instead of foralls? |
| 2025-01-14 10:52:07 +0100 | <kuribas> | tomsmeding: not in the implementing language. |
| 2025-01-14 10:51:04 +0100 | __monty__ | (~toonn@user/toonn) toonn |
| 2025-01-14 10:50:59 +0100 | <tomsmeding> | but then you aren't actually applying types, are you? What is S? |
| 2025-01-14 10:50:50 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-14 10:50:42 +0100 | <kuribas> | a -> a |
| 2025-01-14 10:50:22 +0100 | <tomsmeding> | what is S? |
| 2025-01-14 10:50:19 +0100 | <tomsmeding> | is I "a -> a"? or is I just "a"? |
| 2025-01-14 10:49:20 +0100 | <kuribas> | But in my case, level 1 would just work. |
| 2025-01-14 10:49:10 +0100 | <kuribas> | yeah, I haven't worked with universes yet... |
| 2025-01-14 10:47:59 +0100 | <tomsmeding> | hm, "-> Set l", perhaps |
| 2025-01-14 10:47:23 +0100 | <tomsmeding> | but the question is: shouldn't it be "I : (l : Level) -> (a : Set l) -> Set ; I l a = a -> a" |
| 2025-01-14 10:47:11 +0100 | m5zs7k | (aquares@web10.mydevil.net) m5zs7k |
| 2025-01-14 10:46:47 +0100 | <tomsmeding> | agda certainly also has implicit inferred universe levels |
| 2025-01-14 10:46:33 +0100 | <kuribas> | Doesn't idris1 have an inferred universe level? |
| 2025-01-14 10:46:13 +0100 | <tomsmeding> | iirc |
| 2025-01-14 10:46:10 +0100 | <tomsmeding> | I : (l : Level) -> (a : Set l) -> a -> a |
| 2025-01-14 10:46:02 +0100 | <kuribas> | If you have an implicit, does it work in all universes? |
| 2025-01-14 10:45:49 +0100 | <kuribas> | idk, how does that work in agda? |
| 2025-01-14 10:45:42 +0100 | <tomsmeding> | but a fun exercise perhaps |
| 2025-01-14 10:45:35 +0100 | <tomsmeding> | I think it isn't at all :p |
| 2025-01-14 10:45:26 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.4.2) |
| 2025-01-14 10:45:26 +0100 | <tomsmeding> | oh I see, so I would be a universe-polymorphic function |
| 2025-01-14 10:45:01 +0100 | <kuribas> | tomsmeding: still not sure if using combinators or lambdas to represent foralls in an advantage though... |
| 2025-01-14 10:44:20 +0100 | <kuribas> | no: I : {a:Type} -> a -> a |
| 2025-01-14 10:44:09 +0100 | swistak | (~swistak@185.21.216.141) (Ping timeout: 260 seconds) |
| 2025-01-14 10:44:09 +0100 | <tomsmeding> | (iirc) |
| 2025-01-14 10:44:08 +0100 | <tomsmeding> | which is precisely possible only if Type : Type |
| 2025-01-14 10:43:34 +0100 | <kuribas> | tomsmeding: well, the forall would need to accept any kind. |
| 2025-01-14 10:41:27 +0100 | <kuribas> | But idris2 doesn't implement it yet. |
| 2025-01-14 10:41:21 +0100 | <kuribas> | It's implied that the Type of Type is Type <2> |
| 2025-01-14 10:40:15 +0100 | <tomsmeding> | ah no, that's false |
| 2025-01-14 10:40:04 +0100 | <tomsmeding> | but you'll only be able to write non-dependent function types this way, I think |
| 2025-01-14 10:39:53 +0100 | <tomsmeding> | in that case you could perhaps do this |
| 2025-01-14 10:39:45 +0100 | <tomsmeding> | so idris2 has Type : Type? |
| 2025-01-14 10:39:35 +0100 | <tomsmeding> | interesting |
| 2025-01-14 10:39:28 +0100 | <kuribas> | yeah |
| 2025-01-14 10:39:24 +0100 | <tomsmeding> | so idris2 is inconsistent? |