Newest at the top
| 2025-01-14 18:33:03 +0100 | <r-sta> | i used that but it broke on another error that it didnt have when not using -fbreak-on-error |
| 2025-01-14 18:33:03 +0100 | <geekosaur> | (`-fbreak-on-error` only breaks on unhandled exceptions) |
| 2025-01-14 18:32:33 +0100 | <geekosaur> | you might want `-fbreak-on-error` instead; some things use exceptions internally and usually you don't want ghci stopping in that case |
| 2025-01-14 18:32:23 +0100 | <r-sta> | i was concerned that any kind of diagram would need a fully compiling thing |
| 2025-01-14 18:31:35 +0100 | <r-sta> | i tried using breaks and stepping but it didnt work at all! it didnt even make it *to* the <<loop>> |
| 2025-01-14 18:31:31 +0100 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) (Quit: ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.3)) |
| 2025-01-14 18:31:28 +0100 | kuribas | GTG |
| 2025-01-14 18:31:24 +0100 | <r-sta> | i saw some kind of tree representation or something with -prof |
| 2025-01-14 18:31:24 +0100 | <r-sta> | so im still stuck trying to find out how to debug this <<loop>> in my program |
| 2025-01-14 18:30:34 +0100 | <geekosaur> | I'm considering switching to matrix-appservice-irc so users are puppeted on both sides instead of just the matrix side |
| 2025-01-14 18:30:23 +0100 | r-sta | (~r-sta@sgyl-37-b2-v4wan-168528-cust2421.vm6.cable.virginm.net) |
| 2025-01-14 18:30:06 +0100 | <geekosaur> | yeh |
| 2025-01-14 18:30:00 +0100 | <geekosaur> | (the person on the other side of the bridge has no idea what "haskellbridge" is, it only shows on IRC) |
| 2025-01-14 18:29:59 +0100 | <int-e> | geekosaur: tab-completion actually works for the bridge ;) |
| 2025-01-14 18:29:46 +0100 | <kuribas> | geekosaur: TIL :) |
| 2025-01-14 18:28:45 +0100 | <geekosaur> | why are you talking to the bridge instead of the person on the other side of it? |
| 2025-01-14 18:28:18 +0100 | euleritian | (~euleritia@dynamic-176-004-140-090.176.4.pool.telefonica.de) |
| 2025-01-14 18:26:36 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 2025-01-14 18:24:54 +0100 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2025-01-14 18:21:47 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-14 18:21:34 +0100 | <kuribas> | Or {0 a} -> a |
| 2025-01-14 18:21:34 +0100 | euleritian | (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-01-14 18:21:34 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-01-14 18:20:44 +0100 | <kuribas> | haskellbridge: oh, and I is (forall a . a). |
| 2025-01-14 18:19:27 +0100 | <kuribas> | haskellbridge: "forall a. a -> a" has term "* -> *", but the first argument is implicit, so inferred by the compiler. |
| 2025-01-14 18:17:24 +0100 | <kuribas> | Which is a Pi type. |
| 2025-01-14 18:17:06 +0100 | <kuribas> | AFAIK "forall a.A" is sugar for "{0 a} -> A". |
| 2025-01-14 18:16:40 +0100 | <kuribas> | haskellbridge: but they are in idris2 |
| 2025-01-14 18:11:49 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 2025-01-14 18:11:48 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2025-01-14 18:05:16 +0100 | dmwit | (~dmwit@pool-173-66-76-243.washdc.fios.verizon.net) (Quit: Client closed) |
| 2025-01-14 17:57:36 +0100 | lbseale | (~quassel@user/ep1ctetus) ep1ctetus |
| 2025-01-14 17:56:58 +0100 | <dolio> | Since Π is not the only quantifier when you start getting into such things. |
| 2025-01-14 17:56:08 +0100 | <dolio> | There are some papers on making lambda and pi the same. But they seem misguided to me. |
| 2025-01-14 17:50:44 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2025-01-14 17:49:06 +0100 | jespada | (~jespada@2800:a4:31:b00:a974:16da:8c45:e3b4) jespada |
| 2025-01-14 17:43:54 +0100 | EvanR | (~EvanR@user/evanr) EvanR |
| 2025-01-14 17:43:34 +0100 | EvanR | (~EvanR@user/evanr) (Remote host closed the connection) |
| 2025-01-14 17:41:53 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2025-01-14 17:37:30 +0100 | euleritian | (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) |
| 2025-01-14 17:36:48 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 244 seconds) |
| 2025-01-14 17:35:41 +0100 | <haskellbridge> | <Bowuigi> Instead, combinators should be defined in the usual way but at the type level, using type level lambdas. To get arrows and forall you just add them as combinators, same for pairs, sums, pi types, sigma types, propositional equality types, constraints (the arrow is a "Constraint -> * -> *" operator), etc |
| 2025-01-14 17:34:22 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 252 seconds) |
| 2025-01-14 17:30:32 +0100 | <haskellbridge> | <Bowuigi> The type level combinator system ypu proposed simply wouldn't work. Lemme show you why: Suppose we want to know the type that "I I" expands to. Unfolding everything, using the definition you gave for I ("forall a. a -> a") leaves you with "(forall a. a -> a) (forall a. a -> a)". This term is not well kinded, as you are trying to apply a type of term * to another of term * |
| 2025-01-14 17:28:05 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-14 17:27:50 +0100 | rvalue | (~rvalue@user/rvalue) rvalue |
| 2025-01-14 17:27:47 +0100 | euleritian | (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-01-14 17:27:20 +0100 | rvalue | (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 2025-01-14 17:22:50 +0100 | euleritian | (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) |
| 2025-01-14 17:22:37 +0100 | euleritian | (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |