Newest at the top
| 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) |
| 2025-01-14 17:21:34 +0100 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2025-01-14 17:21:14 +0100 | Square2 | (~Square4@user/square) (Ping timeout: 248 seconds) |
| 2025-01-14 17:20:45 +0100 | <haskellbridge> | <Bowuigi> The note on erasure is correct tho IIRC |
| 2025-01-14 17:20:26 +0100 | euleritian | (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) |
| 2025-01-14 17:20:16 +0100 | <haskellbridge> | <Bowuigi> kuribas re:dependent-type-forall even from a dependent type viewpoint, foralls are not lambdas, but it unifies type lambdas and term lambdas (both term level constructs) into one |
| 2025-01-14 17:19:46 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-01-14 17:15:12 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 2025-01-14 17:10:07 +0100 | Digit | (~user@user/digit) Digit |
| 2025-01-14 17:04:34 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-14 17:04:16 +0100 | euleritian | (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-01-14 17:00:34 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-14 16:59:24 +0100 | jespada | (~jespada@2800:a4:31:b00:a974:16da:8c45:e3b4) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-01-14 16:56:40 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2025-01-14 16:52:41 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-01-14 16:44:32 +0100 | inedia | (~irc@2600:3c00:e000:287::1) dove |
| 2025-01-14 16:41:43 +0100 | <merijn> | I don't really go to more frequent things than NL-FP :p |
| 2025-01-14 16:41:06 +0100 | Digit | (~user@user/digit) (Remote host closed the connection) |
| 2025-01-14 16:41:03 +0100 | <__monty__> | Either way, my info dates back 7-ish years. So I don't have current info. |